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.
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 first implementation, developed in April 2001, is based on the graph editor
dottywritten in a scripting language
leftyof 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
tcldotlibrary 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.
- 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.
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.
September 17, 1999
August 10, 2001
November 1, 2001
February 5, 2002
April 23, 2002
June 23, 2002
September 4, 2002
November 15, 2002
December 5, 2002
December 9, 2002
June 20, 2003
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: