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
prompt would show the following
This indicates that the process
SYSTEM' is composed of two subprocesses,
PHILS is composed of 6 subprocesses, each
of the form
sbisim applied to
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.
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).
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
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).