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.

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).