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 the BRICS Research Center  at
20       University of Aarhus, Denmark.
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
65              http://www.research.att.com/sw/tools/graphviz/)
66
67       -gs    Output satisfying example tree in Graphviz format (implies -q).
68
69       -gc    Output counter-example tree in Graphviz format (implies -q).
70
71       -gd    Dump code DAG in Graphviz format (implies -n -q).
72
73       -xw    Output  whole  automaton  in  external  format  (implies -n -q).
74              "External format" is the format used by dfalib and  gtalib,  see
75              the source package.
76

ENVIRONMENT

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

BUGS

83       Please send bug reports to <mona@brics.dk>
84

AUTHORS

86       Anders Moeller <amoeller@brics.dk>, Nils Klarlund, Jacob Elgaard, Theis
87       Rauhe, and Morten Biehl.
88
89
90
91                                 FEBRUARY 2008                         MONA(1)
Impressum