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 3.2.3 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, FDR2 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.
Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.