477 (Brock-Ackerman) The following picture shows a network of communicating processes.
b a
d
The formal description of this network is
chan a, b, c· a! 0 || choose || (c?. b! c)
Formally define choose , add transit time, and state the output message and time if
(a) choose either reads from a and then outputs a 0 on c and d , or reads from b and then outputs a 1 on c and d . The choice is made freely.
§ We define choose as follows:
choose = (a?. (c! 0 || d! 0)) ∨ (b?. (c! 1 || d! 1))
Now we calculate.
chan a, b, c· a! 0 || choose || (c?. b! c)
= ∃𝓜a, 𝓣a, 𝓻a, 𝓻aʹ, 𝔀a, 𝔀aʹ, 𝓜b, 𝓣b, 𝓻b, 𝓻bʹ, 𝔀b, 𝔀bʹ, 𝓜c, 𝓣c, 𝓻c, 𝓻cʹ,𝔀c,𝔀cʹ· (∀i,j·i≤j ⇒ t≤𝓣ai ≤𝓣aj ≤tʹ∧ t≤𝓣bi ≤𝓣bj ≤tʹ ∧ t≤𝓣ci ≤𝓣cj ≤tʹ)
∧ 𝓻a=𝔀a=𝓻b=𝔀b=𝓻c=𝔀c=0
∧ (𝓜a𝔀a=0 ∧ 𝓣a𝔀a=t ∧ (𝔀a:= 𝔀a+1)
a! 0
choose
c?. b!c
|| (
t:= max t (𝓣a𝓻a + 1). 𝓻a:= 𝓻a+1.
( 𝓜c𝔀c=0 ∧ 𝓣c𝔀c=t ∧ (𝔀c:= 𝔀c+1)
|| 𝓜d𝔀d=0 ∧ 𝓣d𝔀d=t ∧ (𝔀d:= 𝔀d+1) ) )
|| (
|| 𝓜d𝔀d=1 ∧ 𝓣d𝔀d=t ∧ (𝔀d:= 𝔀d+1) ) ) t:= max t (𝓣c𝓻c + 1). 𝓻c:= 𝓻c+1. 𝓜b𝔀b=𝓜c𝓻c–1 ∧ 𝓣b𝔀b=t ∧ (𝔀b:= 𝔀b+1) ) )
Except for time, all processes in independent compositions change different variables, so || is easily replaced by conjunction. Also, make all substitutions indicated by assignments.
c
∨( t:= max t (𝓣b𝓻b + 1). 𝓻b:= 𝓻b+1.
( 𝓜c𝔀c=1 ∧ 𝓣c𝔀c=t ∧ (𝔀c:= 𝔀c+1)
= ∃𝓜a, 𝓣a, 𝓻a, 𝓻aʹ, 𝔀a, 𝔀aʹ, 𝓜b, 𝓣b, 𝓻b, 𝓻bʹ, 𝔀b, 𝔀bʹ, 𝓜c, 𝓣c, 𝓻c, 𝓻cʹ,𝔀c,𝔀cʹ· (∀i,j·i≤j ⇒ t≤𝓣ai ≤𝓣aj ≤tʹ∧ t≤𝓣bi ≤𝓣bj ≤tʹ ∧ t≤𝓣ci ≤𝓣cj ≤tʹ)
∧ ∧
𝓻a=𝔀a=𝓻b=𝔀b=𝓻c=𝔀c=0 ∃ta, tc, tb·
ta=𝓣a0=t ∧ 𝓜a0=0 ∧ 𝔀aʹ=1
∧ ( tc = 𝓣c0 = 𝓣d𝔀d = 𝓣a0 + 1 ∧ 𝓻aʹ=𝔀cʹ=1 ∧ 𝓜c0=𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1
∨ tc = 𝓣c0 = 𝓣d𝔀d = 𝓣b0+1 ∧ 𝓻bʹ=𝔀cʹ=1 ∧ 𝓜c0=𝓜d𝔀d=1 ∧ 𝔀dʹ=𝔀d+1)
∧ tb = 𝓣b0 = 𝓣c0 + 1 ∧ 𝓻cʹ=𝔀bʹ=1 ∧ 𝓜b0=𝓜c0
∧ tʹ = MAX [ta; tc; tb] use One-Point laws to eliminate most quantifiers
= ∃tc, tb·
( tc = 𝓣d𝔀d = t+1 ∧ 𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1
∨ tc = 𝓣d𝔀d = tb + 1 ∧ 𝓜d𝔀d=1 ∧ 𝔀dʹ=𝔀d+1 )
∧ tb = tc+1
∧ tʹ = MAX [t; tc; tb] move the conjunctions into the disjunction
= ∃tc, tb·
tc=𝓣d𝔀d=t+1 ∧ 𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1 ∧ tb=tc+1 ∧ tʹ=MAX[t;tc;tb] ∨ tc=𝓣d𝔀d=tb+1 ∧ 𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1 ∧ tb=tc+1 ∧ tʹ=MAX[t;tc;tb] now we can eliminate tc and tb in each disjunct separately
= 𝓣d𝔀d=t+1 ∧ 𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1 ∧ tʹ=t+2 ∨ 𝓣d𝔀d=∞ ∧ 𝓜d𝔀d=1 ∧ 𝔀dʹ=𝔀d+1 ∧ tʹ=∞
= (t:= t+1. d! 0. t:= t+1) ∨ (t:= ∞. d! 1)
Either a 0 is output after time 1 or nothing ever happens. There is probably a better way to do this question by using laws of programs and not translating to ordinary logic.
(b) as in part (a), choose either reads from a and then outputs a 0 on c and d , or reads from b and then outputs a 1 on c and d . But this time the choice is not made freely; choose reads from the channel whose input is available first (if there’s a tie, then take either one).
§ We define choose as follows:
choose = (√a ∨ 𝓣ara≤𝓣brb) ∧ (a?. (c! 0 || d! 0))
∨ (√b ∨ 𝓣brb≤𝓣ara) ∧ (b?. (c! 1 || d! 1)) Now we calculate.
chan a, b, c· a! 0 || choose || (c?. b! c)
= ∃𝓜a, 𝓣a, 𝓻a, 𝓻aʹ, 𝔀a, 𝔀aʹ, 𝓜b, 𝓣b, 𝓻b, 𝓻bʹ, 𝔀b, 𝔀bʹ, 𝓜c, 𝓣c, 𝓻c, 𝓻cʹ,𝔀c,𝔀cʹ· (∀i,j·i≤j ⇒ t≤𝓣ai ≤𝓣aj ≤tʹ∧ t≤𝓣bi ≤𝓣bj ≤tʹ ∧ t≤𝓣ci ≤𝓣cj ≤tʹ)
∧ 𝓻a=𝔀a=𝓻b=𝔀b=𝓻c=𝔀c=0
∧ ( ||
||
𝓜a𝔀a=0 ∧ 𝓣a𝔀a=t ∧ (𝔀a:= 𝔀a+1)
( (
∨ (
(𝓣a𝓻a≤t ∨ 𝓣a𝓻a≤𝓣b𝓻b)
∧ (t:= max t (𝓣a𝓻a + 1). 𝓻a:= 𝓻a+1.
( 𝓜c𝔀c=0 ∧ 𝓣c𝔀c=t ∧ (𝔀c:= 𝔀c+1)
|| 𝓜d𝔀d=0 ∧ 𝓣d𝔀d=t ∧ (𝔀d:= 𝔀d+1) ) ) ) (𝓣b𝓻b≤t ∨ 𝓣b𝓻b≤𝓣a𝓻a)
∧ (t:= max t (𝓣b𝓻b + 1). 𝓻b:= 𝓻b+1.
( 𝓜c𝔀c=1 ∧ 𝓣c𝔀c=t ∧ (𝔀c:= 𝔀c+1)
|| 𝓜d𝔀d=1 ∧ 𝓣d𝔀d=t ∧ (𝔀d:= 𝔀d+1) ) ) ) )
( t:= max t (𝓣c𝓻c + 1). 𝓻c:= 𝓻c+1. 𝓜b𝔀b=𝓜c𝓻c–1 ∧ 𝓣b𝔀b=t ∧ (𝔀b:= 𝔀b+1) ) )
Except for time, all processes in independent compositions change different variables, so || is easily replaced by conjunction. Also, make all substitutions indicated by assignments.
= ∃𝓜a, 𝓣a, 𝓻a, 𝓻aʹ, 𝔀a, 𝔀aʹ, 𝓜b, 𝓣b, 𝓻b, 𝓻bʹ, 𝔀b, 𝔀bʹ, 𝓜c, 𝓣c, 𝓻c, 𝓻cʹ,𝔀c,𝔀cʹ· (∀i,j·i≤j ⇒ t≤𝓣ai ≤𝓣aj ≤tʹ∧ t≤𝓣bi ≤𝓣bj ≤tʹ ∧ t≤𝓣ci ≤𝓣cj ≤tʹ)
∧ 𝓻a=𝔀a=𝓻b=𝔀b=𝓻c=𝔀c=0 ∧ ∃ta, tc, tb·
ta=𝓣a0=t ∧ 𝓜a0=0 ∧ 𝔀aʹ=1
∧ ( (𝓣a0≤t ∨ 𝓣a0≤𝓣b0)
∧ tc=𝓣c0=𝓣d𝔀d=𝓣a0+1 ∧ 𝓻aʹ=𝔀cʹ=1 ∧ 𝓜c0=𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1 ∨ (𝓣b0≤t ∨ 𝓣b0≤𝓣a0)
∧ tc=𝓣c0=𝓣d𝔀d=𝓣b0+1 ∧ 𝓻bʹ=𝔀cʹ=1 ∧ 𝓜c0=𝓜d𝔀d=1 ∧ 𝔀dʹ=𝔀d+1)
∧ tb = 𝓣b0 = 𝓣c0 + 1 ∧ 𝓻cʹ=𝔀bʹ=1 ∧ 𝓜b0=𝓜c0
∧ tʹ = MAX [ta; tc; tb] use the One-Point laws to eliminate most quantifiers
= ∃tc, tb·
( (t≤t ∨ t≤tb) ∧ tc = 𝓣d𝔀d = t+1 ∧ 𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1
∨ (tb≤t ∨ tb≤t) ∧ tc = 𝓣d𝔀d = tb+1 ∧ 𝓜d𝔀d=1 ∧ 𝔀dʹ=𝔀d+1 )
∧ tb = tc+1
∧ tʹ = MAX [t; tc; tb] simplify the two minor disjunctions
and move the conjunctions into the major disjunction
= ∃tc, tc·
tc=𝓣d𝔀d=t+1 ∧ 𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1 ∧tb=tc+1∧tʹ=MAX[t;tc;tb]
∨ tb≤t ∧ tc=𝓣d𝔀d=tb+1 ∧ 𝓜d𝔀d=1 ∧ 𝔀dʹ=𝔀d+1 ∧ tb = tc+1 ∧ tʹ=MAX[t;tc;tb] now we can eliminate tc and tb in each disjunct separately
= 𝓣d𝔀d=t+1 ∧ 𝓜d𝔀d=0 ∧ 𝔀dʹ=𝔀d+1 ∧ tʹ=t+2 ∨ ∞≤t ∧ 𝓣d𝔀d=∞ ∧ 𝓜d𝔀d=1 ∧ 𝔀dʹ=𝔀d+1 ∧ tʹ=∞
= (t:= t+1. d! 0. t:= t+1) ∨ t=tʹ=∞ ∧ (d! 1)
If the computation starts before time ∞ the output is definitely 0 after time 1 . Again, there is probably a better way to do this question by using laws of programs and not translating to ordinary logic.