Why is the IDE telling me my actions will never be enabled? How should a mutable array of booleans be represented?

[Alexander Farley]

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? 

[Markus Kuppe]

Your definition of Occupation in Init violates TypeOK. You probably meant to write:

Init ==
Occupation = [ i \in 1..5 |-> IF i = 1 THEN TRUE ELSE FALSE ]

More compactly:

Init ==
Occupation = [ i \in 1..5 |-> i = 1 ]


Your formula in Idle also lacks the DOMAIN operator.


Markus

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b92cf6ed-f011-404d-b46c-0f6e63d2b56dn%40googlegroups.com.