;;; Integrity for Uniform Voting 
;;; (with N processes, no resilience, two values)
;;;  Elena - Apr. 18, 2018


PARAMETER_DECLARATIONS 1
N


INTEGER_VARIABLES_DECLARATIONS 2
round
dec


; three values: 0, 1, or 2 for the '?'
ARITHMETIC_ARRAY_DECLARATIONS 4
R00
R02
R11
R12


ENUMERATED_ARRAY_DECLARATIONS 3
X 2
V 3
D 3


COUNTER_DECLARATIONS 8
zd0 : (= D[x] 0)
zd1 : (= D[x] 1)
zx0 : (= X[x] 0)
zx1 : (= X[x] 1)
z00 : (= X[x] 0) (= V[x] 0)
z02 : (= X[x] 0) (= V[x] 2) 
z11 : (= X[x] 1) (= V[x] 1)
z12 : (= X[x] 1) (= V[x] 2)


ARITHMETIC_ASSERTION
true


TRANSITION_CASES 15

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

; T1  --  minimum received value is 0 and no 1 received
CASE
 (= round 0) (>= R00[x] 0) (<= R00[x] zx0) (>= R11[x] 0) (<= R11[x] zx1) (> R00[x] 0) (= R11[x] 0)   (= roundp 1) (= decp dec)
(= Xp[x] 0) (= Vp[x] 0) (= Dp[x] D[x])
 

; T2  --  minimum received value is 1 and no 0 received
CASE
 (= round 0) (>= R00[x] 0) (<= R00[x] zx0) (>= R11[x] 0) (<= R11[x] zx1) (= R00[x] 0) (> R11[x] 0)   (= roundp 1) (= decp dec)
(= Xp[x] 1) (= Vp[x] 1) (= Dp[x] D[x])
 

; T3  --  minimum received value is 0 but also 1 received
CASE
 (= round 0) (>= R00[x] 0) (<= R00[x] zx0) (>= R11[x] 0) (<= R11[x] zx1) (> R00[x] 0) (> R11[x] 0)   (= roundp 1) (= decp dec)
(= Xp[x] 0) (= Vp[x] V[x]) (= Dp[x] D[x])
 
 
; T4  --  no value received; nothing changes
CASE
 (= round 0) (>= R00[x] 0) (<= R00[x] zx0) (>= R11[x] 0) (<= R11[x] zx1) (= R00[x] 0) (= R11[x] 0)   (= roundp 1) (= decp dec)
(= Xp[x] X[x]) (= Vp[x] V[x]) (= Dp[x] D[x])


;;; round r=2 phi --> count received couples

; T5  --  all votes for 0; decide for 0 and not decided before
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R00[x] 0) (= (+ R02[x] R11[x] R12[x]) 0)   (= roundp 0) (= decp dec)
(= D[x] 2)   (= Xp[x] 0) (= Vp[x] 2) (= Dp[x] 0)


; T6  --  all votes for 0; decide for 0 and already decided for 0 before
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R00[x] 0) (= (+ R02[x] R11[x] R12[x]) 0)   (= roundp 0) (= decp dec)
(= D[x] 0)   (= Xp[x] 0) (= Vp[x] 2) (= Dp[x] 0)


; T7  --  all votes for 0; decide for 0 and already decided for 1 before!
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R00[x] 0) (= (+ R02[x] R11[x] R12[x]) 0)   (= roundp 0) (= decp 1)
(= D[x] 1)   (= Xp[x] 0) (= Vp[x] 2) (= Dp[x] 0)


; T8  --  all votes for 1; decide for 1 and not decided before
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R11[x] 0) (= (+ R12[x] R00[x] R02[x]) 0)   (= roundp 0) (= decp dec)
(= D[x] 2)   (= Xp[x] 1) (= Vp[x] 2) (= Dp[x] 1)


; T9  --  all votes for 1; decide for 1 and already decided for 1 before
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R11[x] 0) (= (+ R12[x] R00[x] R02[x]) 0)   (= roundp 0) (= decp dec)
(= D[x] 1)   (= Xp[x] 1) (= Vp[x] 2) (= Dp[x] 1)


; T10  --  all votes for 1; decide for 1 and already decided for 0 before!
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R11[x] 0) (= (+ R12[x] R00[x] R02[x]) 0)   (= roundp 0) (= decp 1)
(= D[x] 0)   (= Xp[x] 1) (= Vp[x] 2) (= Dp[x] 1)


; T11  --  some but not all votes for 0; may nondeterministically take it
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R00[x] 0) (< R00[x] (+ R00[x] R02[x] R11[x] R12[x]) )   (= roundp 0) (= decp dec)
(= Xp[x] 0) (= Vp[x] 2) (= Dp[x] D[x])


; T12  --  some but not all votes for 1; may nondeterministically take it
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R11[x] 0) (< R11[x] (+ R11[x] R12[x] R00[x] R02[x]) )   (= roundp 0) (= decp dec)
(= Xp[x] 1) (= Vp[x] 2) (= Dp[x] D[x])


; T13  --  no votes but some 0 value
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R02[x] 0) (= (+ R11[x] R00[x]) 0)   (= roundp 0) (= decp dec)
(= Xp[x] 0) (= Vp[x] 2) (= Dp[x] D[x])


; T14  --  no votes and no 0 value but some 1 value
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (> R12[x] 0) (= (+ R00[x] R11[x] R02[x]) 0)   (= roundp 0) (= decp dec)
(= Xp[x] 1) (= Vp[x] 2) (= Dp[x] D[x])


; T15 -- else nothing changes
CASE
 (= round 1) (>= R00[x] 0) (<= R00[x] z00) (>= R02[x] 0) (<= R02[x] z02) (>= R11[x] 0) (<= R11[x] z11) (>= R12[x] 0) (<= R12[x] z12) (= (+ R00[x] R11[x] R02[x] R12[x]) 0)   (= roundp 0) (= decp dec)
(= Xp[x] X[x]) (= Vp[x] 2) (= Dp[x] D[x]) 


INITIALIZATION
 (= round 0) (= dec 0)
 (= V[x] 2) (= D[x] 2)


UNSAFE_CONDITION
(> dec 0)