An FDR2 CSP script file can include statements making assertions about refinement properties. These statements will typically have the following form
assert Abstract [X= Concrete
where Abstract
and Concrete
are processes, and `X'
indicates the type of comparison: `T' for traces, `F' for
failures, or `FD' for failures-divergences.
When such a script file is loaded, any assertions of this form are
listed in the FDR2 main window.
Initially, each such assertion is marked as unexplored, using a question
mark symbol.
An assertion can be selected by clicking on it with Mouse-1. The currently selected assertion can be submitted for testing by choosing the Run option from the Assert menu. FDR2 will then attempt to prove the conjecture by compiling, normalising and checking the refinement (see 1.2 The CSP View of the World). While a test is in progress, the assertion will be marked with a clock symbol, to indicate that FDR2 is busy.
When a test finishes or is stopped by the interrupt button, the symbol associated with the assertion will be updated to reflect the result:
When a check has been completed, either a tick or cross will be displayed. If this symbol has a small dot next to it, then counter-examples are available and the check may be sensibly debugged.
The FDR2 debugger can be invoked on the result by double-clicking on it, or by selecting the assertion and choosing Debug from the Assert menu. This will open a new window allowing the behaviour of the processes involved to be examined. The FDR2 process debugger is described in detail below (see 2.9 The FDR2 Process Debugger). An assertion can be re-checked after termination (with different options, for example) by selecting the Run command from the same menu.
Alternatively, assertions can be run or debugged using a pop-up menu which is invoked by clicking on the assertion with Mouse-3 (usually the right mouse button).
In addition to the conjectures made about process refinements in the CSP script, the assertion list will also record other postulates made by the user in the course of an FDR2 session using the buttons in a tab pane (see 2.6 The Tab Pane).
(It is possible to debug an assertion which does not display the small blob, but it is not productive since the underlying check was successful and the behaviour of none of the components is relevant.)
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.