NAME¶
mona - a decision procedure for the logics WS1S and WS2S
SYNOPSIS¶
mona [
options ]
mona-file
DESCRIPTION¶
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 the BRICS Research Center at
University of Aarhus, Denmark.
Full documentation, GPL source code, and related research papers are available
from the MONA project home page at
http://www.brics.dk/mona
OPTIONS¶
- -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.research.att.com/sw/tools/graphviz/)
- -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.
ENVIRONMENT¶
- MONALIB
- Defines the directory used for separate-compilation
automata (default is current directory).
BUGS¶
Please send bug reports to <mona@brics.dk>
AUTHORS¶
Anders Moeller <amoeller@brics.dk>, Nils Klarlund, Jacob Elgaard, Theis
Rauhe, and Morten Biehl.