;;; Abort-validity for non-blocking atomic commitment
;;; R. Guerraoui - On the hardness of failure-sensitive agreement problems
;;; Transcription of FMSD'17 model
;;; Elena - July 20, 2018


PARAMETER_DECLARATIONS 2
N
F


INTEGER_VARIABLES_DECLARATIONS 1
round


ARITHMETIC_ARRAY_DECLARATIONS 2
nrcvdNo
nrcvdYes


; FD: failure detector (process who will crash) 
; DE: 0 (abort) - 1 (commit) - 2 (undefined)
ENUMERATED_ARRAY_DECLARATIONS 3
FD 2
VO 2
DE 3


COUNTER_DECLARATIONS 7
nsntNo  : (= VO[x] 0) (= FD[x] 0)
nsntYes : (= VO[x] 1) (= FD[x] 0)
nsntNoF  : (= VO[x] 0) (= FD[x] 1)
nsntYesF : (= VO[x] 1) (= FD[x] 1)
zc  : (= FD[x] 1)
zda : (= DE[x] 0)
zdc : (= DE[x] 1)


ARITHMETIC_ASSERTION
 (> N 1) (> N F) (<= zc F)


TRANSITION_CASES 3

; T1 -- if crash predicted
CASE
(= round 0) (= roundp 1) (> zc 0)
(= DE[x] 2) (= DEp[x] 0) (= FDp[x] FD[x]) (= VOp[x] VO[x])  


; T2 -- if no crash predicted and some "no" vote
CASE
(= round 0) (= roundp 1) (= zc 0) (>= nrcvdNo[x] nsntNo) (<= nrcvdNo[x] (+ nsntNo nsntNoF)) (>= nrcvdYes[x] nsntYes) (<= nrcvdYes[x] (+ nsntYes nsntYesF)) (> nrcvdNo[x] 0)
(= DE[x] 2) (= DEp[x] 0) (= FDp[x] FD[x]) (= VOp[x] VO[x]) 


; T3 -- if no crash predicted and all "yes" votes
CASE
(= round 0) (= roundp 1) (= zc 0) (>= nrcvdNo[x] nsntNo) (<= nrcvdNo[x] (+ nsntNo nsntNoF)) (>= nrcvdYes[x] nsntYes) (<= nrcvdYes[x] (+ nsntYes nsntYesF)) (= nrcvdNo[x] 0) (= nrcvdYes[x] N)
(= DE[x] 2) (= DEp[x] 1) (= FDp[x] FD[x]) (= VOp[x] VO[x]) 



;every correct process receives init from correct sender
INITIALIZATION
 (= round 0) (>= nsntNo 1)
 (= DE[x] 2)


UNSAFE_CONDITION
(> zdc 0) (= round 1)