TLC: Difference between revisions

Line 57: Line 57:
  INVARIANT
  INVARIANT
   x : 1..10
   x : 1..10
  INITIALISATION x:=1
  INITIALISATION x:=k
  END
  END


ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):
[[File:NumberOfStates.jpeg|1000px|thumb|left|State space generated by ProB]]
[[File:NumberOfStates.jpeg|800px|left|State space generated by ProB]]
TLC will only report 10 distinct states (10 initialization states).
TLC will only report 10 distinct states (10 initialization states).


= More Information =
= More Information =
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].
More information can be found in our [http://www.stups.uni-duesseldorf.de/w/Special:Publication/HansenLeuschel_ABZ14 ABZ'14 article].

Revision as of 10:06, 10 November 2014

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.

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.

Download TLA Tools.png

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.

Model Checking With TLC.png

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.

Model Checking With TLC Trace.png

When to use TLC

TLC is extremely valuable when it comes to explicit state model checking for large state spaces. Otherwise, TLC has no constraint solving abilities.

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+.

Limitations

The following constructs are currently not supported by the TLC4B translator:

  • Refinement specifications
  • Machine inclusion (SEES, INCLUDES, ..)
  • Sequential composition statement (G;H)

Visited States

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 : 1..10
INITIALISATION x:=k
END

ProB will report 21 distinct states (1 root state, 10 constant setup states, 10 initialization states):

State space generated by ProB

TLC will only report 10 distinct states (10 initialization states).

More Information

More information can be found in our ABZ'14 article.