Line 141: | Line 141: | ||
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. | 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. | ||
== Other Tutorials about LTL Model Checking == | == Other Tutorials about LTL Model Checking == | ||
A brief tutorial on visualizing LTL counter-examples in the Rodin tool can be found [ | A brief tutorial on visualizing LTL counter-examples in the Rodin tool can be found [http://www.stups.uni-duesseldorf.de/ProB/index.php5/Tutorial_LTL_Counter-example_View here]. | ||
== References == | == References == | ||
<references /> | <references /> |
ProB provides support for LTL (linear temporal logic) model checking. For an introduction to LTL see the Wikipedia Article.
To use this feature, select "Check LTL/CTL Assertions" in the "Verify" menu. The feature can also be accessed by the key combination "Ctrl+L" under Windows and Linux, and by the key combination "Cmd+L" under MacOS. The following window appears:
All LTL formulas that are given in the "DEFINTIONS" section of a B machine are displayed in the list box of the LTL/CTL Assertions Viewer. For CSP-M specifications all LTL formulas given in the LTL pragmas of the loaded CSP-M file will be shown in the viewer. (For more detailed information of how LTL/CTL assertions can be stored into B and CSP-M models see Section Storing LTL Assertions into a Model).
A new LTL formula can be entered in the entry below the list box. (We explain the supported syntax below). The typed formula can then be either added to the list box by clicking the "Add" button or directly checked by clicking the "Check" button. Before doing that assure whether you are in the proper frame ("Add LTL Formula") of the bottom part of the LTL viewer.
The LTL model checker can be started for an LTL formula by performing a double-click on the respective formula or typing "Enter" after selecting the respective formula. Each LTL formula in the list box has on the left hand side a symbol that indicates what the status of the respective formula is. An LTL formula can have one of the following statuses (status symbols may differ under different operating systems):
All formulas can be checked by "Assertions -> Check All Assertions" in the menu bar. All formulas will be then checked from top to bottom in the list box.
Additionally, the viewer provides a context menu for the list box elements. The context menu can be popped-up by a right-mouse-click on a formula from the list box, and it performs a set of actions available to be performed on the currently selected formula (see Figure below).
The old LTL and CTL dialogs can be accessed from "OldLtlViewers" in the menu bar.
There is a set of options coming with the LTL model checker. In this section we give a brief overview of the preferences. The LTL preferences can be viewed by selecting "LTL Preferences" in the "Preferences" menu of the LTL/CTL Assertions Viewer.
Exploring new states
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 computed). 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 counterexample or to assure the absence of a counterexample. If there's still the possibility of a counterexample in the remaining unexplored state space, the user will get a message.
Optimizing the process of LTL model checking
The process of model checking can be optimized for B and Event-B models by using partial order reduction. The idea of partial order reduction is to execute only a subset of all enabled actions in each state. Thus, only a part of the original state space is checked for the checked property. The reduction of the state space depends on the number of concurrent and independent actions in the model, as well as on the property being checked.
Search Options
The model checker searches for a counterexample (i.e. a path that does not satisfy the current formula). Where the checked paths through the model's search space start depend on the following options in the LTL Preferences’ menu:
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.
ProB supports LTL[e], an extended version of LTL. In contrast to the standard LTL, LTL[e] provides also support for propositions on transitions, not only on states. In practice, writing propositions on transitions is allowed by using the constructs `e(...)` and `[...]`. (see below). The LTL model checker of ProB supports Past-LTL[e] as well.
Fairness is a notion where the search for counterexamples is restricted to paths that do not ignore infinitely the execution of a set of enabled operations imposed by the user as "fair" constraints. One possibility to set fairness constraints in ProB is to encode them in the LTL[e] formula intended to be checked. For example, for a given LTL[e] formula "f" a set of weak fairness conditions {a1,…,an} can be given as follows:
(FG e(a1) => GF [a1]) & … & (FG e(an) => GF [an]) => f.
In a similar way, strong fairness constraints can be imposed expressed by means of an LTL[e] formula:
(GF e(a1) => GF [a1]) & … & (GF e(an) => GF [an]) => f.
Checking fairness in this way is very often considered to be inefficient as usually the number of atoms (the possible valuations of the property) of the LTL property is exponential in the size of the formula.[1] For this reason, the search algorithm of the LTL model checker has been extended in order to allow fairness to be checked efficiently. In addition, new operators have been added to the ProB’s LTL parser for setting fairness constraints to an LTL[e] property. The new operators are WF(-) and SF(-) and both accept as argument an operation. The fairness constraints must be given by means of implication: "fair => f", where "f" is the property to be checked and "fair" the fairness constraints.
In particular, "fair" can have one of the forms: "wfair", "sfair", "wfair & sfair", and "sfair & wfair", where "wfair" and "sfair" represent the imposed weak and strong fairness constraints, respectively.
Basically, "wfair" and "sfair" are expressed by means of logical formulas having the following syntax:
For instance, if we want to check an LTL property "f" on paths that are weak fair in regard to the operations "a" and "b" and additionally strong fair in regard to "c" or "d", then this can be given as follows:
(WF(a) & WF(b)) & (SF(c) or SF(d)) => f
Note that the operators WF(-) and SF(-) cannot appear on the right side of the fairness implication. Basically, WF(-) and SF(-) can be described by the following equivalences:
WF(a) ≡ (FG e(a) => GF [a]) and SF(a) ≡ (GF e(a) => GF [a]), where a is an operation.
Storing LTL formulas in B machines
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. In case there is more than one LTL assertion given in the ‘DEFINITIONS’ section, the particular LTL assertions must be separated by semicolon. For example:
DEFINITIONS ASSERT_LTL == "G (e(SetCruiseSpeed) => e(CruiseBecomesNotAllowed))"; ASSERT_LTL1 == "G (e(CruiseBecomesNotAllowed) => e(SetCruiseSpeed))"; ASSERT_LTL2 == "G (e(CruiseBecomesNotAllowed) => (ObstacleDisappears))"
Storing LTL formulas in CSP-M specifications
LTL formulas can be stored within pragmas in CSP-M specifications. A pragma in which a single LTL formula is stored has the form "{-# assert_ltl "f" "c" #-}", where "assert_ltl" indicates the type of the information stored in the pragma (there are currently two types: assert_ltl and assert_ctl), and is followed by the LTL formula f and a comment (the comment is optional). Both, the LTL formula and the comment, must be enclosed in double quotes.
It is also possible to give several LTL formulas in a single pragma within which the particular LTL assertions are separated by semicolon. For example:
{-# assert_ltl "SF(enter.1) & WF(req.1) => GF([enter.1])"; assert_ltl "SF(enter.2) & WF(req.2) => GF([enter.2])"; assert_ltl "GF [enter.1] & GF [enter.2]" "Should fail."#-}
Note that a semicolon must not follow the last assertion in a pragma.
With the command line version of ProB it is possible to check several LTL[e] 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.
A brief tutorial on visualizing LTL counter-examples in the Rodin tool can be found here.