LTSmin: Difference between revisions
| Line 20: | Line 20: | ||
[[File:ProBLTSMinTk.png||600px]] | [[File:ProBLTSMinTk.png||600px]] | ||
== ProB LTSmin CLI-Commands == | |||
Note that on Linux, you might prefix the commands with LD_LIBRARY_PATH=lib/ | |||
Flag Example Usage 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) | |||
Revision as of 07:41, 10 June 2020
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 Usage 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)