I would like to represent a data-structure which is (for example) a 5-element array of booleans. The values of each element need to be mutated by the state transitions. I must be doing something wrong because the model-checker is telling me that my actions are never enabled. Here is my code:
---- MODULE naschr ----
EXTENDS Naturals
VARIABLE Occupation
TypeOK ==
/\ Occupation \in [ { 1, 2, 3, 4, 5 } -> {TRUE, FALSE} ]
Init ==
/\ Occupation = [ i \in 1..5 |-> {TRUE, FALSE, FALSE, FALSE, FALSE} ]
MoveCar1 ==
/\ Occupation[1] = TRUE
/\ Occupation[2] = FALSE
/\ Occupation' = [Occupation EXCEPT ![1] = FALSE, ![2] = TRUE]
MoveCar2 ==
/\ Occupation[2] = TRUE
/\ Occupation[3] = FALSE
/\ Occupation' = [Occupation EXCEPT ![2] = FALSE, ![3] = TRUE]
MoveCar3 ==
/\ Occupation[3] = TRUE
/\ Occupation[4] = FALSE
/\ Occupation' = [Occupation EXCEPT ![3] = FALSE, ![4] = TRUE]
MoveCar4 ==
/\ Occupation[4] = TRUE
/\ Occupation[5] = FALSE
/\ Occupation' = [Occupation EXCEPT ![4] = FALSE, ![5] = TRUE]
MoveCar5 ==
/\ Occupation[5] = TRUE
/\ Occupation[1] = FALSE
/\ Occupation' = [Occupation EXCEPT ![5] = FALSE, ![1] = TRUE]
Idle ==
/\ \A i \in Occupation: FALSE
/\ Occupation' = Occupation
Next ==
\/ MoveCar1
\/ MoveCar2
\/ MoveCar3
\/ MoveCar4
\/ MoveCar5
\/ Idle
====
The idea here is to cause an occupied element of the array to transition to the next spot in the array if the next spot is empty.
Note: I have already posted this on Reddit:
https://www.reddit.com/r/tlaplus/comments/v5t98f/why_is_the_ide_telling_me_my_actions_will_never/
And I got a helpful suggestion on how to convert my code to use a Tuple instead of a Function. So, I do understand how to get this to work if I convert Occupation into a Tuple. I am specifically wondering: how do I get this to work using Function notation?
--