Line 85: | Line 85: | ||
The formula itself can spread several lines. Additional comments can be added with a leading #. | The formula itself can spread several lines. Additional comments can be added with a leading #. | ||
If a counter-example is found, the trace of the counter-example is saved into the file | If a counter-example is found, the trace of the counter-example is saved into the file ltlce_Name.trace, where Name is the name of the formula in the LTL file. |
ProB provides support for LTL (linear temporal logic) model checking. For an introduction see the Wikipedia Article.
To use this feature, select "Check LTL formula..." in the "Verify" menu. The following dialog appears:
You can enter an LTL formula in the dialog's text field. We explain the supported syntax below. If the model checker finds a counter-example the animator navigates to the last state of the counter-example. The full path can then be seen in the history.
The model checker searches for a counter-example (i.e. a path that does not satisfy the current formula). Where the checked pathes through the model's search space start depend on the following options:
Note: Whereas `Y true` is always false when checked with option 1 or 2, it is usually true (but not in all cases) for option 3.
There are three possible results:
The LTL model checker searches in the already explored search space of the model. If a state is encountered that has not been explored before, the state will be explored (i.e. all transitions to successor states are calculated). The number of how often this can happen is limited by the field "Max no. of new states".
Depending on the LTL formula, a partially explored state space can be sufficient to find a counter-example or to assure the absence of a counter-example. If there's still the possibility of a counter-example in the remaining unexplored state space, the user will get a message.
ProB supports LTLe, an extended version of LTL. In contrast to standard LTL, LTLe also supports propositions on transitions, not only on states. In practice, this allows the operator `[...]` (see below). Also Past-LTL is supported.
LTL formulas can be stored in the `DEFINITIONS` section of a B machine. The name of the definition must start with `ASSERT_LTL` and a string must be specified. E.g.:
DEFINITIONS ASSERT_LTL == "G ([add] => X {card(db)>0})"
All assertions can be checked automatically by selecting "Check LTL assertions" in the "Verify" menu. Each formula is checked for all paths starting in the states of the initialisation of the machine. Formulas that pass are marked green, formulas that failed are marked red.
With the command line version of ProB it is possible to check several LTL formulas with one call. The command has the following syntax
probcli -ltlfile FILE ...
The file FILE contains one or more sections, where each section has the form
[Name] Formula
The formula itself can spread several lines. Additional comments can be added with a leading #.
If a counter-example is found, the trace of the counter-example is saved into the file ltlce_Name.trace, where Name is the name of the formula in the LTL file.