Dear Alexandre: I am trying to figure out whether SPOT can accept boolean assertions such as "x >1". For example, can SPOT recognize the LTL formula F (x > 1), which is accepted by Promela format? I tried it with SPOT by ./ltl2tgba -f "F (x>1)" and SPOT fails to parse it. But I really want to make sure whether I have used it correctly. Many thanks~ -- Best Regards Jianwen Li
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
participants (2)
-
Alexandre Duret-Lutz -
Jianwen Li