(Created page with 'The model checker [http://research.microsoft.com/en-us/um/people/lamport/tla/tlc.html TLC] has been integrated into ProB (Tcl/Tk) as of version 1.3.7-beta.') |
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. | |||
= 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]. | |||
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. | |||
= Validating B specifications with TLC = | |||
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. | |||
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. Hence, the user needs no knowledge of TLA+ to use TLC. | |||
As of version 1.3.7-beta, ProB can make use of TLC as an alternative model checker to validate B specifications.
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.
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. Hence, the user needs no knowledge of TLA+ to use TLC.