2.4 The Assertion List

An FDR 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 FDR 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. FDR will then attempt to prove the conjecture by compiling, normalising and checking the refinement (see section The CSP View of the World). While a test is in progress, the assertion will be marked with a clock symbol, to indicate that FDR 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:

Tick

indicates that the check completed successfully; the stated refinement holds.

Cross

indicates that the check completed, but found one or more counterexamples to the stated property: the refinement does not hold, and the FDR debugger can be used to explore the reasons why.

Exclamation mark

indicates that the check failed to complete for some reason: either a syntax or type error was detected in the scripts, some resource was exhausted while trying to run the check, or the check was interrupted. If a process could not be compiled, FDR will also indicate this by popping up a warning dialogue box. Other error messages, and further information, are available in the status log (see section Options).

Zig-zag

indicates that FDR was unable to complete a check because of a weakness in the currently coded algorithms. (This can occur under rare cirumstances when performing a determinism check in the Failures model.)

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 FDR 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 FDR process debugger is described in detail below (see section The FDR 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 FDR session using the buttons in a tab pane (see section 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.)

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.