Abstract
This manual describes MONA version 1.4. Section 1 contains an introductory example and a brief description of MONA applications. In Section 2, the basic features of the MONA tool are described through a number of examples. Section 3 discusses the automaton-logic connection and the MONA compilation semantics. Section 4 describes DAGification, formula reduction, and separate compilation. In Section 5, it is shown how to make MONA produce detailed information about the processing and the resulting automata. Section 6 describes some more advanced constructs, such as, exporting and importing automata, controlling restrictions, and emulating Presburger arithmetic and M2L-Str. In Section 7, the decision procedure for WS2S is presented along with the MONA concept of Guided Tree Automata and an extension with recursive types. Section 8 discusses our plans for future work. In the appendices, the full syntax is defined, the command-line usage of MONA is shown, and the MONA DFA, GTA, and BDD packages are described.
The complete source code for MONA version 1.4 is available under the GNU General Public License. Please visit the MONA home page at http://www.brics.dk/mona for further information.