INIT(Q, s) = _{R} P.R^{I} ? ini (E, Q, s, n) → SKIP
SEND = (P.E? dat (e) → Q.P^{O}! dat (e) → s := dat (e))

(P.E? req → _{R} R.P ! new → Q.P^{O}! req (R) → s := req (R))

ACK =

case t of ok ⇒ P.Q^{I} ? ack → t := ack
| ack ⇒ E.P ! ack → s, t := ok, ok

ACS(R)

=

case t of  ok ⇒ P.R? acs (F) → t := acs (F)
| acs (F) ⇒ E.P ! acs (F) → s, t := ok, ok
RECV(Q) = (P.Q^{I} ? dat (e) → s := dat (e))  (P.Q^{I} ? req (R) → s := req (R))

DAT(e)

=

case t of ok ⇒ E.P ! dat (e) → t := dat
| dat ⇒ P.E? ack → Q.P^{O}! ack → s, t := ok, ok

REQ(R)

=

case t of  ok ⇒ E.P ! req → t := req
|  req ⇒ P.E? acs (F) → t := acs (F)
| acs (F) ⇒ F.P ! mov (R) → s, t := ok, ok

Figure 1: “Subroutines” of the port process.

1 The Port Process

The state of a port involves three variables E: name of C-channel end associated with this port. Q: name of port currently attached to the other end of E. s: state of port vis a vis communications in progess. Additionally, R, S and T are local variables holding port names, F is a local variable holding a channel end name, and e is a local variable which holds a data value.

2 The Channel End Processes

The state of a channel end involves a variable P —the port the channel end is currently attached to. If E is the name of the output end of a channel

MOVE = _{Q} E.Q? mov (R) → P.E! mov (R) → P := R; E
E = MOVE

(E.U ? dat (e) → P.E! dat (e) → E.P ? ack → U.E! ack → E) (E.U ? req → P.E! req → E.P ? acs (F) → U.E! acs (F) → E)

SEED(F) = E, s, t, n := F, ok, ok, 0;

Q := (case F of in (C) ⇒ init (out (C)) | out (C) ⇒ init (in (C)))

NEW = _{R} P.R? new → (INIT(Q, s)

S(P.S^{I} ? chg (Q, n′) → INIT(Q′, s); P.S^{O}! chg (P, n) → SKIP) S(RECV(S) → INIT(Q, s′); n := n + 1)); R.P ! acs (E) → t := ok

BEGIN = SEED(init^{−1}(P)) <| init^{−1}(P) ≠ null> | NEW

OUTPUT =

case s of  ok ⇒ SEND; n := n + 1
| dat (e) ⇒ ACK
| req (R) ⇒ ACS(R)

INPUT =

case s of  ok ⇒ RECV(Q); n := n + 1
| dat (e) ⇒ DAT(e)
| req (T) ⇒ REQ(R)
END = P.E? mov (S) → Q.P^{O}! chg (S, n) →

((RECV(Q); n := n + 1; P.Q^{I} ? chg (T, n′) → Q := T) (P.Q^{I} ? chg (T, n′) → ((RECV(Q); n := n + 1) <| n′ ≠ n> | SKIP); Q := T)); S.P^{O}! ini (E, Q, s, n) → (case s, t of req (R), tacs(F) ⇒ F.P ! mov (R) → STOP | ⇒ STOP)

P = BEGIN; ∗( \begin{matrix}(P.Q^{I} ? chg (R, n′) → Q.P^{O}! chg (P, n) → Q := R) \\ (case E of in (C) ⇒ INPUT | out (C) ⇒ OUTPUT) \\ END ) \end{matrix}

Figure 2: Implementation of an individual port.

If E is the name of the input end of a channel

E = MOVE
(E.P ? dat (e) →
(MOVE U.E! dat (e) → E.U ? ack → P.E! ack → E))
(E.P ? req →
(MOVE U.E! req → E.U ? acs (F) → P.E! acs (F) → E))

with MOVE defined as above.

3 External interface of the port system.

Some definitions:

A useful function on event sequences (the content of the first mov message from E appearing in s, or init if there is no such message):

port (E)(s) = (if r = ⟨⟩ then init (E) else (case message (r_{0}) of mov (P) ⇒ P))

where r = s ↓ Alph mov port (E)

The specification that only one channel end owns a particular port at any time:

True (P)(tr) = ∀E : Ends · ∀F : Ends ·
(port (E)(\overline{tr}) = P ∧ port (F)(\overline{tr}) = P) ⇒ E = F

The specification that a channel end always communicates with “its own” port:

Faithful (E)(tr) = (s = ⟨⟩ ∨
channel (s_{0}) = port (E)(s′).E ∨ channel (s_{0}) = E.port (E)(s′))
where s = \overline{tr} ↓ Alph end (E)

Introduce

Prefix^{∗}(T)(tr) = ∃s : T^{∗} · tr < ˆ / s

where T is a set of event sequences. This asserts that tr is a prefix of some concatenation of the sequences in T. Now introduce the specifications

Good end (E)(tr) = Prefix^{∗}(Seq end (E))(tr ↓ Alph end (E))
Good chan (C)(tr) = Prefix^{∗}(Seq chan (C))(tr ↓ Alph chan (C))
Good transf (E)(tr) = Prefix^{∗}(Seq transf (E))(tr ↓ Alph transf (E))
Good mov (E)(tr) = Prefix^{∗}(Seq mov (E))(tr ↓ Alph mov (E))
Good excl (E)(tr) = Prefix^{∗}(Seq excl (E))(tr ↓ Alph excl (E))

