2.5 The Process List

The list of processes which is displayed by FDR2 when a file is loaded serves two main purposes: it allows the user to select processes for insertion into a tab pane, and it also allows the user to invoke a variety of tests on intrinsic properties of processes.

The entries in the list consist of the name of each process or function which way return a process, followed by the number of arguments required by the function, if any.

Selection in this window follows the same pattern as in the assertion list: Mouse-1 selects the current process, and Mouse-3 invokes a pop-up menu of commands which can be activated on the process under the cursor. The currently selected process may be transferred to the tab pane by clicking one of the arrow buttons, or used in any of the following commands from the Process menu:

Deadlock

Tests to determine whether the process can reach a state in which no further action is possible. If a deadlock can occur, a trace leading to deadlock will be available to the debugger.

Livelock

Tests to determine if a process can reach a series of states in which endless internal action is possible without any external events taking place (CSP divergence or internal chatter). If such a sequence is found, it will again be accessible through the debugger (which will allow examination of the details of the internal actions involved).

Deterministic

This command tests to determine if the process is deterministic; i.e., if the set of actions possible at any stage is always uniquely determined by the previous history of visible actions. A process will fail to be deterministic in this CSP sense if either it can diverge (livelock), or if it is possible for a given action to be allowed after a given trace of visible events and also possible that it could be refused after the same trace. In this latter case, the debugger will present two behaviours of the same process as a counterexample; one leading to the possible event, and one leading to its refusal.

Graph

This option is currently experimental and available only if the environment variable FDRGRAPH is set. It produces a graph of the selected process which can be manipulated (states can be rearranged) and printed.

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