An LTL formula may contain propositional symbols, boolean operators, temporal operators, and parentheses.
true, false any lowercase stringBoolean operators:
! (negation) -> (implication) <-> (equivalence) && (and) || (or)Temporal operators:
G (always) (Spin syntax : ) F (eventually) (Spin syntax : <>) U (until) R (realease) (Spin syntax : V) X (next)Use spaces between any symbols.
Our program can draw automatically the resulting automaton, and can also print a never claim that can be given to the Spin model checker to verify properties on a system.
Automatas are drawn by 'dot', a program devellopped in the Graphviz package.