CIF explorer crashes due to inconsistent calculations of number of possible initial states
The precondition check is correct, but the CIF explorer may come to a wrong conclusion, leading to crashes.
For instance, consider the following model:
automaton a:
disc int x in any;
invariant x >= 0;
location:
initial;
end
automaton b:
location:
initial false;
endThe precondition check correctly concludes there are zero initial states, as b has no initial location. The explorer considers b to have one potential location, and since a.x has many potential initial values, it is more than we can support. It leads to an assertion failure:
java.lang.AssertionError
at org.eclipse.escet.common.java.Assert.check(Assert.java:38)
at org.eclipse.escet.cif.explorer.runtime.Explorer.getPotentialInitialStates(Explorer.java:298)
at org.eclipse.escet.cif.explorer.runtime.Explorer.getInitialStates(Explorer.java:201)
at org.eclipse.escet.cif.explorer.app.ExplorerApplication.explore(ExplorerApplication.java:198)
at org.eclipse.escet.cif.explorer.app.ExplorerApplication.runInternal(ExplorerApplication.java:155)
at org.eclipse.escet.common.app.framework.Application.runApplication(Application.java:315)
at org.eclipse.escet.common.app.framework.Application.run(Application.java:180)
at org.eclipse.escet.common.eclipse.ui.BaseFileCommandHandler.run(BaseFileCommandHandler.java:261)
at org.eclipse.escet.common.eclipse.ui.BaseFileCommandHandler$1.run(BaseFileCommandHandler.java:102)
at java.base/java.lang.Thread.run(Thread.java:1583)We should fix the inconsistencies between the precondition check and the CIF explorer's own computations.