13.1 Sequential Processes

13.1 Sequential Processes

Although abstractly a process always means the same thing, for pragmatic implementation reasons FSP divides processes into three types: local processes that define a state within a primitive process, primitive processes defined by a set of local processes and composite processes that use parallel composition, relabeling and hiding to compose primitive processes. A local process is defined using STOP, ERROR, action prefix and choice. We now extend our definition of processes to include sequential processes.

A sequential process is a process that can terminate. A process can terminate if the local process END is reachable from its start state.

13.1.1 Local Process END

The local process END denotes the state in which a process successfully terminates. A process engages in no further actions after END. In this respect it has the same semantics as STOP. However, STOP denotes a state in which a process has halted prematurely, usually due to communication deadlock. In earlier chapters, to simplify presentation, we used STOP to indicate termination of a process. It would be more precise to replace these uses of STOP with END. With the introduction of a state describing successful termination, the need to use STOP explicitly in process description largely disappears. Figure 13.1 depicts an example of a sequential process together with its LTS, where E is used to denote END.

Figure 13.1: Sequential process BOMB.

13.1.2 Sequential Composition;

If P is a sequential process and Q is a local process, then P;Q represents the sequential composition such that when P terminates, P;Q becomes the process Q.

If we define a process SKIP = END then P;SKIP ≡ P and SKIP;P ≡ P. A sequential composition in FSP always takes the form:

 SP1;SP2;..SPn;LP

where SP1,..,SPn are sequential processes and LP is a local process. A sequential composition can appear anywhere in the definition of a primitive process that a local process reference can appear (for example, processes P123 and LOOP in Figure 13.2).

Figure 13.2: Sequential composition LOOP.

Sequential composition can be used in a recursive context as in Figure 13.3, where process R is defined as the sequential composition of sequential processes R(I) for values of I from 0 to 2 and the local process END when I=3.

Figure 13.3: Sequential composition and recursion.

13.1.3 Parallel Composition and Sequential Processes

The parallel composition SP1||SP2 of two sequential processes SP1 and SP2 terminates when both of these processes terminate. If termination is reachable in SP1||SP2 then it is a sequential process.

Figure 13.4 gives an example of parallel composition of sequential processes. Note that a composite process that terminates can appear in the definition of a primitive process.

Figure 13.4: Parallel composition of sequential processes.

13.1.4 Sequential Processes and Analysis

While a reachable STOP state is a safety violation resulting in the LTSA generating a counter example trace, a reachable END state is not a safety violation. However, a trace to a reachable END state will be generated during progress analysis since the END state violates all progress properties.