Skip to content

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;
end

The 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.