mona - a decision procedure for the logics WS1S and WS2S
mona [ options ] mona-file
MONA is a tool that translates formulas in the logics WS1S
or WS2S into finite-state automata represented by BDDs. The formulas may
express search patterns, temporal properties of reactive systems, parse tree
constraints, etc. MONA also analyses the automaton resulting from the
compilation, and determines whether the formula is valid and, if the formula
is not valid, generates a counter-example.
The MONA project is a research project at Department of Computer
Science, Aarhus University.
Full documentation, GPL source code, and related research papers
are available from the MONA project home page at
http://www.brics.dk/mona
- -w
- Output whole automaton. Default is to only output its size.
- -n
- Don't analyze automaton. Default is to analyze for validity and
unsatisfiability and to generate a satisfying example and
counter-example.
- -t
- Print elapsed time for each phase. If -s is also used, the time for each
automaton operation is also printed.
- -s
- Print statistics. Prints information for each automaton operation and a
summary.
- -i
- Print intermediate automata (implies -s).
- -d
- Dump AST, symboltable, and code DAG. Useful for debugging.
- -q
- Quiet, don't print progress.
- -e
- Enable separate compilation. (See the MONALIB environment variable
below.)
- -oN
- Code optimization level N (0=none, 1=safe, 2=heuristic) (default 1).
- -r
- Disable BDD index reordering, use order of declaration as index ordering.
Default is to reorder BDD indices heuristically.
- -f
- Force normal tree-mode output style. Only applicable for WSRT mode.
- -m
- Alternative M2L-Str emulation (v1.3 style).
- -h
- Enable inherited acceptance analysis.
- -u
- Unrestrict output automata. Create conventional automata by converting
"don't-care" states to "reject" states and
minimizes.
- -gw
- Output whole automaton in Graphviz format (implies -n -q). (Graphviz is
available at http://www.graphviz.org/)
- -gs
- Output satisfying example tree in Graphviz format (implies -q).
- -gc
- Output counter-example tree in Graphviz format (implies -q).
- -gd
- Dump code DAG in Graphviz format (implies -n -q).
- -xw
- Output whole automaton in external format (implies -n -q). "External
format" is the format used by dfalib and gtalib, see the source
package.
- MONALIB
- Defines the directory used for separate-compilation automata (default is
current directory).
Please send bug reports to <amoeller@cs.au.dk>
Anders Moeller, Nils Klarlund, Jacob Elgaard, Theis Rauhe, and
Morten Biehl.