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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

> On Jun 7, 2022, at 9:19 AM, Alexander Farley <alexander.s.farley@xxxxxxxxx> wrote:
> 
> 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? 
> 
> 
> -- 
> 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+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b92cf6ed-f011-404d-b46c-0f6e63d2b56dn%40googlegroups.com.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CD4F919D-8300-4DB8-8298-463E46875DE7%40lemmster.de.