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 support JavaScript.
Print elapsed time Print statistics 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 Normal output