;;; Dekker's algorithm for mutual exclusion 
;;; Elena - June 14, 2018


PARAMETER_DECLARATIONS 1
N


; subphase for choice of next value of turn
INTEGER_VARIABLES_DECLARATIONS 1
round

 
ARITHMETIC_ARRAY_DECLARATIONS 0


; WE (want-to-enter): boolean local flag globally visible
; ST (status): indicates whether process is in critical section
; T (turn): flag representing the global variable "turn"
ENUMERATED_ARRAY_DECLARATIONS 3
WE 2
ST 2
T  2


COUNTER_DECLARATIONS 3
zwe : (= WE[x] 1)
zcs : (= ST[x] 1)
zt  : (= T[x] 1)


ARITHMETIC_ASSERTION
 (>= zt 0) (<= zt 1)


TRANSITION_CASES 6


; T1 -- choice of next turn
CASE
(= round 0) (= roundp 1) (= zt 0)
(= ST[x] 0) (= T[x] 0) (= STp[x] ST[x]) (= Tp[x] 1) (= WEp[x] WE[x])


; T2 -- process enters in critical section
CASE
(= round 1) (= roundp round)
(= ST[x] 0) (= T[x] 1) (= STp[x] 1) (= Tp[x] T[x]) (= WEp[x] 1)


; T3 -- process cannot enter critical section (1)
CASE
(= round 1) (= roundp round) (>= zwe 2)
(= ST[x] 0) (= WE[x] 1) (not (= T[x] 1)) (= STp[x] ST[x]) (= WEp[x] 0) (= Tp[x] T[x])


; T4 -- busy waiting
CASE
(= round 1) (= roundp round)
(= ST[x] 0) (not (= T[x] 1)) (= STp[x] ST[x]) (= WEp[x] WE[x]) (= Tp[x] T[x])


; T5 -- process leaves critical section and gives turn
CASE
(= round 1) (= roundp 0)
(= ST[x] 1) (= STp[x] 0) (= Tp[x] 0) (= WEp[x] 0)


; T6 -- process wants to re-enter in critical section
CASE
(= round 1) (= roundp round)
(= ST[x] 0) (= WE[x] 0) (= STp[x] ST[x]) (= WEp[x] 1) (= Tp[x] T[x])



; turn may have whatever value
INITIALIZATION
 (= round 0)
 (= ST[x] 0) (= WE[x] 1) (= T[x] 0)


UNSAFE_CONDITION
(> zcs 1)