Please insert an LTL[F,G] formula in the text field below and press "Generate". If everything works,
you should see shortly afterwards a gif file showing the graph of an automaton corresponding to the formula.
Examples of valid formulas (F, G binds
more strongly than "&" and "|"):
Atomic variables can be arbitrary strings of alphanumeric characters (except "F" and "G").
- F a & G (!a | F b)
- G F 1 & G F 0
- ((F G reset) | (G F loc2)) & G test & ! G wait & init
Please note that e.g. "Fa" is a single atomic variable, whereas "F a" (a space separating "F" and "a") denotes an instance of the F-operator.
(Sunday, 29th of April, 2012)