Skip to content
/ mist Public
forked from pierreganty/mist

Safety checker for Petri Nets (and monotonic extensions)

License

Notifications You must be signed in to change notification settings

pevalme/mist

 
 

Repository files navigation

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)

About

Safety checker for Petri Nets (and monotonic extensions)

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • C 93.0%
  • Python 3.9%
  • Bison 2.4%
  • Shell 0.7%