OnWorks favicon

mona - Online in the Cloud

Run mona in OnWorks free hosting provider over Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

This is the command mona that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator



mona - a decision procedure for the logics WS1S and WS2S


mona [ options ] mona-file


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

Full documentation, GPL source code, and related research papers are available from the
MONA project home page at http://www.brics.dk/mona


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


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

Use mona online using onworks.net services

Free Servers & Workstations

Download Windows & Linux apps

  • 1
    The strace project has been moved to
    https://strace.io. strace is a
    diagnostic, debugging and instructional
    userspace tracer for Linux. It is used
    to monitor a...
    Download strace
  • 2
    A GUI for mkvextract utility (part of
    MKVToolNix) which incorporates most (if
    not all) functionality of mkvextract and
    mkvinfo utilities. Written in C#NET 4.0,...
    Download gMKVExtractGUI
  • 3
    JasperReports Library
    JasperReports Library
    JasperReports Library is the
    world's most popular open source
    business intelligence and reporting
    engine. It is entirely written in Java
    and it is able to ...
    Download JasperReports Library
  • 4
    Frappe Books
    Frappe Books
    Frappe Books is a free and open source
    desktop book-keeping software that's
    simple and well-designed to be used by
    small businesses and freelancers. It'...
    Download Frappe Books
  • 5
    Numerical Python
    Numerical Python
    NEWS: NumPy 1.11.2 is the last release
    that will be made on sourceforge. Wheels
    for Windows, Mac, and Linux as well as
    archived source distributions can be fou...
    Download Numerical Python
  • 6
    CMU Sphinx
    CMU Sphinx
    CMUSphinx is a speaker-independent large
    vocabulary continuous speech recognizer
    released under BSD style license. It is
    also a collection of open source tools ...
    Download CMU Sphinx
  • 7
    Old Feren OS Repositories
    Old Feren OS Repositories
    This was the Official Repository for
    Feren OS. To add the latest one, run
    this command: (16.04-based) echo
    "deb ...
    Download Old Feren OS Repositories
  • More »

Linux commands