;;; Integrity for U_{T,E,alpha} with alpha=0 and no P_safe 
;;; (with N processes, two values)
;;;  Elena - Apr. 23, 2018


PARAMETER_DECLARATIONS 1
N


INTEGER_VARIABLES_DECLARATIONS 1
round


ARITHMETIC_ARRAY_DECLARATIONS 3
R0
R1
R2


; three values: 0, 1, or 2 for the '?'; 1 is default value
ENUMERATED_ARRAY_DECLARATIONS 3
X 2
V 3
D 3


COUNTER_DECLARATIONS 6
zd1 : (= D[x] 1)
zx0 : (= X[x] 0)
zx1 : (= X[x] 1)
zv0 : (= V[x] 0)
zv1 : (= V[x] 1)
zv2 : (= V[x] 2)


ARITHMETIC_ASSERTION
true


TRANSITION_CASES 8

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

; T1  --  received > N/2 messages carrying 0
CASE
 (= round 0) (>= R0[x] 0) (<= R0[x] zx0) (>= R1[x] 0) (<= R1[x] zx1) (> (* 2 R0[x]) N)   (= roundp 1)
(= Xp[x] X[x]) (= Vp[x] 0) (= Dp[x] D[x])
 

; T2  --  received > N/2 messages carrying 1
CASE
 (= round 0) (>= R0[x] 0) (<= R0[x] zx0) (>= R1[x] 0) (<= R1[x] zx1) (> (* 2 R1[x]) N)   (= roundp 1)
(= Xp[x] X[x]) (= Vp[x] 1) (= Dp[x] D[x])
 

; T3  --  no value supported by > N/2 messages (also no msg received)
CASE
 (= round 0) (>= R0[x] 0) (<= R0[x] zx0) (>= R1[x] 0) (<= R1[x] zx1) (<= (* 2 R0[x]) N) (<= (* 2 R1[x]) N)   (= roundp 1)
(= Xp[x] X[x]) (= Vp[x] V[x]) (= Dp[x] D[x])
 
 
;;; round r=2 phi --> count received votes

; T4  --  majority of votes for 0; take it as new value and decide!
CASE
 (= round 1) (>= R0[x] 0) (<= R0[x] zv0) (>= R1[x] 0) (<= R1[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (> (* 2 R0[x]) N)   (= roundp 0)
(= Xp[x] 0) (= Vp[x] 2) (= Dp[x] 0)


; T5  --  majority of votes for 1; take it as new value and decide!
CASE
 (= round 1) (>= R0[x] 0) (<= R0[x] zv0) (>= R1[x] 0) (<= R1[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (> (* 2 R1[x]) N)   (= roundp 0)
(= Xp[x] 1) (= Vp[x] 2) (= Dp[x] 1)


; T6  --  at least 1 vote for 0 but not majority; may take it but not decide
CASE
 (= round 1) (>= R0[x] 0) (<= R0[x] zv0) (>= R1[x] 0) (<= R1[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (> R0[x] 0) (<= (* 2 R0[x]) N)   (= roundp 0)
(= Xp[x] 0) (= Vp[x] 2) (= Dp[x] D[x])


; T7  --  at least 1 vote for 1 but not majority; may take it but not decide
CASE
 (= round 1) (>= R0[x] 0) (<= R0[x] zv0) (>= R1[x] 0) (<= R1[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (> R1[x] 0) (<= (* 2 R1[x]) N)   (= roundp 0)
(= Xp[x] 1) (= Vp[x] 2) (= Dp[x] D[x])


; T8  --  received just '?' votes or no msg at all; take default value (1) and do not decide
CASE
 (= round 1) (>= R0[x] 0) (<= R0[x] zv0) (>= R1[x] 0) (<= R1[x] zv1) (>= R2[x] 0) (<= R2[x] zv2) (= R0[x] 0) (= R1[x] 0)   (= roundp 0)
(= Xp[x] 1) (= Vp[x] 2) (= Dp[x] D[x])


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


UNSAFE_CONDITION
(> zd1 0)