2.1 The Main Window

When FDR2 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

Menu Bar

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 FDR2 to act immediately on further commands.

Tab Bar

The second portion of the window is a strip containing tabs for the different kinds of checks that FDR2 can perform. There is also a tab for interaction with the compiler and evaluation of arbitrary expressions.

Tab Pane

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ôles in 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.

Assertion List

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, FDR2 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 FDR2 process debugger can be invoked on the counterexamples generated.

Process List

Below the list of assertions, FDR2 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.

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