Machine Structure Viewer¶

The machine structure viewer provides a way of viewing FDR’s internal representation of a CSP process. This takes the form of a tree of processes, where the leaves are simple processes, and the internal vertices (i.e. non-leaf nodes) correspond to processes composed of others. For example, if Dining Philosophers is loaded, then typing :structure SYSTEM' into the prompt would show the following window:

This indicates that the process SYSTEM' is composed of two subprocesses, PHILS and FORKS. Further, PHILS is composed of 6 subprocesses, each of the form sbisim(PHIL(i)) (i.e. sbisim applied to PHIL(i)). This viewer can be a useful tool for checking that a process has been defined correctly, and for investigating how FDR has represented the process in order to diagnose any performance problems. It is also a useful tool for investigating the effectiveness of compression, since it is capable of displaying the number of states both before and after compression.

In general, there are three different types of nodes that will appears in the tree. Exactly which node will appear depends on how FDR internally decides to represent a process.

• High-level machine nodes: these correspond to individual CSP operators, such as Alphabetised Parallel and Hide, that are applied to any number of subprocesses (depending on the operator). In this case, the node will display the number of formats and rules, which can be a useful indicator of the complexity of a machine (the more formats and rules, the more complex the machine).
• Low-level machine nodes: these will generally correspond to simple recursive CSP processes which FDR decides to compile into a single labelled-transition system, and thus these nodes are not divisible. The number of states and transitions is given.
• Compressed machines: these will appear wherever a compression function, such as normal or sbisim, is applied. This will indicate how many states and transitions the compression managed to save. This data is used to estimate the total number of states and transitions that compression saved.

The right-hand pane displays information about the selected process. For example, if PHILS is selected, the information pane displays the following:

This shows information about what CSP operator the process represents (if the node is a non-leaf node), the alphabet of the process (i.e. the set of events it can perform), and the list of processes that are leaf processes underneath this vertex (if the node is not a leaf itself).