All tools based on Owl
understand the same LTL input language.
The following constructs are supported:
tt
, true
, 1
ff
, false
, 0
[a-zA-Z_][a-zA-Z_0-9]*
!
, NOT
->
, =>
, IMP
<->
, <=>
, BIIMP
^
, XOR
&&
, &
, AND
||
, |
, OR
(
, )
F
G
X
U
W
R
M
The parser uses the following precedence:
OR
< AND
< Binary Expressions < Unary Expressions < Literals, Constants, Parentheses
For chained binary expressions (without parentheses), the rightmost binary operator takes precedence.
For example, a -> b U c
is parsed as a -> (b U c)
.