The MONA Project

Try MONA online! Just type in a MONA program and click "Run MONA". The User Manual contains a thorough description of how to use MONA and how it works.

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.

MONA program:


Options:

Output whole automaton
Disable automaton analysis

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