Rabinizer tryout

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").
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)