C.2 Processes

In the following, E ranges over FSP process expressions, Q ranges over process identifiers, and A, B range over sets of observable actions (i.e. A L and B L).

Process Definition:

 Q = E means that lts(Q) =_def lts(E).

Process Constants:

 lts(END) = <{e}, {τ}, {}, e> where e ∈ES lts(STOP) = <{s}, {τ}, {}, s> lts(ERROR) = Π

Prefix ->:

If lts(E) = < S, A, Δ, q > and E is not ERROR

 then lts(a -> E) = < S ∪ {p}, A ∪ {a}, Δ ∪ {(p, a, q)}, p >, where p  S. lts(a -> ERROR) = < {p, π}, {a}, {(p, a, π)}, p >, where p ≠ π.

Choice | :

 Let 1 ≤ i ≤ n, and lts(E_i) = < S_i, A_i, Δ_i, q_i >, then lts(a₁ -> E₁ | ... | a_n -> E_n)          = < S ∪ {p}, A ∪ {a₁ ...a_n}, Δ ∪ {(p, a₁, q₁)...(p, a_n, q_n)}, p >, where . If E_i is ERROR then A_i = {}.

Alphabet Extension + :

 If lts(E) =< S, A, Δ, q >, then lts(E + B) =< S, A ∪ B, Δ, q >.

Recursion:

We represent the FSP process defined by the recursive equation X = E as rec(X = E), where X is a variable in E. For example, the process defined by the recursive definition X = (a -> X) is represented as rec(X =(a -> X)).
We use E[X ← rec(X = E)] to denote the FSP expression that is obtained by substituting rec(X = E) for X in E. Then lts(rec(X = E)) is the smallest LTS that satisfies the following rule:
where “~” is strong semantic equivalence defined in section C.6.1. Mutually recursive equations can be reduced to the simple form described above. For local processes, all occurrences of process variables are guarded by an action prefix and consequently, recursive definitions are guaranteed to have a fixed-point solution.

Sequential Composition:

 If lts(P) = < S_p, A_p, Δ_p, q_p > is terminating with end state e_p ∈ ES and lts(E) = < S_e, A_e, Δ_e, q_e > then lts(P; E) = < S_p ∪ S_e, A_p ∪ A_e, Δ_p ∪ Δ_e, q_p > where q_e = e_p.