Jan Gruteser (talk | contribs) |
|||
(3 intermediate revisions by 2 users not shown) | |||
Line 39: | Line 39: | ||
* -noltl (no checking of LTL assertions) | * -noltl (no checking of LTL assertions) | ||
ProB Preferences influencing TLC: | |||
* <tt>TLC_WORKERS</tt>: influences the number of workers that will be used by TLC; a call might look like this: | |||
probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl | <tt>probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl</tt> | ||
* <tt>TLC_USE_PROB_CONSTANTS</tt>: setup constants using ProB before applying TLC (can lead to a considerable speed-up); e.g. | |||
<tt>probcli FILE.mch -mc_with_tlc -p TLC_USE_PROB_CONSTANTS TRUE</tt> | |||
= When to use TLC = | = When to use TLC = | ||
Line 56: | Line 58: | ||
The following article describes the translation in more detail: | The following article describes the translation in more detail: | ||
* Dominik Hansen and Michael Leuschel. Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, pages 109-125. 2016. [https://doi.org/10.1016/j.scico.2016.04.014 Link]. | * Dominik Hansen and Michael Leuschel. Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, pages 109-125. 2016. [https://doi.org/10.1016/j.scico.2016.04.014 Link]. | ||
= Limitations = | = Limitations = | ||
Line 63: | Line 63: | ||
* Refinement specifications | * Refinement specifications | ||
* Machine inclusion (SEES, INCLUDES, ..) | * Machine inclusion (SEES, INCLUDES, ..) | ||
* Sequential composition | * Sequential composition (G;H) with variables assigned more than once | ||
= Visited States = | = Visited States = | ||
Line 85: | Line 85: | ||
= More Information = | = More Information = | ||
More information can be found in our [https:// | More information can be found in our article which is an extended version of the ABZ'2014 conference paper: | ||
* Dominik Hansen and Michael Leuschel. Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131, pages 109-125. 2016. [https://doi.org/10.1016/j.scico.2016.04.014 Link]. |
As of version 1.4.0, ProB can make use of TLC as an alternative model checker to validate B specifications. TLC is an efficient model checker for TLA+ specifications, which can check LTL properties with fairness. It is particularly good for lower level specifications, where it can be substantially faster than ProB's own model checker. TLC has been released as an open source project, under the MIT License.
First you have to open a B specification in the ProB GUI. Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu.
You can use TLC to find the following kinds of errors in the B specification:
In some cases, TLC reports a trace leading to the state where the error (e.g. deadlock or invariant violation) occur. Such traces are automatically replayed in the ProB animator (displayed in the history pane) to give an optimal feedback.
On Linux the tlc-thread package is required to run TLC from the tcl/tk ui:
sudo apt-get install tcl-thread
You can use the following switch to use TLC rather than ProB's model checker:
-mc_with_tlc
Some of the standard probcli options also work for TLC:
In addition you can provide
ProB Preferences influencing TLC:
probcli FILE.mch -mc_with_tlc -p TLC_WORKERS 2 -noltl
probcli FILE.mch -mc_with_tlc -p TLC_USE_PROB_CONSTANTS TRUE
TLC is extremely valuable when it comes to explicit state model checking for large state spaces. Otherwise, TLC has no constraint solving abilities.
TLC is a very efficient model checker for specifications written in TLA+. To validate B specification with TLC we developed the translator TLC4B which automatically translates a B specification to TLA+, invokes the model checker TLC, and translates the results back to B. Counter examples produced by TLC are double checked by ProB and replayed in the ProB animator. The translation to TLA+ and back to B is completely hidden to the user. Hence, the user needs no knowledge of TLA+ to use TLC.
The following article describes the translation in more detail:
The following constructs are currently not supported by the TLC4B translator:
Sometimes TLC will show a different number of visited states compared to the ProB model checker. The following example should illustrate this issue:
MACHINE NumberOfStates CONSTANTS k PROPERTIES k : 1..10 VARIABLES x INVARIANT x : NATURAL INITIALISATION x := k END
ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
TLC will only report 10 distinct states (10 initialization states).
More information can be found in our article which is an extended version of the ABZ'2014 conference paper: