[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Why is the IDE telling me my actions will never be enabled? How should a mutable array of booleans be represented?
- From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
- Date: Tue, 7 Jun 2022 10:07:34 -0700
- Ironport-data: A9a23:t6f17KJCSQjT+uXIFE+RKpAlxSXFcZb7ZxGr2PjKsXjdYENS0DdRx mYYCDqAOf7eamb3edtwaojl9UkOuMDdzIVrSQQd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefSLlbFILas1hpZHGeIcw98z0M68wIFqtQw24LhXVvS4 YmaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhvvEo8 9BDkNuLdRoAL5bl37gfcUF3DHQrVUFG0OevzXmXtMWSywjCfSKpzag+Sk4xOoIc96B8BmQmG f4wcmhcKEDewbvon/TmGoGAhex7RCXvFJ8bs2lk0CqaB/Ata7vjcZ3l1fNo9R4KrPBzOamER OM8RgNCSzXhPUBwG38YD5UxmOqnnH7iayYeo1WQzUYyyzOCnFwtgeK0WDbTUv6mVZ5tuVuin SHpxXn+Ww0iBoKV6hPQpxpAgceWxX+hMG4IL5W09+VhnUaI7nAXAVsTTkH+oP+ji0f4WtRFK kVS9DBGkEQp3EmiT924WxPh5XDZ7lgTXN1fF+B84waIokbJ3+qHLkklFwVEZvlhj/MrbC0R/ xjVnfGxKiM65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8NFbYvXnHoYLLUKlsjHmMWqvn G3S/UDSk51W3JFbjfzqlbzSq2v0/sChc+Ij2unAsouYAu5RYYekY8ms5wGe46sQaomeSVaFs T4PnM32AAEy4XOly3HlrAYlRurBCxO53Nv03AQH834Jqm3FxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzsV5l2lfK6RI29D5g4i+aihLAhJGdrGwk+NSatM5zFzSDAbIlkZ cvBLp7yZZrkIf03lWboLwvi7VPb7nlmmTm7qWHTwBOg3r6TDEN5up9UWGZimtsRvfPsiFyNr b53bpLaoz0CDrCWSnSJoOY7cABbRVBmVM2eg5EGJoarfFA6cEl/UKW56e16K+RYc1F907mgE oeVBB8CkTISRBTvcm23V5yUQO+0Bssv9S5kVcHuVH7xs0UejU+UxP93X/MKkXMPrYSPFNZ4E KsIfduuGPNKRmiV8jgRd8Cj/oNlcxuviA2UODe9e340eJs5H17F/drtfw3O8igSD3vn7pBn+ OL+iQ6LE4AeQwlCDdrNbK79xV2Gu3VAyvl5WFHFI4UOdUi1qNpqJiX9g+UZOcYJLRmflDKW2 xzPWEUcqOzIuJM46p/FiPnc/YuuFuJ/GGtcHnXatOrna3OFozD7mYIZCbSGZzHQUm/w6Z6OX +QNwqGuKuADkXZLr5F4T+Rhw5U46oa9vLRd1AllQCjGYlnyUeFgL3CK0NN1u7VJ16NevQfqC EuD9sMDZ+eGP8TqFFMePg04dv/F3vYRw2GA4fMwKUT8xSl24LvWAR4JZkLT1nNQfOlvLYco4 eY9o8pKuQaxvRwnb4SdhSdO+mXQc3ENXvl1tpweB4O32AMnxksYOs7ZAy7ypZWBMpBCbxlsL TiTi67Pwb9bwxOaIXY0EHHM28tbhIgP6E8Wlg5cfwzRl4qXnOIz0T1Q7S8zElZfwCJB3r8hI WNsLUB0efiD8mY6gMlYQ12qABxLABHFqEX9x0FXxD/cRkisSmufI2o6NuKA81oe7npHOz1S+ riXxSW+Dma7IJyvjnRrABAmtvr4UNZq/RfDks2PEMOCEJ03biDin7e1I2EPrkK/U882gUTGo 8hs/fpxOP2gbndL/PNkBtnIz6kURTCFOHdGHaNr8pQPEDyOYzq1wzWPdx28d88RdfXG/VXkW p5uOt5XTEb5kymUqS0DHugDJLh7mPNv790HPbzxInMe9KebpyJtrYmX7TX0n2QxQt9jnMthe JndcSmOTj6ZiXdOwTSfqcBFPi+8b4BBalCsmu+y9+oNGtQIt+Q1KRM+1b69vnO0Ngp7/kLL4 FmSOfeOl+Eym55xm4bME7lYA1nmI93EUunVohu4tM5DbI+SPMrD3+/PRoIL4+iL0Xott9VLe XCltdf22AbBsu9zXT2J3ZaGEKZN6IO5W+8/3gcb6pVFtXPqZSMuy0JrF6OExVhhn9Ra6c2qS BG/ddOrM9USXr+xAVVLPjNGHU9157vfN8/dSODUkxhIIhca1gPDIdy98mLxdidQcSpg11gSz OPrk67G2+20Z7igyPPJ6z+KznO4zJLetXMaSuDM
- Ironport-hdrordr: A9a23:456NcqnP4zIsxwQY239wfH/236TpDfN0imdD5ihNYBxZY6Wkfp +V8IVi6fakslthIU3Ix+rrSc+9qBTnhOBICOgqTMiftWzd11dAQ7sSnrcKrweQZxEWs9QtoZ uJncBFeZ3N5XYTt7e63OD6Kads/DG/mJrYy9s2tk0dDj2D3spbnk1E43igYzpLrXh9dOsE/c Gnl4F6TlObEBx9H6DLfQh5YwXanaywqHulW291O/dA0njHsdqG0t/H+nOjr2cjul10sMIfGa msqX2d2kxhiZGGI93nuVM6X/9t6ZTcIxd4da+xYsV/EESktu5ZD74RLYFqdQpFwpDJ1H8a1O PUqxNlFcV+4XHccyWUpl/CwA/9yV8VmjPf9WM=
- Ironport-sdr: E7SFVCXwWTEVJYFBYETKF/Brt7oRB4y2tK1pZd71tTg+X6N3p87o7mMbo7rg2tL2u9cERs0J+8 K2+J2U3Huf1S1mJPSwyzI4UYMxEmZF0L/cxcack8oz/+hREKgFkVSkL5KZo09pa1KySJbFFAKi PvxSsaA0jkazSCqdb3Ml/aJ46vFkXa7utLcQ4hjBD7gH5vmbj/OSbjxUWJQaKoU8CIsrO92l1X rTjC1L42HW+MDpuXf7xDr/8YHQgCL9kBKgKnvkhW92QjHsHmOhkl2X8kGPno9yLPTeMdhf3fim OEu5QbBSKFR214/FImDFVwrx
- References: <b92cf6ed-f011-404d-b46c-0f6e63d2b56dn@googlegroups.com>
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.