Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.


2.6 The Tab Pane

The middle portion of the FDR2 main window allows the user to assemble and check properties of processes defined by the model without adding explicit assertions to the file.(5)

For each possible check, it consists of a number of components: selectors allowing processes to be chosen; a selector for the CSP refinement relation (i.e., the semantic model used), and a set of buttons for managing these assertions.

The process selectors operate identically: each consists of a title and three elements: a selection button (the arrow symbol), a text field and a pull-down list. Each of these may be used to modify the process definition displayed in the text field:

Additionally, these the text entries can be emptied by clicking the Clear button at the bottom of the process selector.

The semantic model to be used for a check can be changed by clicking Mouse-1 on the Model button of the tab pane; FDR2 will display a list of alternative models which can be selected with Mouse-1. The choice of models may be constrained by the check under construction: deadlock and determinism checks cannot be performed in the traces model, and divergence checks must be performed in the failures-divergences model.

Three command buttons complete the tab pane. These allow checks to be recorded and tested as follows:

Check
The check is added to the assertion list and immediately run.

Add
This causes a check to be added to the assertion list as above, but the check is not immediately started; it may be run later using any of the mechanisms described above (see 2.4 The Assertion List).

Clear
Clicking this button clears any process selectors, ready for a new definition to be selected or typed.


Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.