MONA(1) 							    BRICS tools 							   MONA(1)

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.

								   FEBRUARY 2008							   MONA(1)