2 Mar
2015
2 Mar
'15
11:39 p.m.
I tried it with SPOT by ./ltl2tgba -f "F
(x>1)" and SPOT fails to parse it.
There are two ways to parse it:
Either quote the part you want Spot to consider as an atomic proposition:
ltl2tgba 'F("x > 1")'
Or use --lenient to allow any parenthesized block that Spot do not
understand to be considered as an atomic proposition
ltl2tgba --lenient 'F(x > 1)'
See this page for more examples:
http://spot.lip6.fr/userdoc/ioltl.html