[tlaplus] non-atomic Peterson in TLA+

I have that TLA+ Program, and I don't understand why do I get zero states when I run the TLC model checker? P.S: The method here is non-atomic. Do I need to edit something in the Review Model?

Thanks in advance,

VARIABLES req1, req2, crit1, crit2, turn, inReq1, inReq2

TypeInv ==

/\ req1 \in BOOLEAN

/\ req2 \in BOOLEAN

/\ crit1 \in BOOLEAN

/\ crit2 \in BOOLEAN

/\ turn \in {1,2}

/\ inReq1 \in BOOLEAN

/\ inReq2 \in BOOLEAN

v == <<req1, req2, crit1, crit2, turn, inReq1, inReq2>>

Init ==

/\ req1 = FALSE

/\ crit1 = FALSE

/\ req2 = FALSE

/\ crit2 = FALSE

/\ inReq1 = FALSE

/\ inReq2 = FALSE

/\ TypeInv

Request1a ==

/\ ~req1

/\ ~inReq1

/\ req1 = TRUE

/\ inReq1 = TRUE

/\ UNCHANGED <<req2, crit1, crit2, inReq2, turn>>

Request2a ==

/\ ~req2

/\ ~inReq2

/\ req2 = TRUE

/\ inReq2 = TRUE

/\ UNCHANGED <<req1, crit1, crit2, inReq1, turn>>

Request1b ==

/\ inReq1

/\ inReq1' = FALSE

/\ turn' = 2

/\ UNCHANGED <<req1, req2, crit1, crit2, inReq2>>

Request2b ==

/\ inReq2

/\ inReq2' = FALSE

/\ turn' = 1

/\ UNCHANGED <<req1, req2, crit1, crit2, inReq1>>

Enter1 ==

/\ ~inReq1 \* here we check if it is not in the req1,

/\ req1 \* then we get into req1

/\ ~req2 \/ turn = 1 \* then we check if it is not in the req2, and not turn 1

/\ crit1' = TRUE \* then we get into the other flag which is crit1 and assign it to TRUE

/\ UNCHANGED <<req1, req2, crit2, turn, inReq1, inReq2>>

Enter2 ==

/\ ~inReq2

/\ req2

/\ ~req1 \/ turn = 2

/\ crit2' = TRUE

/\ UNCHANGED <<req1, req2, crit1, turn, inReq1, inReq2>>

Exit1 ==

/\ crit1

/\ crit1' = FALSE

/\ req1' = FALSE

/\ UNCHANGED <<req2, crit2, inReq1, inReq2, turn>>

Exit2 ==

/\ crit2

/\ crit2' = FALSE

/\ req2' = FALSE

/\ UNCHANGED <<req1, crit1, inReq1, inReq2, turn>>

Prog1 ==

\/ Request1a

\/ Request1b

\/ Enter1

\/ Exit1

Prog2 ==

\/ Request2a

\/ Request2b

\/ Enter2

\/ Exit2

Next == Prog1 \/ Prog2

Prog == Init /\ [][Next]_v /\ WF_v(Prog1) /\ WF_v(Prog2)

====================================================

Safety == [] ~(crit1 /\ crit2)

Liveness == /\ (req1 ~> crit1)

/\ (req2 ~> crit2)

Spec == Safety /\ Liveness