;;; Integrity for U_{T,E,alpha} with alpha>0 and P_safe 
;;; alpha := upper bound on number of byzantine messages
;;; P_safe := total number of received (correct) messages is > N/2 + alpha
;;; (with N processes, two values)
;;;  Elena - May 2, 2018


PARAMETER_DECLARATIONS 2
N
alpha


INTEGER_VARIABLES_DECLARATIONS 1
round


; Bij represents byzantine messages with value/vote i from processes owning value/vote j
ARITHMETIC_ARRAY_DECLARATIONS 9
R0
R1
R2
B01
B02
B10
B12
B20
B21


; 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)


; tests performed with (= alpha 1) and with  (>= alpha 1) (< (* 2 alpha) N)
ARITHMETIC_ASSERTION
 (>= alpha 1) (< (* 2 alpha) N)


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] R1[x])) (+ N (* 2 alpha))) (>= B01[x] 0) (<= B01[x] zx1) (>= B10[x] 0) (<= B10[x] zx0) (<= (+ R0[x] B10[x]) zx0) (<= (+ R1[x] B01[x]) zx1) (<= (+ R0[x] R1[x] B10[x] B01[x]) N) (<= (+ B01[x] B10[x]) alpha) (> (* 2 (+ R0[x] B01[x])) (+ N (* 2 alpha)))   (= 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 (+ R0[x] R1[x])) (+ N (* 2 alpha))) (>= B01[x] 0) (<= B01[x] zx1) (>= B10[x] 0) (<= B10[x] zx0) (<= (+ R0[x] B10[x]) zx0) (<= (+ R1[x] B01[x]) zx1) (<= (+ R0[x] R1[x] B10[x] B01[x]) N) (<= (+ B01[x] B10[x]) alpha) (> (* 2 (+ R1[x] B10[x])) (+ N (* 2 alpha)))   (= 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] R1[x])) (+ N (* 2 alpha))) (>= B01[x] 0) (<= B01[x] zx1) (>= B10[x] 0) (<= B10[x] zx0) (<= (+ R0[x] B10[x]) zx0) (<= (+ R1[x] B01[x]) zx1) (<= (+ R0[x] R1[x] B10[x] B01[x]) N) (<= (+ B01[x] B10[x]) alpha) (<= (* 2 (+ R0[x] B01[x])) (+ N (* 2 alpha))) (<= (* 2 (+ R1[x] B10[x])) (+ N (* 2 alpha)))   (= 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] R1[x] R2[x])) (+ N (* 2 alpha))) (>= B01[x] 0) (<= B01[x] zv1) (>= B10[x] 0) (<= B10[x] zv0) (>= B02[x] 0) (<= B02[x] zv2) (>= B20[x] 0) (<= B20[x] zv0) (>= B12[x] 0) (<= B12[x] zv2) (>= B21[x] 0) (<= B21[x] zv1) (<= (+ R0[x] B10[x] B20[x]) zv0) (<= (+ R1[x] B01[x] B21[x]) zv1) (<= (+ R2[x] B02[x] B12[x]) zv2)  (<= (+ R0[x] R1[x] R2[x] B10[x] B01[x] B02[x] B12[x] B20[x] B21[x]) N) (<= (+ B01[x] B10[x] B02[x] B20[x] B12[x] B21[x]) alpha) (> (* 2 (+ R0[x] B01[x] B02[x])) (+ N (* 2 alpha)))   (= 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) (>= R2[x] 0) (<= R2[x] zv2) (> (* 2 (+ R0[x] R1[x] R2[x])) (+ N (* 2 alpha))) (>= B01[x] 0) (<= B01[x] zv1) (>= B10[x] 0) (<= B10[x] zv0) (>= B02[x] 0) (<= B02[x] zv2) (>= B20[x] 0) (<= B20[x] zv0) (>= B12[x] 0) (<= B12[x] zv2) (>= B21[x] 0) (<= B21[x] zv1) (<= (+ R0[x] B10[x] B20[x]) zv0) (<= (+ R1[x] B01[x] B21[x]) zv1) (<= (+ R2[x] B02[x] B12[x]) zv2)  (<= (+ R0[x] R1[x] R2[x] B10[x] B01[x] B02[x] B12[x] B20[x] B21[x]) N) (<= (+ B01[x] B10[x] B02[x] B20[x] B12[x] B21[x]) alpha) (> (* 2 (+ R1[x] B10[x] B12[x])) (+ N (* 2 alpha)))   (= roundp 0)
(= Xp[x] 1) (= Vp[x] 2) (= Dp[x] 1)


