LTSmin: Difference between revisions
| Line 9: | Line 9: | ||
* [https://link.springer.com/chapter/10.1007%2F978-3-319-98938-9_16 State-of-the-Art Model Checking for B and Event-B Using ProB and LTSmin], Proceedings iFM'2018. | * [https://link.springer.com/chapter/10.1007%2F978-3-319-98938-9_16 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 | 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 | * Download the latest LTSmin release: https://github.com/utwente-fmt/ltsmin/releases and extract it | ||
| Line 15: | Line 15: | ||
* In ProB, go to Preferences > All Preferences (alphabetical)… | * In ProB, go to Preferences > All Preferences (alphabetical)… | ||
* Set the LTSmin preference to the bin/ subfolder of the extracted LTSmin archive | * Set the LTSmin preference to the bin/ subfolder of the extracted LTSmin archive | ||
* Start Model Checking via Verify > External Tools > Model Checking with LTSmin | * Start Model Checking via Verify > External Tools > Model Checking with LTSmin (see screenshot below) | ||
Note that the LTSmin extension is not available for Windows. | Note that the LTSmin extension is not available for Windows. | ||
[[File:ProBLTSMinTk.png||800px]] | [[File:ProBLTSMinTk.png||800px]] | ||
Revision as of 12:43, 9 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.
