1 Deriving the Big Predicate

1.1 User Messages

Q.P^{O}.mes (u, H) Q.P^{I}.mes (u, H)

P = port associated with channel end from (H). Q = port associated with channel end to (H). u = user field transferred in message. H = data transfer half-channel.

mes output is in the alphabets of port P, the user process, and the message delivery system. mes input is in the alphabets of port Q, the user process, and the message delivery system.

1.2 Control Transfer Messages

The ini message is sent from a port process to its successor on termination of the former. It carries information needed to initialise the new port.

P.S^{O}.ini (E, Q, u, H) P.S^{I}.ini (E, Q, u, H)

P = port formerly associated with channel end E. S = successor port to P. E = a channel end. u = user field transferred in message. H = access transfer half-channel.

ini output is in the alphabets of the user process, port P, and the message delivery system. ini input is in the alphabets of the user process, port S, and the message delivery system.

1.3 Port Repointing Messages

These messages are used during transfer of access to a channel end to inform the port associated with the partner channel end of the move. quo is an acknowledgement of a chg message.

Q.P^{O}.chg (E, S, H) Q.P^{I}.chg (E, S, H)

P = port formerly associated with channel end E. Q = port associated with partner of E. S = successor port to P. E = a channel end. H = access transfer half-channel.

chg output is in the alphabets of the user process, port P, and the message delivery system. chg input is in the alphabets of port Q and the message delivery system.

P.Q^{O}.quo (E, H) P.Q^{I}.quo (E, H)

P = port formerly associated with channel end E. Q = port associated with partner of E. E = a channel end. H = access transfer half-channel.

quo output is in the alphabets of port Q, and the message delivery system. quo input is in the alphabets of port P and the message delivery system.

2 The Port Process

A port process 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 a port process 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

Communication events

.P^{O}.mes P. ^{I}.mes

The traces of P satisfy

1. The trace restricted to mes , chg , quo and ini output events, and ini inputs, is a prefix of some sequence from

S(E)

if P is an initialised port, or

⋃_{E}{⟨P. ^{I}.ini (E, , , )⟩}S(E)

if it is uninitialised. Here

S(E) = {⟨ .P^{O}.mes ( , from (E))⟩, ⟨ .P^{O}.quo ⟩}^{N}
{⟨ .P^{O}.chg (E, , ), .P^{O}.ini (E, , , )⟩}

2. The trace restricted to repointing events and ini output is a prefix of a sequence from

{⟨P.Q^{I}.chg (F, , ), Q.P^{O}.quo (F)⟩}^{N} ⋃_{R,H}{⟨ .P^{O}.chg ( , R, H)⟩} {⟨P. ^{I}.quo ⟩, ⟨P. ^{I}.chg ⟩}

{⟨R.P^{O}.ini ( , , , H)⟩}

3. 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 constraints impose that communications are always sent to the active partner port.

(These constraints describe a non-terminating process, because they don’t restrict occurrences of message input.)