2.9 The FDR Process Debugger

When a completed check is selected for debugging, FDR 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ôleare 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.

2.9.1 Debugger menu commands

The current release of FDR supports only a few simple commands on the debugger view menu bar:

File

This contains a Close command, which causes the debugger window to be closed. (The save option is intended for testing purposes only.)

Help

Gives access to the on-line help facility described (see section On-line Help).

2.9.2 Viewing process behaviours

The behaviour viewer is organised as a series of pages indexed by numbered tabs, one for each process relevant to the currently selected counterexample (see Figure 6 in Debugging). For any particular counterexample, the system maintains a record of the processes involved. If the property being checked was intrinsic, like deadlock- or livelock- freedom, there is only a single process involved. In the case of a refinement check, there will be two processes, a specification and an implementation. In this case, FDR will display the behaviour of the implementation by default (labelled with tab 1), but we can choose to view information about the specification by clicking the alternative “file tab” (labelled 0).

Each page thus represents a single process and its involvement in a particular behaviour. This information is represented in two parts: a hierarchical view of the structure of the process, and a series of windows showing the contribution of a selected part of the process to the overall behaviour.

2.9.2.1 The process structure

The process structure is represented as a tree similar in form to a standard organisation diagram or program structure chart. The root node (at the top of the tree) represents the process as a whole, and is initially shown alone, with no further detail. Any leaf node for which more information is available can be expanded by double-clicking with Mouse-1; double-clicking a node which is currently expanded will cause that part of the tree to be “folded up”.

When a leaf node is expanded, branches are added according to the number of sub-components of the node in question. Thus, a node labelled with a parallel composition symbol ‘[|..|]’ will expand to have two children representing the sub-processes which are combined in parallel. Each child will be associated with its own contribution to the overall erroneous behaviour being examined(6).

If any of the compression or factorisation operators (see section Using Compressions) were applied in building up a system, the process of extracting the back-trace information may involve further refinement checks and thus significant computation. To indicate this, nodes of the process structure corresponding to compressed processes will be coloured red, and will not be expanded by default. Examining their internal behaviour is still straightforward, however: simply double click on the coloured node.

(Note: some lesser-used CSP constructions, such has the repetition operator ^*of [Hoare85], have a single syntactic sub-component which may be responsible for more than one independent sub-behaviour. In this case, the process tree will contain a branch for each independent behaviour. There are currently no operators which involve both multiple processes and multiple behaviours!)

2.9.2.2 The behaviour information

When exploring the process structure view, any node in the tree can be selected by a single click with Mouse-1. Information about the currently selected node is displayed in the area to the right of the window. The exact information displayed will depend on the nature of the counterexample being examined and the contribution made to it by the selected component. In general, the following types of information may be displayed:

• An erroneous trace, ending in a prohibited event. This will be flagged Allows, and will be displayed as a scrollable list. By default, internal actions (events) will be included, but these can be hidden by toggling the Show tau option button displayed at the bottom of the list.
• A non-erroneous trace, perhaps leading to an error elsewhere but not in itself illegal. This will be labelled Performs, and can be manipulated as for an erroneous trace.
• An illegal acceptance or refusal. This information can be expressed either as an acceptance set (which will be smaller than the specification permits) or as a refusal larger than any legal maximum. To switch between these views, click on the Acc. (acceptances) or Ref. (refusals) button displayed below the set. In some cases, information will be available on which behaviours the specification was willing to permit. To display this, click on the Allowed… button; the information will be displayed in a pop-up window.
• Divergence. If a process diverges illegally, this will be stated.
• Repetition of visible events. In the course of decomposing a divergent behaviour (e.g., through a hiding operator), we may discover a series of visible events which can be repeated endlessly, and which are all concealed from the ultimate environment. This sequence will be labelled with the word Repeats and will be displayed in the same manner as the other traces discussed above.

Typically the following information will be displayed for each type of counterexample behaviour:

Successful refinement

(or no relevant behaviour): no information displayed.

No direct contribution

a non-erroneous trace.

Refusal/acceptance failure

a non-erroneous trace, plus the illegal refusal/acceptance.

Divergence

the trace leading to divergence.

Divergence (internally)

the trace leading to divergence, plus a trace of repeated events.

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.