LTSmin

LTSmin is a high-performance language-independent model checker that allows numerous modelling language front-ends to be connected to various analysis algorithms, through a common interface.

LTSmin Extension of ProB

We have implemented an integration of LTSmin with ProB for symbolic reachability and for explicit state model checking:

Symbolic Reachability Analysis of B Through ProB and LTSmin, Proceedings of iFM'2016
State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin, Proceedings iFM'2018.

In order to set up the LTSmin and ProB integration, do the following:

Download the latest LTSmin release: https://github.com/utwente-fmt/ltsmin/releases and extract it
(Linux only) start ProB via LD_LIBRARY_PATH=lib/ ./prob if you have not installed ZeroMQ and CZMQ
In ProB, go to Preferences > All Preferences (alphabetical)…
Set the LTSmin preference to the bin/ subfolder of the extracted LTSmin archive
Start Model Checking via Verify > External Tools > Model Checking with LTSmin (see screenshot below)

Note that the LTSmin extension is not available for Windows.

ProB LTSmin CLI-Commands

Note that on Linux, you might prefix the commands with LD_LIBRARY_PATH=lib/

Flag	Example	Description
-ltsmin	probcli -ltsmin FILE	Start the ProB server for LTSmin at the default endpoint /tmp/ltsmin.probz - it will use the machine FILE in order to provide information to LTSmin
-ltsmin2	probcli -ltsmin2 endpoint.probz FILE	Start the ProB server for LTSmin at the endpoint given by the specific endpoint.probz file. It will use the machine FILE in order to provide information to LTSmin
-mc-with-lts-seq	probcli -nodead -mc-with-lts-seq FILE	Start invariant model checking with the sequential backend of LTSmin on FILE. Note that at least one of -nodead or -noinv must be provided.
-mc-with-lts-sym	probcli -nodead -mc-with-lts-sym FILE	Start invariant model checking with the symbolic backend of LTSmin on FILE. Note that at least one of -nodead or -noinv must be provided.
-p LTSMIN	-p LTSMIN /opt/ltsmin/	Use the LTSmin commands in the provided directory (here /opt/ltsmin)