Download Heaps and Hops

3.3. Contracts
A non-trimmed contract is one in which there are control states that are “disconnected”
from the rest of the control states. Any non-trimmed contract may be turned into a trimmed
one with the same operational meaning simply by deleting those states.
Lemma 3.5 For every deterministic trimmed contract C, C is half-duplex if and only if it
is positional.
Proof The reverse implication is already proved by Lemma 3.4. Let us prove the direct
implication.
Let us notice first that in the dialogue system associated to a trimmed contract C =
(Σ, Q, q0 , F, T ), ⟨q, q, ␣, ␣⟩ is always reachable. Indeed q ∈ Q is reachable in the oriented graph formed using Q as vertices and T as edges, so there is a sequence of transitions
(q0 , τ1 , q1 ), . . . , (qn−1 , τn , q) from q0 to q . The following execution is thus valid, where
τ ′ = τ for sending actions and τ ′ = τ̄ for receiving ones:
τ1′
τ¯1′
τn′
τ¯n′
⟨q0 , q0 , ␣, ␣⟩ Ð→ ⋅ Ð→ ⟨q1 , q1 , ␣, ␣⟩⋯⟨qn−1 , qn−1 , ␣, ␣⟩ Ð→ ⋅ Ð→ ⟨q, q, ␣, ␣⟩
Suppose that C is not positional. There is q ∈ Q and a1 , a2 , q1 and q2 such that
(q, !a1 , q1 ), (q, ?a2 , q2 ) ∈ T . Since ⟨q, q, ␣, ␣⟩ is reachable, the following execution is
valid:
1!a1
2!a2
⟨q0 , q0 , ␣, ␣⟩ →∗ ⟨q, q, ␣, ␣⟩ ÐÐ→ ⟨q1 , q, a1 , λ⟩ ÐÐ→ ⟨q1 , q2 , a1 , a2 ⟩
This execution is not half-duplex.
◻
Even trimmed half-duplex contracts are not necessarily deterministic. For instance, the
following contracts are not deterministic but half-duplex nonetheless:
?b
!a
!a
q1
q1
.
.
q
q
q′
q2
q2
!a
!a
?b
Deterministic and positional contracts have more properties than
just being half-duplex: they are fault and deadlock-free. Before proving this claim, let us
show that we cannot say the same of non-deterministic or non-positional contracts. For
instance, the following non-deterministic contract is not fault-free:
Fault-free contracts
!a
q1
!b
q.0
q2
!a
q1′
!b′
The first machine can send a, then b, while the dual one receives a and then tries to
receive b′ whereas b is available. Non-positional contracts also embed a form of choice
that can harm the safety properties, since in a non-positional state both machines may make
dissonant moves.
56