and

Ante (tr) = ∀E : Ends · Good mov (E)(tr) ∧ Good excl (E)(tr)
Vtrace (tr) = Ante (tr) ∧

(∀E : Ends · Good end (E)(tr) ∧ Good transf (E)(tr) ∧ Faithful (E)(tr)) ∧ (∀C : Channels · Good chan (C)(tr)) ∧ (∀P : Ports · True (P)(tr))

Finally, an attempt at a specification of the external interface of the port system:

Ante (tr) ⇒ (Vtrace (tr) ∧ ∀c · Vtrace (⟨c⟩ ˆ tr) ⇒ c ∉ ref)

Seq mov port (E) = {⟨P.E.mov (Q)⟩ | P ∈ Ports ∧ Q ∈ Ports}
Seq dat out (E) = {⟨P.E.dat (e), E.P.ack⟩ | P ∈ Ports ∧ e ∈ Values}
Seq req out (E) = {⟨P.E.req , E.P.acs (F)⟩ | P ∈ Ports ∧ F ∈ Ends}
Seq dat in (E) = {⟨E.P.dat (e), P.E.mov(Q)⟩ | P ∈ Ports ∧ Q ∈ Ports} ∪

{⟨E.P.dat (e), P.E.ack⟩ | P ∈ Ports ∧ e ∈ Values}

Seq req in (E) = {⟨E.P.req , P.E.mov(Q)⟩ | P ∈ Ports ∧ Q ∈ Ports}

{⟨E.P.req , P.E.acs (F)⟩ | P ∈ Ports ∧ F ∈ Ends}

Seq end (E) = Seq mov port (E) ∪
case E of out (C) ⇒ (Seq dat out (E) ∪ Seq req out (E))
| in (C) ⇒ (Seq dat in (E) ∪ Seq req in (E))
Seq transf (E) = {⟨P.in (C).acs (E), E.Q.mov (R), S.E.mov (R′), out (C).T.acs (E)⟩ |

{P, Q, R, R′, S, T } ⊂ Ports ∧ C ∈ Channels}

Seq dat com (C) = {⟨P.out (C).dat (e)⟩ ˆ a ˆ

⟨in (C).Q.dat (e), Q.in (C).ack, out (C).P.ack⟩ | {P, Q} ⊂ Ports ∧ e ∈ Values ∧ a ∈ A(e)^{∗}} where A(e) = {in(C).R.dat (e) | R ∈ Ports}

Seq req com (C) = {⟨P.out (C).req ⟩ ˆ a ˆ

⟨in (C).Q.req , Q.in (C).acs (F), out (C).P.acs (F)⟩ | {P, Q} ⊂ Ports ∧ F ∈ Ends ∧ a ∈ A^{∗}} where A = {in(C).R.req | R ∈ Ports}

Seq chan (C) = Seq dat com (C) ∪ Seq req com (C)
Seq mov (E) = {⟨E.Q.mov (R), P.E.mov (R)⟩ | {P, Q, R} ⊂ Ports}
Seq excl (E) = {⟨P.in (C).acs (E), out (C).Q.acs (E)⟩ | {P, Q} ⊂ Ports ∧ C ∈ Channels} ∪
case E of out (C) ⇒ (Seq dat out (E) ∪ Seq req out (E))
| in (C) ⇒ ∅

Figure 3: Some sub-sequences of the port system traces.

Alph mov end (E) = {E.P.mov (Q) | P ∈ Ports ∧ Q ∈ Ports}
Alph mov port (E) = {P.E.mov (Q) | P ∈ Ports ∧ Q ∈ Ports}
Alph dat out (E) = {P.E.dat (e) | P ∈ Ports ∧ e ∈ Values} ∪ {E.P.ack | P ∈ Ports}
Alph req out (E) = {P.E.req | P ∈ Ports} ∪ {E.P.acs (F) | P ∈ Ports ∧ F ∈ Ends}
Alph dat in (E) = {E.P.dat (e) | P ∈ Ports ∧ e ∈ Values} ∪ {P.E.ack | P ∈ Ports}
Alph req in (E) = {E.P.req | P ∈ Ports} ∪ {P.E.acs (F) | P ∈ Ports ∧ F ∈ Ends}
Alph out (E) = Alph dat out (E) ∪ Alph req out (E)
Alph in (E) = Alph dat in (E) ∪ Alph req in (E)
Alph end (E) = Alph mov port (E) ∪

(case E of out (C) ⇒ Alph out (E) | in (C) ⇒ Alph in (E))

Alph mov (E) = Alph mov end (E) ∪ Alph mov port (E)
Alph acs (E) = {P.in (C).acs (E) | P ∈ Ports ∧ C ∈ Channels} ∪

{out (C).P.acs (E) | P ∈ Ports ∧ C ∈ Channels}

Alph transf (E) = Alph mov (E) ∪ Alph acs (E)
Alph excl (E) = Alph acs (E) ∪ (case E of out (C) ⇒ Alph out (E) | in (C) ⇒ ∅)
Alph chan (C) = Alph out (out (C)) ∪ Alph in (in (C))

Figure 4: Some sub-sets of the port system alphabet.