LTSmin: Difference between revisions
| Line 54: | Line 54: | ||
An example run: | An example run: | ||
<pre> | <pre> | ||
$ probcli scheduler.mch -mc_with_lts_seq -noinv -p LTSMIN ~/bin/ltsmin_v3.0.2/bin | |||
starting prob2lts-sym/seq (flags nodead=false, noinv=true, moreflags=[]) | starting prob2lts-sym/seq (flags nodead=false, noinv=true, moreflags=[]) | ||
prob2lts-seq, 0.001: ProB module initialized | prob2lts-seq, 0.001: ProB module initialized | ||
Revision as of 08:00, 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 (containing the binaries prob2-lts-seq, prob2lts-sym, ...)
- 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/
| probcli 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) |
An example run:
$ probcli scheduler.mch -mc_with_lts_seq -noinv -p LTSMIN ~/bin/ltsmin_v3.0.2/bin starting prob2lts-sym/seq (flags nodead=false, noinv=true, moreflags=[]) prob2lts-seq, 0.001: ProB module initialized prob2lts-seq, 0.001: Loading model from /tmp/ltsmin.probz prob2lts-seq, 0.001: ProB init prob2lts-seq, 0.002: connecting to zocket ipc:///private/tmp/ltsmin.probz pl_init_for_lts_min vars([active,ready,waiting]) prob2lts-seq, 0.026: There are 7 state labels and 1 edge labels prob2lts-seq, 0.026: State length is 4, there are 6 groups prob2lts-seq, 0.026: Running dfs search strategy prob2lts-seq, 0.026: Using a tree for state storage prob2lts-seq, 0.147: state space 30 levels, 36 states 156 transitions prob2lts-seq, 0.147: Deadlocks: >= 0 prob2lts-seq, 0.147: terminating ProB connection get-next-state: 121 get-next-state (short): 0 get-next-action: 0 get-next-action (short): 0 get-state-label: 0 get-state-label (short): 0 get-label-group: 0 prob2lts-seq, 0.147: disconnecting from zocket ipc:///private/tmp/ltsmin.probz /prob2lts-seq with [--trace,/tmp/prob-ltsmin-trace.gcf,-c,-d] exited with status: exit(0) LTSMin found no counter example