| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The middle portion of the FDR 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:
The check is added to the assertion list and immediately run.
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 section The Assertion List).
Clicking this button clears any process selectors, ready for a new definition to be selected or typed.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] |
This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.