;;; (Weak) Validity for EDAC algorithm with crash failures, |V|=2
;;; (with N processes, at most t<N faulty)
;;; Silvio & Elena - June 6, 2018


PARAMETER_DECLARATIONS 3
N
t
f


; cnum (crash number) abstracts the vector containing the id's of crashed processes 
INTEGER_VARIABLES_DECLARATIONS 2
round
cnum


; R0/R1 msgs with values; D0/D1 msgs with "decide" directive
ARITHMETIC_ARRAY_DECLARATIONS 5
R0
R1
R2
D0
D1


; W: {0} / {1} / {0,1} (=2) ; DE (decision): 0 / 1 / undefined (=2)
; DN (done): boolean + 2 (= halt)
; F: 1=correct; 0=going to crash; 2=crashed
ENUMERATED_ARRAY_DECLARATIONS 4
W  3
DN 3
DE 3
F  3


COUNTER_DECLARATIONS 14
zv0 : (= DN[x] 0) (= W[x] 0) (= F[x] 1)
zv1 : (= DN[x] 0) (= W[x] 1) (= F[x] 1)
zv2 : (= DN[x] 0) (= W[x] 2) (= F[x] 1)
zc0 : (= DN[x] 0) (= W[x] 0) (= F[x] 0)
zc1 : (= DN[x] 0) (= W[x] 1) (= F[x] 0)
zc2 : (= DN[x] 0) (= W[x] 2) (= F[x] 0)
zdv0 : (= DN[x] 1) (= DE[x] 0) (= F[x] 1)
zdv1 : (= DN[x] 1) (= DE[x] 1) (= F[x] 1)
zdc0 : (= DN[x] 1) (= DE[x] 0) (= F[x] 0)
zdc1 : (= DN[x] 1) (= DE[x] 1) (= F[x] 0)
zd0 : (= DE[x] 0) (= F[x] 1) 
zf0 : (= F[x] 0)
zf1 : (= F[x] 1)
zf2 : (= F[x] 2)


ARITHMETIC_ASSERTION
 (> N t) (>= t f) (>= f 0) (<= (+ zf0 zf2) f) (<= cnum (+ zf0 zf2))


TRANSITION_CASES 12

; T1 -- undecided process receives decision for 0
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (= cnump cnum) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (> D0[x] 0)
(= DE[x] 2) (= DEp[x] 0) (= Wp[x] W[x]) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) )  (or (and (= DN[x] 0) (= DNp[x] 1)) (and (= DN[x] 1) (= DNp[x] 2)) (and (= DN[x] 2) (= DNp[x] 2)))


; T2 -- undecided process receives decision for 1
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (= cnump cnum) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (> D1[x] 0)
(= DE[x] 2) (= DEp[x] 1) (= Wp[x] W[x]) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) )  (or (and (= DN[x] 0) (= DNp[x] 1)) (and (= DN[x] 1) (= DNp[x] 2)) (and (= DN[x] 2) (= DNp[x] 2)))


; T3  --  undecided process with 0 receives only 0's and sees new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (= R1[x] 0) (= R2[x] 0)  (> N (+ R0[x] cnum)) (= N (+ cnump R0[x])) 
(= W[x] 0) (= DE[x] 2)  (= Wp[x] 0) (= DEp[x] DE[x]) (= DNp[x] DN[x]) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T4  --  undecided process with 0 receives only 0's and doesn't see new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (= R1[x] 0) (= R2[x] 0)  (= N (+ R0[x] cnum)) (= cnump cnum)
(= W[x] 0) (= DE[x] 2)  (= Wp[x] 0) (= DEp[x] 0) (= DNp[x] 1) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T5  --  undecided process with 0 receives 1's and sees new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (> (+ R1[x] R2[x]) 0)  (> N (+ R0[x] R1[x] R2[x] cnum)) (= N (+ cnump R0[x] R1[x] R2[x]))
(= W[x] 0) (= DE[x] 2)  (= Wp[x] 2) (= DEp[x] DE[x]) (= DNp[x] DN[x]) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T6  --  undecided process with 0 receives 1's and doesn't see new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (> (+ R1[x] R2[x]) 0)  (= N (+ R0[x] R1[x] R2[x] cnum)) (= cnump cnum)
(= W[x] 0) (= DE[x] 2)  (= Wp[x] 2) (= DEp[x] 0) (= DNp[x] 1) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T7  --  undecided process with 1 receives only 1's and sees new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (= R0[x] 0) (= R2[x] 0)  (> N (+ R1[x] cnum)) (= N (+ cnump R1[x]))
(= W[x] 1) (= DE[x] 2)  (= Wp[x] 1) (= DEp[x] DE[x]) (= DNp[x] DN[x]) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T8  --  undecided process with 1 receives only 1's and doesn't see new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (= R0[x] 0) (= R2[x] 0)  (= N (+ R1[x] cnum)) (= cnump cnum) 
(= W[x] 1) (= DE[x] 2)  (= Wp[x] 1) (= DEp[x] 1) (= DNp[x] 1) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T9  --  undecided process with 1 receives 0's and sees new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (> (+ R0[x] R2[x]) 0)  (> N (+ R0[x] R1[x] R2[x] cnum)) (= N (+ cnump R0[x] R1[x] R2[x]))
(= W[x] 1) (= DE[x] 2)  (= Wp[x] 2) (= DEp[x] DE[x]) (= DNp[x] DN[x]) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T10  --  undecided process with 1 receives 0's and doesn't see new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (> (+ R0[x] R2[x]) 0)  (= N (+ R0[x] R1[x] R2[x] cnum)) (= cnump cnum) 
(= W[x] 1) (= DE[x] 2)  (= Wp[x] 2) (= DEp[x] 0) (= DNp[x] 1) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T11 --  undecided process with {0,1} receives something and sees new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (> N (+ R0[x] R1[x] R2[x] cnum)) (= N (+ cnump R0[x] R1[x] R2[x]))
(= W[x] 2) (= DE[x] 2)  (= Wp[x] 2) (= DEp[x] DE[x]) (= DNp[x] DN[x]) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 


; T12 --  undecided process with {0,1} receives something and doesn't see new crashes
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= D0[x] zdv0) (<= D0[x] (+ zdv0 zdc0)) (>= D1[x] zdv1) (<= D1[x] (+ zdv1 zdc1)) (>= R0[x] zv0) (<= R0[x] (+ zv0 zc0)) (>= R1[x] zv1) (<= R1[x] (+ zv1 zc1)) (<= R2[x] zv2) (>= R2[x] (+ zv2 zc2)) (= D0[x] 0) (= D1[x] 0) (= N (+ R0[x] R1[x] R2[x] cnum)) (= cnump cnum) 
(= W[x] 2) (= DE[x] 2)  (= Wp[x] 2) (= DEp[x] 0) (= DNp[x] 1) (=> (= F[x] 0) (= Fp[x] 2)) (or (and (= F[x] 1) (= Fp[x] 0)) (= F[x] Fp[x]) ) 



; each process has initial value 1 and has not decided
INITIALIZATION
 (= round 0) (= zf1 N) (= cnum 0)
 (= DE[x] 2) (= W[x] 1) (= DN[x] 0)


UNSAFE_CONDITION
(> zd0 0) (= round (+ f 2))