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

Failing RemoveSimpleUnsatInvariantsPass #27

Closed omarali75 closed 8 years ago

omarali75 commented 8 years ago

I have successfully analyzed this example in SpaceEx. But during hyst conversion, it failed the invariant pass as per following error message in hyst: "Automaton Export Exception while exporting: Hybrid Automaton IR structure was corrupted after running pass com.verivital.hyst.passes.basic.RemoveSimpleUnsatInvariantsPass".

invariants_pass_issue.zip

stanleybak commented 8 years ago

When I convert the model using verbose mode, I get the message:

Exported label 'jump_i' was not used in BaseComponent ''. This would block all transitions using this label in other components, and is typically a mistake.

If you look at controller_i and converter_i, we see what this error means. In automaton converter_i, we have a single mode with invariant control_i==1. In controller_i there are two modes, one with invariant control_i==1 and one with control_i==0. Since the mode with control_i==0 could NEVER be entered (because there is no mode in converter_i that satisfies the invariant), it is removed, along with all of its transitions.

In this way, controller_i is left with no transitions, in particular no transitions that use the jump_i label. This has the effect of blocking every other automaton that uses the jump_i label (these transitions can never be taken, since there is no such transition in controller_i), which is typically a mistake and is what is reported.

This is not a bug in Hyst, but a malformed model which I believe we'd be better off rejecting than allowing the user to think everything is okay. Hope that makes sense.