search

verivital / hyst

HyST: A Source Transformation and Translation Tool for Hybrid Automaton Models
http://verivital.com/hyst/
Other
15 stars 18 forks source link

Unsupported operation for range extraction #36

Closed rajray84 closed 8 years ago

rajray84 commented 8 years ago

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 commented 8 years ago

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

stanleybak commented 8 years ago

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.