1MONA(1)                           BRICS tools                          MONA(1)
2
3
4

NAME

6       mona - a decision procedure for the logics WS1S and WS2S
7

SYNOPSIS

9       mona [ options ] mona-file
10

DESCRIPTION

12       MONA is a tool that translates formulas in the logics WS1S or WS2S into
13       finite-state automata represented by BDDs.  The  formulas  may  express
14       search  patterns,  temporal  properties of reactive systems, parse tree
15       constraints, etc.  MONA also analyses the automaton resulting from  the
16       compilation,  and  determines  whether the formula is valid and, if the
17       formula is not valid, generates a counter-example.
18
19       The MONA project is a research project at Department of  Computer  Sci‐
20       ence, Aarhus University.
21
22       Full  documentation,  GPL  source code, and related research papers are
23       available from the MONA project home page at http://www.brics.dk/mona
24

OPTIONS

26       -w     Output whole automaton. Default is to only output its size.
27
28       -n     Don't analyze automaton. Default is to analyze for validity  and
29              unsatisfiability  and  to  generate  a  satisfying  example  and
30              counter-example.
31
32       -t     Print elapsed time for each phase. If -s is also used, the  time
33              for each automaton operation is also printed.
34
35       -s     Print  statistics.  Prints information for each automaton opera‐
36              tion and a summary.
37
38       -i     Print intermediate automata (implies -s).
39
40       -d     Dump AST, symboltable, and code DAG. Useful for debugging.
41
42       -q     Quiet, don't print progress.
43
44       -e     Enable separate compilation. (See the MONALIB environment  vari‐
45              able below.)
46
47       -oN    Code optimization level N (0=none, 1=safe, 2=heuristic) (default
48              1).
49
50       -r     Disable BDD index reordering, use order of declaration as  index
51              ordering.  Default is to reorder BDD indices heuristically.
52
53       -f     Force  normal  tree-mode  output style. Only applicable for WSRT
54              mode.
55
56       -m     Alternative M2L-Str emulation (v1.3 style).
57
58       -h     Enable inherited acceptance analysis.
59
60       -u     Unrestrict output automata. Create conventional automata by con‐
61              verting "don't-care" states to "reject" states and minimizes.
62
63       -gw    Output  whole  automaton  in  Graphviz  format  (implies -n -q).
64              (Graphviz is available at http://www.graphviz.org/)
65
66       -gs    Output satisfying example tree in Graphviz format (implies -q).
67
68       -gc    Output counter-example tree in Graphviz format (implies -q).
69
70       -gd    Dump code DAG in Graphviz format (implies -n -q).
71
72       -xw    Output whole automaton  in  external  format  (implies  -n  -q).
73              "External  format"  is the format used by dfalib and gtalib, see
74              the source package.
75

ENVIRONMENT

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

BUGS

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

AUTHORS

85       Anders  Moeller,  Nils Klarlund, Jacob Elgaard, Theis Rauhe, and Morten
86       Biehl.
87
88
89
90                                  MARCH 2016                           MONA(1)
Impressum