CIF explorer crashes on models with minimum integer value
CIF model:
automaton a:
disc int i = -2147483647 - 1; // Minimum integer value.
location:
initial;
end
Running the CIF explorer on this model gives:
java.lang.RuntimeException: Specification became invalid.
at org.eclipse.escet.cif.checkers.CifChecker.check(CifChecker.java:75)
at org.eclipse.escet.cif.explorer.app.ExplorerApplication.runInternal(ExplorerApplication.java:287)
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:840)
Caused by: Failed to load CIF file "<in-memory-cif-spec>": the file has errors.
at org.eclipse.escet.setext.runtime.io.BaseReader.tcheck(BaseReader.java:245)
at org.eclipse.escet.setext.runtime.io.BaseReader.read(BaseReader.java:213)
at org.eclipse.escet.cif.checkers.CifChecker.check(CifChecker.java:73)
... 6 more
The CIF explorer runs the 'simplify values (no refs, optimized)' CIF to CIF transformation, which simplifies the value to an integer literal that is not a valid CIF integer literal. When checking the 'requirements as plant' precondition using the new checkers framework, the model is pretty printed to an invalid model that can't be read in again.