; T6  --  at least alpha+1 votes 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) (>= R2[x] 0) (<= R2[x] zv2) (> (* 2 (+ R0[x] R1[x] R2[x])) (+ N (* 2 alpha))) (>= B01[x] 0) (<= B01[x] zv1) (>= B10[x] 0) (<= B10[x] zv0) (>= B02[x] 0) (<= B02[x] zv2) (>= B20[x] 0) (<= B20[x] zv0) (>= B12[x] 0) (<= B12[x] zv2) (>= B21[x] 0) (<= B21[x] zv1) (<= (+ R0[x] B10[x] B20[x]) zv0) (<= (+ R1[x] B01[x] B21[x]) zv1) (<= (+ R2[x] B02[x] B12[x]) zv2)  (<= (+ R0[x] R1[x] R2[x] B10[x] B01[x] B02[x] B12[x] B20[x] B21[x]) N) (<= (+ B01[x] B10[x] B02[x] B20[x] B12[x] B21[x]) alpha) (>= (+ R0[x] B01[x] B02[x]) (+ alpha 1)) (<= (* 2 (+ R0[x] B01[x] B02[x])) (+ N (* 2 alpha)))   (= roundp 0)
(= Xp[x] 0) (= Vp[x] 2) (= Dp[x] D[x])


; T7  --  at least alpha+1 votes 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) (>= R2[x] 0) (<= R2[x] zv2) (> (* 2 (+ R0[x] R1[x] R2[x])) (+ N (* 2 alpha))) (>= B01[x] 0) (<= B01[x] zv1) (>= B10[x] 0) (<= B10[x] zv0) (>= B02[x] 0) (<= B02[x] zv2) (>= B20[x] 0) (<= B20[x] zv0) (>= B12[x] 0) (<= B12[x] zv2) (>= B21[x] 0) (<= B21[x] zv1) (<= (+ R0[x] B10[x] B20[x]) zv0) (<= (+ R1[x] B01[x] B21[x]) zv1) (<= (+ R2[x] B02[x] B12[x]) zv2)  (<= (+ R0[x] R1[x] R2[x] B10[x] B01[x] B02[x] B12[x] B20[x] B21[x]) N) (<= (+ B01[x] B10[x] B02[x] B20[x] B12[x] B21[x]) alpha) (>= (+ R1[x] B10[x] B12[x]) (+ alpha 1)) (<= (* 2 (+ R1[x] B10[x] B12[x])) (+ N (* 2 alpha)))   (= 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) (>= R2[x] 0) (<= R2[x] zv2) (> (* 2 (+ R0[x] R1[x] R2[x])) (+ N (* 2 alpha))) (>= B01[x] 0) (<= B01[x] zv1) (>= B10[x] 0) (<= B10[x] zv0) (>= B02[x] 0) (<= B02[x] zv2) (>= B20[x] 0) (<= B20[x] zv0) (>= B12[x] 0) (<= B12[x] zv2) (>= B21[x] 0) (<= B21[x] zv1) (<= (+ R0[x] B10[x] B20[x]) zv0) (<= (+ R1[x] B01[x] B21[x]) zv1) (<= (+ R2[x] B02[x] B12[x]) zv2)  (<= (+ R0[x] R1[x] R2[x] B10[x] B01[x] B02[x] B12[x] B20[x] B21[x]) N) (<= (+ B01[x] B10[x] B02[x] B20[x] B12[x] B21[x]) alpha) (< (+ R0[x] B01[x] B02[x]) (+ alpha 1)) (< (+ R1[x] B10[x] B12[x]) (+ alpha 1))   (= 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)