Owl On-Line Demo

Some formulas to try out (simply copy-paste them in the above field):

Format:

DGRA (Rabinizer construction)
DRA (Rabinizer + Degeneralization)
DPA (Rabinizer + Degeneralization + IAR construction)
DPA (LDBA construction)
LDBA

Options:

Show state annotations (Warning: Large pictures)
Highlight SCCs (green: contains acc cycle, red: contains no acc cycle, black: trivial, gray: useless)


We use Spot's autfilt to convert the result into the dot format and render it to SVG using the equally named tool.