You might want to try one of the following examples:
- a WS1S example from the manual.
- a WS2S (tree logic) example from the manual.
- verification of a hardware circuit.
- verification of a mutual-exclusion algorithm.
Click "Run MONA" below to start MONA on our server. Graphviz-format
output will be shown in GIF format. You should get a reply within
30 seconds (or 60 if using Graphviz options). The reply might look
strange if the resource limits are exceeded. If you don't receive an
answer, try disabling the Graphviz options (click "normal output"
button). You have limited access to the demo server resources: max
64MB memory and max. 30 seconds per execution. Your browser must
Print elapsed time
Dump AST, symboltable and code DAG
Disable progress reports
Force tree-mode output style
Output whole automaton in Graphviz format (linear mode only)
Output satisfying example tree in Graphviz format (tree mode only)
Output counter-example tree in Graphviz format (tree mode only)
Dump code DAG in Graphviz format