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 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

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.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.

ENVIRONMENT

       MONALIB
              Defines the directory used for separate-compilation automata (default is current directory).

BUGS

       Please send bug reports to <amoeller@cs.au.dk>

AUTHORS

       Anders Moeller, Nils Klarlund, Jacob Elgaard, Theis Rauhe, and Morten Biehl.

                                                   MARCH 2016                                            MONA(1)