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.
For ease of use, pre-built binaries are available using these links :
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.
$ mist --algorithm --[option] <input_file>
$ mist --help
$ mist --version
| 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) |
| 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 |
Further information can be found on the wiki.
Please report issues on GitHub.
Contact the author, Pierre Ganty.
You need to install mustache to generate the graphs with our script.
Tested under linux (Ubuntu 14.10) and MacOS (OSX 10.9)