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.
| 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 |
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..
Read also about the background of the Maria project, and see our publications.
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:
dotty written in a scripting language
lefty of GraphViz. It is the recommended graphical
front-end, and it works with older versions of GraphViz.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.
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.
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