;;; Correctness for Bizantine Broadcast Primitive 
;;; (with N0 processes, at most f<=t<1/3 N0 faulty)
;;; Elena - Apr. 13, 2018


PARAMETER_DECLARATIONS 4
N
N0
t
f


INTEGER_VARIABLES_DECLARATIONS 1
round


ARITHMETIC_ARRAY_DECLARATIONS 1
RE


ENUMERATED_ARRAY_DECLARATIONS 3
RI 2
SE 2
AC 2


COUNTER_DECLARATIONS 3
zse : (= SE[x] 1) 
zac : (= AC[x] 1)  
zri : (= RI[x] 1) 


ARITHMETIC_ASSERTION
 (= N0 (+ N f)) (>= N0 (* 3 t)) (>= t f)  (>= f 0)


TRANSITION_CASES 5

; sender is correct --> every correct process received init from it and thus sends echo
CASE
(= round 0) (= roundp 1)
(= RI[x] 1) (= SEp[x] 1) (= ACp[x] AC[x])


; every correct process that did not receive the init does nothing
CASE
(= round 0) (= roundp 1)
(= RI[x] 0) (= SEp[x] 0) (= ACp[x] AC[x])


; if received >= N0-t > 2t echos then accept (and send echo)
CASE
(>= round 1) (= roundp 2) (>= RE[x] zse) (>= (+ zse f) RE[x]) (>= (+ RE[x] t) N0) 
(= SEp[x] 1) (= ACp[x] 1) 


; if received >= N0 - 2t > t echos then send echo
CASE
(>= round 1) (= roundp 2) (>= RE[x] zse) (>= (+ zse f) RE[x]) (< (+ RE[x] t) N0) (>= (+ RE[x] (* 2 t)) N0)
(= SEp[x] 1) (= ACp[x] AC[x])


; if received less than N0 -2t echos then do nothing
CASE
(>= round 1) (= roundp 2) (>= RE[x] zse) (>= (+ zse f) RE[x])  (< (+ RE[x] (* 2 t)) N0)
(= SEp[x] SE[x]) (= ACp[x] AC[x])
 

;every correct process receives init from correct sender
INITIALIZATION
 (= zri 0) (= zse 0) (= zac 0) (= round 0)
 (= AC[x] 0) (= SE[x] 0) (= RI[x] 0)


UNSAFE_CONDITION
(> zac 0)