dk.brics.automaton  |  dk.brics.grammar  |  dk.brics.schematools
Thor  |  TSCheck  |  JSRefactor  |  Artemis  |  TAJS  |  Java String Analyzer  |  XSLT Validator  |  WARlord  |  XSugar  |  Xact  |  JWIG
MONA  |  PALE

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:


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.

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