;;; Agreement for Coordinated Uniform Voting (without nosplit Property)
;;; (with N processes, no resilience, two values)
;;;  Elena - July 2, 2018


PARAMETER_DECLARATIONS 1
N


INTEGER_VARIABLES_DECLARATIONS 1
round


; three values: 0, 1, or 2 for the '?'
ARITHMETIC_ARRAY_DECLARATIONS 3
R00
R11
R2


; C (coordinator): 0=not done; 1=doing; 2=already done
; V (vote): 2=undefined.  Same for decision D
ENUMERATED_ARRAY_DECLARATIONS 4
X 2
V 3
D 3
C 3


COUNTER_DECLARATIONS 10
zc  : (= C[x] 1)
zd0 : (= D[x] 0)
zd1 : (= D[x] 1)
zc0 : (= X[x] 0) (= C[x] 1)
zc1 : (= X[x] 1) (= C[x] 1)
zx0 : (= X[x] 0)
zx1 : (= X[x] 1)
zv0 : (= V[x] 0)
zv1 : (= V[x] 1) 
zv2 : (= V[x] 2)


ARITHMETIC_ASSERTION
(<= zc 1)


TRANSITION_CASES 12

; T1 -- selection of coordinator
CASE
(= round 0) (= roundp 1)
(= C[x] 0) (= Cp[x] 1) (= Vp[x] V[x]) (= Xp[x] X[x]) (= Dp[x] D[x])


;;; round r=3phi-2 --> count received values (using R00 for 0 and R11 for 1)

; T2  --  received value from coord is 0
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] zc0) (>= R11[x] 0) (<= R11[x] zc1) (> R00[x] 0) (= R11[x] 0)   (= roundp 2)
(= Xp[x] 0) (= Vp[x] V[x]) (= Dp[x] D[x]) (= Cp[x] C[x])


; T3  --  received value from coord is 1
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] zc0) (>= R11[x] 0) (<= R11[x] zc1) (= R00[x] 0) (> R11[x] 0)   (= roundp 2)
(= Xp[x] 1) (= Vp[x] V[x]) (= Dp[x] D[x]) (= Cp[x] C[x])
 

;;; round r=3phi-1 --> determine vote

; T4  --  all received values are 0
CASE
 (= round 2) (>= R00[x] 0) (<= R00[x] zx0) (>= R11[x] 0) (<= R11[x] zx1) (> R00[x] 0) (= R11[x] 0)   (= roundp 3)
(= Xp[x] X[x]) (= Vp[x] 0) (= Dp[x] D[x]) (= Cp[x] C[x])

 
; T5  --  all received values are 1
CASE
 (= round 2) (>= R00[x] 0) (<= R00[x] zx0) (>= R11[x] 0) (<= R11[x] zx1) (= R00[x] 0) (> R11[x] 0)   (= roundp 3)
(= Xp[x] X[x]) (= Vp[x] 1) (= Dp[x] D[x]) (= Cp[x] C[x])

 
; T6  --  received both values
CASE
 (= round 2) (>= R00[x] 0) (<= R00[x] zx0) (>= R11[x] 0) (<= R11[x] zx1) (> R00[x] 0) (> R11[x] 0)   (= roundp 3)
(= Xp[x] X[x]) (= Vp[x] V[x]) (= Dp[x] D[x]) (= Cp[x] C[x])

 
; T7  --  no value received (possibly, just "?"'s received); nothing changes
CASE
 (= round 2) (>= R00[x] 0) (<= R00[x] zx0) (>= R11[x] 0) (<= R11[x] zx1) (= R00[x] 0) (= R11[x] 0)   (= roundp 3)
(= Xp[x] X[x]) (= Vp[x] V[x]) (= Dp[x] D[x]) (= Cp[x] C[x])


;;; round r=3 phi --> count received votes

; T8  --  all votes for 0; decide
CASE
 (= round 3) (>= R00[x] 0) (<= R00[x] zv0) (>= R11[x] 0) (<= R11[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (> R00[x] 0) (= (+ R11[x] R2[x]) 0)   (= roundp 0)
(= Xp[x] 0) (= Vp[x] 2) (= Dp[x] 0) (or (and (= C[x] 1) (= Cp[x] 2)) (= Cp[x] C[x]))


; T9  --  all votes for 1; decide
CASE
 (= round 3) (>= R00[x] 0) (<= R00[x] zv0) (>= R11[x] 0) (<= R11[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (> R11[x] 0) (= (+ R00[x] R2[x]) 0)   (= roundp 0)
(= Xp[x] 1) (= Vp[x] 2) (= Dp[x] 1) (or (and (= C[x] 1) (= Cp[x] 2)) (= Cp[x] C[x]))


; T10  --  some but not all votes for 0; may nondeterministically take it
CASE
 (= round 3) (>= R00[x] 0) (<= R00[x] zv0) (>= R11[x] 0) (<= R11[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (> R00[x] 0) (< R00[x] (+ R00[x] R11[x] R2[x]) )   (= roundp 0)
(= Xp[x] 0) (= Vp[x] 2) (= Dp[x] D[x]) (or (and (= C[x] 1) (= Cp[x] 2)) (= Cp[x] C[x]))


; T11  --  some but not all votes for 1; may nondeterministically take it
CASE
 (= round 3) (>= R00[x] 0) (<= R00[x] zv0) (>= R11[x] 0) (<= R11[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (> R11[x] 0) (< R11[x] (+ R11[x] R00[x] R2[x]) )   (= roundp 0)
(= Xp[x] 1) (= Vp[x] 2) (= Dp[x] D[x]) (or (and (= C[x] 1) (= Cp[x] 2)) (= Cp[x] C[x]))


; T12 -- else nothing changes
CASE
 (= round 3) (>= R00[x] 0) (<= R00[x] zv0) (>= R11[x] 0) (<= R11[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (= (+ R00[x] R11[x]) 0) (>= R2[x] 0)   (= roundp 0)
(= Xp[x] X[x]) (= Vp[x] 2) (= Dp[x] D[x]) (or (and (= C[x] 1) (= Cp[x] 2)) (= Cp[x] C[x]))



; processes start with any value
INITIALIZATION
 (= round 0)
 (= V[x] 2) (= D[x] 2) (= C[x] 0)


; someone decides for 0 and someone for 1
UNSAFE_CONDITION
(> zd0 0) (> zd1 0)