Unsupported operation for range extraction

[rajray84]

I see
error model.zip

the following message when trying to print a SpaceEx model in Flow* format. The model works with the SpaceEx tool. Please find the model file and the cfg file attached to reproduce the error msg.

---

Variable u1 didn't have dynamics defined in mode loc_0 as required in the preconditions. Attempting to convert using ConverHavocFlowsPass.
Converting Havoc Flows
Automaton Export Exception while exporting: Havoc dynamics in Hyst can currently only have interval nondeterminism
Stack trace from exception:
com.verivital.hyst.ir.AutomatonExportException: Havoc dynamics in Hyst can currently only have interval nondeterminism
at com.verivital.hyst.internalpasses.ConvertHavocFlows.run(ConvertHavocFlows.java:81)
at com.verivital.hyst.util.Preconditions.convertAllFlowAssigned(Preconditions.java:147)
at com.verivital.hyst.util.Preconditions.check(Preconditions.java:76)
at com.verivital.hyst.printers.ToolPrinter.checkPreconditions(ToolPrinter.java:407)
at com.verivital.hyst.printers.ToolPrinter.print(ToolPrinter.java:134)
at com.verivital.hyst.main.Hyst.runPrinter(Hyst.java:283)
at com.verivital.hyst.main.Hyst.convert(Hyst.java:210)
at com.verivital.hyst.main.Hyst.main(Hyst.java:140)
Caused by: com.verivital.hyst.util.RangeExtractor$UnsupportedConditionException: Unsupported operation for range extraction in expression: x1 >= 0 & x1 <= 1 & x2 >= 0 & x2 <= 1 & -NavigationBenchmark_umax <= u1 & u1 <= NavigationBenchmark_umax & -NavigationBenchmark_umax <= u2 & u2 <= NavigationBenchmark_umax
at com.verivital.hyst.util.RangeExtractor.getVariableRange(RangeExtractor.java:204)
at com.verivital.hyst.internalpasses.ConvertHavocFlows.run(ConvertHavocFlows.java:65)
... 7 more
Caused by: com.verivital.hyst.util.RangeExtractor$UnsupportedConditionException: Unsupported condition for range extraction (one side should be variable, the other side a constant): -NavigationBenchmark_umax <= u1
at com.verivital.hyst.util.RangeExtractor.getVariableRangesRecursive(RangeExtractor.java:364)
at com.verivital.hyst.util.RangeExtractor.getVariableRangesRecursive(RangeExtractor.java:286)
at com.verivital.hyst.util.RangeExtractor.getVariableRangesRecursive(RangeExtractor.java:286)
at com.verivital.hyst.util.RangeExtractor.getVariableRangesRecursive(RangeExtractor.java:287)
at com.verivital.hyst.util.RangeExtractor.getVariableRangesRecursive(RangeExtractor.java:287)
at com.verivital.hyst.util.RangeExtractor.getVariableRangesRecursive(RangeExtractor.java:287)
at com.verivital.hyst.util.RangeExtractor.getVariableRangesRecursive(RangeExtractor.java:287)
at com.verivital.hyst.util.RangeExtractor.getVariableRange(RangeExtractor.java:182)
... 8 more

[stanleybak]

This had been fixed in my master fork https://github.com/stanleybak/hyst, which is part up the pull request: #35

[stanleybak]

The core issue was related to the Hyst IR. Resets are represented as Expression + Interval, where Intervals are pairs of double's. However, in this case, you're using a named constant as part of the interval, not a value... so this caused the error. Two solutions are to either rework the IR, which is a lot of work, or to substitute constant values for named constants (which we already have a pass for). I opted for the latter, and added it as a precondition for all passes and printers unless they explicitly indicate they support named constants.