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:
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.