Maria

The Modular Reachability Analyzer

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.

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

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

Introductory Material

Read also about the background of the Maria project, and see our publications.

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:

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

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.

Documentation

The user's guide for Maria 1.3.4, produced with the GNU project Texinfo system, is available in PDF.

The structure of the reachability graph files and the grammar of the automata are described separately.

The Maria coding style is based on the Ellemtel recommendations.


This page is also available in the following languages:
suomi
How to set the default document language


Marko Mäkelä, the Maria project

Valid HTML 4.01!