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 removed by clicking 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.

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