Download The Meaning and Implementation of SKIP in CSP

10
T. Gibson-Robinson and M. Goldsmith / The Meaning and Implementation of SKIP
P = Q R:
failures s (Q R)
= {(hi, X) | (hi, X) ∈ failures s (Q) ∩ failures s (R)}
∪ {(tr, X) | (tr, X) ∈ failures s (Q)
∪ failures s (R), tr 6= hi}
∪ {(hi, X) | X ⊆ Στr ∧ hXi ∈ traces(Q) ∪ traces(R)}
= {(hi, X) | (hi, X) ∈ failures r (Sig(Q) \ {τr })
∩ failures r (Sig(R) \ {τr })}
∪ {(tr, X) | (tr, X) ∈ failures r (Sig(Q) \ {τr })
∪ failures r (Sig(R) \ {τr }), tr 6= hi}
∪ {(hi, X) | X ⊆ Στr ∧ hXi ∈ traces(Sig(Q) \ {τr })
∪ traces(Sig(R) \ {τr })}
hIH, Theorem 2.4i
= {(hi, X) | tr 6= hi ∧ ∃ tr ∈ {τr }∗ ·
(tr, X ∪ {τr }) ∈ failures r (Sig(Q))
∩ failures r (Sig(R))}
∪ {(tr, X) | ∃ tr0 · tr0 |` ΣX = tr
∧ (tr0 , X ∪ {τr }) ∈ failures r (Sig(Q))
∪ failures r (Sig(R))}
∪ {(hi, X) | X ⊆ Στr ∧ hτr , Xi ∈ traces(Sig(Q))
∪ traces(Sig(R)}
hLemma 2.2i
∗
= {(hi, X) | ∃ tr ∈ {τr } ·
(tr, X ∪ {τr }) ∈ failures r (Sig(Q))
∩ failures r (Sig(R))}
∪ {(tr |` ΣX , X) | (tr, X ∪ {τr }) ∈ failures r (Sig(Q))
∪ failures r (Sig(R)) ∧ tr 6= hi}
h†i
= {(tr |` ΣX , X) | (tr, X ∪ {τr }) ∈ failures r (Sig(Q) (R))}
= failures r ((Sig(Q) Sig(R)) \ {τr })
= failures r (Sig(Q R) \ {τr })
We can prove that the step marked † holds by proving the following equivalence:
{(tr, X) | tr 6= hi ∧ ∃ tr0 · tr0 |` ΣX = tr ∧
(tr0 , X ∪ {τr }) ∈ failures r (Sig(Q)) ∪ failures r (Sig(R))}
∪ {(hi, X) | X ⊆ Στr ∧ hτr , Xi ∈ traces(Sig(Q)) ∪ traces(Sig(R))}
= {(tr |` ΣX , X) | (tr, X ∪ {τr }) ∈ failures r (Sig(Q)) ∪ failures r (Sig(R))
∧ tr 6= hi}
Firstly, suppose (tr, X) is a member of the left-hand equation. Then, if (tr, X) is a
member of the first clause, tr 6= hi and there exists tr0 such that tr0 |` ΣX = tr and