mona(1) [debian man page]
MONA(1) BRICS tools MONA(1) 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 the BRICS Research Center at University of Aarhus, Denmark. 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.research.att.com/sw/tools/graphviz/) -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 <mona@brics.dk> AUTHORS
Anders Moeller <amoeller@brics.dk>, Nils Klarlund, Jacob Elgaard, Theis Rauhe, and Morten Biehl. FEBRUARY 2008 MONA(1)
Check Out this Related Man Page
grammar::fa::dacceptor(n) Finite automaton operations and usage grammar::fa::dacceptor(n) __________________________________________________________________________________________________________________________________________________ NAME
grammar::fa::dacceptor - Create and use deterministic acceptors SYNOPSIS
package require Tcl 8.4 package require snit package require struct::set package require grammar::fa::dacceptor ?0.1.1? ::grammar::fa::dacceptor daName fa ?-any any? daName option ?arg arg ...? daName destroy daName accept? symbols _________________________________________________________________ DESCRIPTION
This package provides a class for acceptors constructed from deterministic finite automatons (DFA). Acceptors are objects which can be given a string of symbols and tell if the DFA they are constructed from would accept that string. For the actual creation of the DFAs the acceptors are based on we have the packages grammar::fa and grammar::fa::op. API
The package exports the API described here. ::grammar::fa::dacceptor daName fa ?-any any? Creates a new deterministic acceptor with an associated global Tcl command whose name is daName. This command may be used to invoke various operations on the acceptor. It has the following general form: daName option ?arg arg ...? Option and the args determine the exact behavior of the command. See section ACCEPTOR METHODS for more explanations. The acceptor will be based on the deterministic finite automaton stored in the object fa. It will keep a copy of the relevant data of the FA in its own storage, in a form easy to use for its purposes. This also means that changes made to the fa after the construction of the acceptor will not influence the acceptor. If any has been specified, then the acceptor will convert all symbols in the input which are unknown to the base FA to that symbol before proceeding with the processing. ACCEPTOR METHODS
All acceptors provide the following methods for their manipulation: daName destroy Destroys the automaton, including its storage space and associated command. daName accept? symbols Takes the list of symbols and checks if the FA the acceptor is based on would accept it. The result is a boolean value. True is returned if the symbols are accepted, and False otherwise. Note that bogus symbols in the input are either translated to the any symbol (if specified), or cause the acceptance test to simply fail. No errors will be thrown. The method will process only just that prefix of the input which is enough to fully determine (non-)acceptance. EXAMPLES
BUGS, IDEAS, FEEDBACK This document, and the package it describes, will undoubtedly contain bugs and other problems. Please report such in the category gram- mar_fa of the Tcllib SF Trackers [http://sourceforge.net/tracker/?group_id=12883]. Please also report any ideas for enhancements you may have for either package and/or documentation. KEYWORDS
acceptance, acceptor, automaton, finite automaton, grammar, parsing, regular expression, regular grammar, regular languages, state, trans- ducer CATEGORY
Grammars and finite automata COPYRIGHT
Copyright (c) 2004 Andreas Kupries <andreas_kupries@users.sourceforge.net> grammar_fa 0.1.1 grammar::fa::dacceptor(n)