Safety checker for Petri Nets (and monotonic extensions)
Ruby C Python Yacc M4 C++ Other
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
benchmarks
img
regression-tests
scripts
src
.gitignore
AUTHORS
COPYING
ChangeLog
INSTALL
Makefile.am
NEWS
README
README.md
autogen.sh
configure.ac

README.md

mist - a safety checker for Petri Nets and extensions

mist is tool to check safety properties against Petri Net like models. It implements a variety of search algorithms described on the wiki. Even though mist has its own input format there it can be translated from other formats (using, for instance, tttrans) mist also ships with Python scripts to run mist over sets of benchmarks and an infrastructure producing bar graphs using d3js with runtime and memory consumption information.

Building mist on Unix

Type ./configure, then make.

If ./configure does not exist (you downloaded from Github), run autoreconf -i first.

make install will build and install mist (under /usr/local by default).

./configure accepts the usual options; see INSTALL for more details.

make uninstall will uninstall mist.

Synopsis

 $ mist --algorithm --[option] <input_file>
 $ mist --help
 $ mist --version

Algorithm

Algorithm: Description of the algorithm
backward the backward algorithm with invariant pruning described in Laurent Van Begin PhD thesis
ic4pn the abstraction refinement algorithm described in Fundamenta Informaticae, 88(3), 2008
tsi the abstraction refinement algorithm described in Technique et Sciences Informatiques, 28(9), 2009
eec Expand, Enlarge and Check algorithm described in the Journal of Computer and System Sciences, 72(1), 2005
eec-cegar Expand, Enlarge and Check with a counter-example based refinement (not described anywhere)

Options

Option Effect of the option
timeout <T> establish an execution timeout of T seconds. Atfer that time the execution will be stopped and proper message will be shown
graph <filename> creates a file called filename to store the data needed to plot graphs of the memory usage and execution time of the given algorithm
verbose <V> establish a verbosity level V
help this help
version show version number

Input file format and further details

Further information can be found on the wiki.

Reporting Problems

Please report issues on GitHub.

Further Questions

Contact the author, Pierre Ganty.

Requirements

You need to install mustache to generate the graphs with our script.

Tested under linux (Ubuntu 14.10) and MacOS (OSX 10.9)