;;; Integrity (I) for Uniform Timed Reliable Broadcast 
;;; If no process broadcasts m, then no process delivers it
;;; (with N processes)
;;; Elena - June 26, 2018


PARAMETER_DECLARATIONS 3
N
t
f


INTEGER_VARIABLES_DECLARATIONS 1
round


ARITHMETIC_ARRAY_DECLARATIONS 1
RE


; FI (first): first reception of message (0= not received; 1=just received; 2=already broadcast) 
; DE (delivered); FA (faulty): 1=correct; 0=going to crash; 2=crashed
ENUMERATED_ARRAY_DECLARATIONS 3
FI 3
DE 2
FA 3


COUNTER_DECLARATIONS 6
zr1 : (= FI[x] 1) (= FA[x] 1)
zr0 : (= FI[x] 1) (= FA[x] 0)
zda : (= DE[x] 1) 
zf0 : (= FA[x] 0)
zf1 : (= FA[x] 1)
zf2 : (= FA[x] 2)


ARITHMETIC_ASSERTION
 (> N t) (>= t f) (>= f 0) (<= (+ zf0 zf2) f)


TRANSITION_CASES 2

; T1 -- process receives message for the first time: enabled to send
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= RE[x] zr1) (<= RE[x] (+ zr1 zr0)) (>= RE[x] 1)
(= FI[x] 0) (< FA[x] 2) (= FIp[x] 1) (= DEp[x] 1) (=> (= FI[x] 1) (= FIp[x] 2) (= DEp[x] 1)) (=> (= FA[x] 0) (= FAp[x] 2)) (or (and (= FA[x] 1) (= FAp[x] 0)) (= FA[x] FAp[x]) ) 


; T2 -- process receives message not for first time: it does nothing
CASE
(>= round 0) (<= round (+ f 1)) (= roundp (+ round 1)) (>= RE[x] zr1) (<= RE[x] (+ zr1 zr0)) (>= RE[x] 1)
(>= FI[x] 1) (< FA[x] 2) (= FIp[x] FI[x]) (= DEp[x] 1) (=> (= FI[x] 1) (= FIp[x] 2) (= DEp[x] 1)) (=> (= FA[x] 0) (= FAp[x] 2)) (or (and (= FA[x] 1) (= FAp[x] 0)) (= FA[x] FAp[x]) ) 



; just one initiator
INITIALIZATION
(= round 0)
(= FI[x] 0) (= FA[x] 1) (= DE[x] 0)


; some process delivered a message
UNSAFE_CONDITION
(>= round (+ f 1)) (> zda 0)