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

Disjunctions in forbidden states #24

Closed asogokon closed 8 years ago

asogokon commented 8 years ago

There appears to be an issue with verification problems featuring disjunctions in the description of the forbidden states. For a concrete example, one may consider the following .cfg :

system = arrowsmith_and_place_fig_3_8_page_82 initially = "x == 1 & y == -1" forbidden = "x < 0 | y > 0" output-variables = x,y scenario = stc directions = box set-aggregation = "none" sampling-time = 0.5 flowpipe-tolerance = 0.25 time-horizon = 9 iter-max = 4 output-format = GEN verbosity = m output-error = 0.001 rel-err = 1.0e-12 abs-err = 1.0e-15

SpaceEx does not appear to have an issue with this, but with HyST one gets

Automaton Export Exception while exporting: Parser Error; Could not parse initial/forbidden: 'x < 0 | y > 0'; sample syntax: loc(automaton) == start & x == 5 & y >= 0 & y <= x For more information about the error, use the -verbose or -debug flag.

Conversion completed with exit code 6: EXPORT_AUTOMATON_EXCEPTION

Disjunctions are really not that unusual in safety specifications; oftentimes the safe states in a system are described using conjunctions such as e.g. x<=1 /\ x>=-1, which turn into disjunctions upon negating them to obtain the forbidden states.

asogokon commented 8 years ago

with '-verbose' :

Verbose mode printing enabled.

line 1:6 no viable alternative at input '|' Automaton Export Exception while exporting: Parser Error; Could not parse initial/forbidden: 'x < 0 | y > 0'; sample syntax: loc(automaton) == start & x == 5 & y >= 0 & y <= x Stack trace from exception: com.verivital.hyst.ir.AutomatonExportException: Parser Error; Could not parse initial/forbidden: 'x < 0 | y > 0'; sample syntax: loc(automaton) == start & x == 5 & y >= 0 & y <= x at com.verivital.hyst.grammar.formula.FormulaParser.parseInitialForbidden(Unknown Source) at de.uni_freiburg.informatik.swt.spaxeexxmlreader.SpaceExXMLReader.parseCFG(Unknown Source) at de.uni_freiburg.informatik.swt.spaxeexxmlreader.SpaceExXMLReader.read(Unknown Source) at com.verivital.hyst.importer.SpaceExImporter.importModels(Unknown Source) at com.verivital.hyst.main.Hyst.convert(Unknown Source) at com.verivital.hyst.main.Hyst.main(Unknown Source) Caused by: com.verivital.hyst.ir.AutomatonExportException: Could not parse initial/forbidden: 'x < 0 | y > 0' at com.verivital.hyst.grammar.formula.FormulaParser.getExpression(Unknown Source) ... 6 more Caused by: org.antlr.v4.runtime.misc.ParseCancellationException at org.antlr.v4.runtime.BailErrorStrategy.recoverInline(BailErrorStrategy.java:90) at org.antlr.v4.runtime.Parser.match(Parser.java:229) at com.verivital.hyst.grammar.antlr.HystExpressionParser.locExpression(Unknown Source) at com.verivital.hyst.grammar.formula.FormulaParser.getParseTree(Unknown Source) ... 7 more Caused by: org.antlr.v4.runtime.InputMismatchException at org.antlr.v4.runtime.BailErrorStrategy.recoverInline(BailErrorStrategy.java:85) ... 10 more

stanleybak commented 8 years ago

The grammar didn't support it, I'll try to get to it tomorrow.

ttj commented 8 years ago

We figured as much, thanks Stan! If you don't get to it tomorrow, let us know, it shouldn't be a big deal to fix (e.g., my ANTLR grammar in passel supported disjunction, etc.).

We need to fix another whitespace tokenization bug in the grammar as per another issue as well that showed up with initial or forbidden states (which leads to a stack overflow...)

stanleybak commented 8 years ago

This is now fixed in this pull request: https://github.com/verivital/hyst/pull/25