Maria is a reachability analyzer for concurrent systems that uses Algebraic System Nets.

Maria is a reachability analyzer for concurrent systems that uses Algebraic System Nets (a high-level variant of Petri nets) as its modelling formalism. It has been written in C++, and its is freely available under the terms of the GNU General Public License.

Maria relies on external programs translating LTL formulae into generalised Büchi automata or finite-word automata. It communicates with these programs by writing a formula to the standard input of the translator and by reading the translated automaton from the standard output of the translator. Each formula is translated in a separate run of the external program. The program is invoked without arguments.

Maria maps the state numbers in the property automata to a contiguous sequence. If you want to see the automata after this mapping, define the preprocessor symbol DEBUG_AUTOMATON when compiling the file Property.C. In that way, Maria will dump the mapped automaton to the standard output. The automaton can be visualised with the lbt2dot tool of LBT.

To grab the formula sent by Maria to the external translator, write a wrapper shell script for the translator that does something like tee formula.txt | exec the-real-translator.

Extensions.

An LTL-X model checker for modular state spaces is available separately. Because the implementation is incomplete, it is available as a patch file against version 1.3.4 and as a patch file against version 1.3.5. Please refer to the installation instruction..

Status of the Tool.

The reachability analyzer, the on-the-fly model checker and the reachability graph traverser have been working since 1999, when version 0.1 was released. Version 0.2 that was published in 2001 has more advanced features, such as model checking with fairness constraints, a net unfolder, a C code generator, and a graphical user interface.

The reachability graph visualization tool is based on GraphViz, a graph visualization library developed at AT&T. There are two implementations of the graph visualizer:

• The first implementation, developed in April 2001, is based on the graph editor dotty written in a scripting language lefty of GraphViz. It is the recommended graphical front-end, and it works with older versions of GraphViz.
• The second implementation, developed in June 2001, is based on Tcl/Tk version 8.3 and the tcldot library of an up-to-date development version of GraphViz. This version is experimental, and it lacks many features. It can display only one graph at a time.

Marko Mäkelä stopped developing the tool in 2004. Version 1.3.5 (with minor portability and performance improvements) will most likely be the last one prepared by him.

External Tools.

• GraphViz visualizes graphs
• LBT translates LTL formulae to Büchi automata
• TVT is not exactly utilized by Maria, but Maria can analyze LSTS models in the TVT format.
• Sforza+ translates Object Petri Nets in the LOOPN++ syntax into Maria syntax.

Obtaining the Code.

The source code is distributed via http://www.tcs.hut.fi/Software/maria/src/. It can be translated into machine executable form e.g. with GCC.

You can also get the most recent development version of the source code and the documentation.

For the convenience of Windows users, we provide a zip file containing an executable that was compiled with gcc-2.95.2 configured as a cross-compiler for the mingw target platform. This version is at a preliminary stage. The option for generating C code is disabled, and graph visualization does not work.

Released Versions.

0.1
September 17, 1999

0.2
August 10, 2001

1.0
November 1, 2001

1.0.1
February 5, 2002

1.1
April 23, 2002

1.2
June 23, 2002

1.3
September 4, 2002

1.3.1
November 15, 2002

1.3.2
December 5, 2002

1.3.3
December 9, 2002

1.3.4
June 20, 2003

1.3.5
July 29, 2005

If you liked this article, subscribe to the feed by clicking the image below to keep informed about new contents of the blog: