2.9 The FDR2 Process Debugger

When a completed check is selected for debugging, FDR2 creates a new window containing information about the counterexamples (if any) which were found in the course of the check. This debugger view consists of three areas:

Menu Bar

As in the main window, the menu bar contains headings describing groups of commands for manipulating or querying the debugger. At present these headings include File commands (for closing the window), and the Help menu.

Process Behaviour Viewer

The largest portion of the debugger view is devoted to this display, which shows the structure of a particular process together with its contribution to a particular counterexample. Where more than one process or rôle are involved in a check (e.g., in a comparison between a specification and an implementation), the individual processes can be selected by the "file tabs" across the top of this region.

The following sections describe the facilities offered by the debugger.

• Debugger menu commands
• Viewing process behaviours

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