Sequential Composition represents a process which executes argument processes sequentially. The Sequential Composition can be described by seq form, which has the following format:
(seq P Q R) behaves as follows: Firstly it behaves as the process P. If P
terminates successfully, it shifts to the process Q and behaves as Q. If Q
terminates successfully, it also shifts to the process R and behaves as R.
Finally, If R terminates successfully, it means (seq P Q R) terminates
- If P terminates, (seq P Q R) can be said to shift to (seq Q R).
- If P stops, (seq P Q R) also stops. In this case, neither Q nor R is executed.
- (seq P) is the same as P.
- (seq) is the same as SKIP.
An Example of Sequential Composition
We define process S which is a sequential composition of processes P and Q.
(seq P Q))
(alt (! a SKIP) (! b STOP)))
(! c SKIP))
- Firstly the process P is executed. If the event a occurs, P terminates
since P shifts to SKIP. At this time, the tick event generated by P through
SKIP is translated to the internal event tau. This means that the termination
of P occurs inside the process S and it cannot be observed from the outside of
the process S. If the tick could have been observed from the outside of the
process S, it would mean that the process S itself had terminated.
- If the event b occurs, P stops. In this case, S also stops and Q is not
- The process Q terminates after generating the event c. Since the process Q
is the last process of the seq expression, it also means the termination of
the process S.
29 July, 2013