1 The Port-Handler Process

A port may be “initialised” or “uninitialised”. An initialised port is associated from the outset with some channel end out (C) or in (C). It has a partner initialised port, associated with the opposite channel end. An uninitialised port is bound to a channel end when it receives an ini message.

The alphabet of the port handling process associated with P contains main control thread events

{(P, )^{I}.ini , ( , P)^{O}.ini },

repointing events

{(P, )^{I}.chg , ( , P)^{O}.quo , ( , P)^{O}.chg , (P, )^{I}.quo },

and communication events

{( , P)^{O}.mes }.

For the time being, mes inputs are omitted from the alphabet of the port handler.

The traces of the process satisfy the following predicates:

1. (Channel end association). Suppose we have a port handler associated with an initialised port P bound to channel end E. The trace of this process restricted to ini input events and mes , chg , quo and ini outputs, is a prefix of a sequence consisting of an arbitrary string of events from {( , P)^{O}.mes (E, ), ( , P)^{O}.quo (E, )} concatentated with a final sequence from {⟨( , P)^{O}.chg (E, , ), ( , P)^{O}.ini (E, , )⟩}.

For an uninitialised port, the similarly restricted trace is a prefix of a sequence consisting of an initial event from {(P, )^{I}.ini (E, , )}, for some E, followed by a sequence from the set described in the previous paragraph (with E fixed through the subsequent life of the port).

2. (Repointing thread). The trace of the port handler restricted to repointing events and ini outputs is a prefix of a sequence from built from an arbitrary concatenation of sequences from {⟨(P, Q^{−}′)^{I}.chg , (Q^{−}′, P)^{O}.quo ⟩}, followed by one sequence from

{⟨( , P)^{O}.chg ( , P^{+}′, ), (P, )^{I}.quo , (P^{+}′, P)^{O}.ini ⟩,
⟨( , P)^{O}.chg ( , P^{+}′, ), (P, )^{I}.chg , (P^{+}′, P)^{O}.ini ⟩}.

3. (Partner port association). In any event from

{(Q, P)^{O}.mes , (Q, P)^{O}.chg , ( , P)^{O}.ini ( , Q, )}

appearing in a trace, the Q field must have the same value as the Q field in the most recent preceding event of type (P, )^{I}.chg ( , Q, ). If there is no preceding chg input, the Q field must match either the initial value for the partner port (if P is initialised), or the value in the trace’s compulsory (P, )^{I}.ini ( , Q, ) event (if it is uninitialised).

These three predicates are a complete specification of the traces of the port process—the process can engage in any event sequence allowed by them. Together with the requirement the process be deterministic, they completely define the process ^{1}.

1.1 Transition model for predicate 1

The state space of the model is

S^{1} = α_{0} | α_{1} of Ends | α_{2} of Ends | α_{3}

The alphabet of the model is

A_{P}^{1} = {(P, )^{I}.ini , .P^{O}.ini , ( , P)^{O}.mes , ( , P)^{O}.quo , ( , P)^{O}.chg }

Its transition function is

T_{P}^{1} (α_{0}) = {((P, )^{I}.ini (E′, , ) ↦ α_{1}(E′))}
T_{P}^{1} (α_{1}(E)) = {(( , P)^{O}.quo (E, ) ↦ α_{1}(E)),
(( , P)^{O}.mes (E, ) ↦ α_{1}(E)),
(( , P)^{O}.chg (E, , ) ↦ α_{2}(E))}
T_{P}^{1} (α_{2}(E)) = {(( , P)^{O}.ini (E, , ) ↦ α_{3})}
T_{P}^{1} (α_{3}) = {}

If P is an initialised port bound to E, the initial state is α_{1}(E); if it’s an uninitialised port the initial state is α_{0}.

1.2 Transition model for predicate 2

The state space of the model is

S^{2} = β_{0} | β′_{0} of Ports | β_{1} of Ports | β_{2} of Ports | β_{3}

1The predicates have been expressed in English, with just a few elementary ideas, like restriction, prefix and concatenation. I’m not aware of a widely used formal notation that would capture these specifications very concisely. Rather than invent a new notation here, I’ll stick with English for a “declarative” style of specification, and immediately introduce state transition models for the three predicates, which can be referred to if the English is too ambiguous.

The alphabet of the model is

A_{P}^{2} = {(P, )^{I}.chg , ( , P)^{O}.quo , ( , P)^{O}.chg , (P, )^{I}.quo , ( , P)^{O}.ini }.

Its transition function is

T_{P}^{2} (β_{0}) = {((P, Q^{−}′)^{I}.chg ↦ β′_{0}(Q^{−}′)),
(( , P)^{O}.chg ( , P^{+}′, ) ↦ β_{1}(P^{+}′))}
T_{P}^{2} (β′_{0}(Q^{−})) = {((Q^{−}, P)^{O}.quo ↦ β_{0})}
T_{P}^{2} (β_{1}(P^{+})) = {((P, )^{I}.quo ↦ β_{2}(P^{+})),
((P, )^{I}.chg ↦ β_{2}(P^{+}))}
T_{P}^{2} (β_{2}(P^{+})) = {((P^{+}, P)^{O}.ini ↦ β_{3})}
T_{P}^{2} (β_{3}) = {}

The initial state is β_{0}.

1.3 Transition model for predicate 3

The state space of the model is

S^{3} = γ_{0} | γ_{1} of Ports

The alphabet of the model is

