TLC: Difference between revisions
No edit summary |
No edit summary |
||
| Line 1: | Line 1: | ||
As of version 1.3.7-beta, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. | As of version 1.3.7-beta, ProB can make use of [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] as an alternative model checker to validate B specifications. | ||
= Download and Installation = | = Download and Installation = | ||
TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License]. | TLC has been released as an open source project, under the [http://research.microsoft.com/en-us/um/people/lamport/tla/license.html MIT License]. | ||
To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu. | To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu. | ||
[[File:Download_TLA_Tools.png|400px|center]] | [[File:Download_TLA_Tools.png|400px|center]] | ||
= How to use TLC = | = How to use TLC = | ||
First you have to open a B specification in the ProB GUI. | 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. | Then you can select the menu command "Model Check with TLC" in the "Verify->External Tools" menu. | ||
| Line 32: | Line 32: | ||
= Translation from B to TLA+ = | = Translation from B to TLA+ = | ||
TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html TLA+]. | TLC is a very efficient model checker for specifications written in [http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html 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. | 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. | ||
Revision as of 15:19, 4 December 2013
As of version 1.3.7-beta, ProB can make use of TLC as an alternative model checker to validate B specifications.
Download and Installation
TLC has been released as an open source project, under the MIT License. To use TLC in the ProB Tcl/Tk GUI you have to select the menu command "Download and Install TLA Tools" in the Help menu.
How to use TLC
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:
- Deadlocks
- Invariant violations
- Assertion errors
- Goal found (a desired state is reached)
- Properties violations (i.e, axioms over the B constants are false)
- Well-definedness violations
- Temporal formulas violations
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.
Translation from B to TLA+
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.
There is a technical report that describes our translation from B to TLA+.