mona - a decision procedure for the logics WS1S and WS2S

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

                                                   MARCH 2016                                            MONA(1)

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

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

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

       mona - a decision procedure for the logics WS1S and WS2S

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

mona [ options ] mona-file