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)