| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
When FDR is started, it displays a window of the form shown in Figure 3. This is made up of five components arranged vertically.
Figure 3: Main Window
At the top of the window, the menu bar includes headings describing groups of related commands. To pop up the menu related to a heading, click with Mouse-1 (usually the left mouse button). Alternatively, hold down the Alt (or Meta) key and type the character which is underlined in the heading. This area also includes the Interrupt button which stops the current check or compilation and prepares FDR to act immediately on further commands.
The second portion of the window is a strip containing tabs for the different kinds of checks that FDR can perform. There is also a tab for interaction with the compiler and evaluation of arbitrary expressions.
The middle part of the main window is used enter information relevant to the currently selected tab. This can be for building up refinement statements or for evaluating expressions. In the case of a simple refinement, two process selectors define the specification and implementation rôlesin the check, and the type of refinement relation can also be varied. (Of course, for deadlock, livelock and determinism checks only one process needs to be selected, and this area contains a single selector.) Once selected, a check can be added to the list of assertions or checked immediately.
Perhaps the most important part of the main window lies below the tab pane: the assertion list contains the assertions made about process refinement, deadlock- or livelock-freedom, or other model properties. For each statement, FDR shows whether it is true, false, or untested. When a file is loaded, the assertion list contains any refinement properties stated in the script file. Properties are added to this list when the an enquiry is made by the user.
Assertions displayed in this list can be tested, and if false, the FDR process debugger can be invoked on the counterexamples generated.
Below the list of assertions, FDR displays a list of all the processes defined in the currently loaded script (and also any functions which could return process results if provided with suitable arguments). Processes selected from this list can be used as the specification or implementation parts of a refinement check, or tested for a variety of intrinsic properties.
| [ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] |
This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.