A_{P}^{3} = {( , P)^{I}.ini , (P, )^{I}.chg , ( , P)^{O}.mes , ( , P)^{O}.chg , ( , P)^{O}.ini }.

Its transition function is

T_{P}^{3} (γ_{0}) = {((P, )^{I}.chg ( , Q′, ) ↦ γ_{1}(Q′)),
((P, )^{I}.ini ( , Q′, ) ↦ γ_{1}(Q′))}
T_{P}^{3} (γ_{1}(Q)) = {((P, )^{I}.chg ( , Q′, ) ↦ γ_{1}(Q′)),
((P, )^{I}.ini ↦ γ_{1}(Q)),
((Q, P)^{O}.mes ↦ γ_{1}(Q)),
((Q, P)^{O}.chg ↦ γ_{1}(Q)),
(( , P)^{O}.ini ( , Q, ) ↦ γ_{1}(Q))}

If P is an initialised port with original partner Q, the initial state is γ_{1}(Q); if it’s an uninitialised port the initial state is γ_{0}.

The three transition functions are illustrated schematically in figure ??.

Inspection of these models (possibly by reference to the diagrams) should persuade that they respectively generate exactly the sets of traces specified by the original three predicates.

[figure: α_{0}; α_{1}; α_{2}; α_{3}; ? ini; ! chg; ! ini; ! mes; ! quo]
[figure: β_{0}; β′_{0}; β_{1}; β_{2}; β_{3}; ! chg; ! ini; ? chg; ! quo; ? quo; ? chg]
[figure: γ_{0}; γ_{1}; ? ini; ? chg; ? ini; ? chg; ! mes; ! chg; ! ini]

Figure 1: “Predicate” state transition diagrams (schematic)

1.4 The Pstat transition model

The port-handling process is described by the conjunction of the three predicates. Consequently it can be modelled by the composition of the three state transition models just introduced. It’s convenient to introduce an equivalent model based on the state space

Pstat = π_{0} | π′_{0} of Ports × Ports | π_{1} of Ends × Ports | π′_{1} of Ends × Ports × Ports | π_{2} of Ends × Ports × Ports | π_{3} of Ends × Ports × Ports | π_{4}

The alphabet of the model A_{P}^{Pstat} is the full alphabet of the port process, which has been defined earlier. Its transition function is

T_{P}^{Pstat}(π_{0}) = {((P, Q^{−}′)^{I}.chg ( , Q′, ) ↦ π′_{0}(Q′, Q^{−}′)),
((P, )^{I}.ini (E′, Q′, ) ↦ π_{1}(E′, Q′))}
T_{P}^{Pstat}(π′_{0}(Q, Q^{−})) = {((P, )^{I}.ini (E′, Q′, ) ↦ (π′_{1}(E′, Q, Q^{−}))}
T_{P}^{Pstat}(π_{1}(E, Q)) = {((Q, P)^{O}.mes (E, ) ↦ π_{1}(E, Q)),

((P, Q^{−}′)^{I}.chg ( , Q′, ) ↦ π′_{1}(E, Q′, Q^{−}′)),

((Q, P)^{O}.chg (E, P^{+}′, ) ↦ π_{2}(E, Q, P^{+}′))}

T_{P}^{Pstat}(π′_{1}(E, Q, Q^{−})) = {((Q, P)^{O}.mes (E, ) ↦ π′_{1}(E, Q, Q^{−})),
((Q^{−}, P)^{O}.quo (E, ) ↦ π_{1}(E, Q))}
T_{P}^{Pstat}(π_{2}(E, Q, P^{+})) = {((P, )^{I}.quo ↦ π_{3}(E, Q, P^{+})),
((P, )^{I}.chg ( , Q′, ) ↦ π_{3}(E, Q′, P^{+}))}
T_{P}^{Pstat}(π_{3}(E, Q, P^{+})) = {((P^{+}, P)^{O}.ini (E, Q, ) ↦ π_{4})}
T_{P}^{Pstat}(π_{4}) = {}

If P is an initialised port bound to E, the initial state is π_{1}(E, Q); if it’s an uninitialised port the initial state is π_{0}.

The equivalence between the set of traces defined by this model and that defined by the composition of the three previous models is formally established by the bisimulation:

\begin{matrix}\{(π_{0} & ↦ & (α_{0}, β_{0}, γ_{0})) \\ (π′_{0}(Q, Q^{−}) & ↦ & (α_{0}, β′_{0}(Q^{−}), γ_{1}(Q))) \\ (π_{1}(E, Q) & ↦ & (α_{1}(E), β_{0}, γ_{1}(Q))) \\ (π′_{1}(E, Q, Q^{−}) & ↦ & (α_{1}(E), β′_{0}(Q^{−}), γ_{1}(Q))) \\ (π_{2}(E, Q, P^{+}) & ↦ & (α_{2}(E), β_{1}(P^{+}), γ_{1}(Q))) \\ (π_{3}(E, Q, P^{+}) & ↦ & (α_{2}(E), β_{2}(P^{+}), γ_{1}(Q))) \\ (π_{4} & ↦ & (α_{3}, β_{3}, γ_{1}( )))\} \end{matrix}

[figure: π_{0}; π′_{0}; π_{1}; π′_{1}; π_{2}; π_{3}; π_{4}; ? ini; ? chg; ? ini; ! chg; ! ini; ? chg; ! quo; ! mes; ! mes; ? quo; ? chg]

Figure 2: Pstat transition diagram (schematic)

(Proof that this relation is a bisimulation is omitted. It follows by straightforward application of the rule for composition of transition models).