[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] New state is function range 1 .. 10

 ChangeX1(a) ==  \E oid \in 1 .. 10 : OwnerId' = [OwnerId EXCEPT ![a] = oid]StephanOn 4 May 2023, at 14:36, Chris Hobbs wrote:I have a question of TLA+ syntax which I'm sure has been asked a dozen times before, but I can't find an answer either here or on StackOverflow. Consider the following program (obviously reduced to illustrate the problem):------------------------------- MODULE tryit3 -------------------------------(***************************************************************************See how to say "any member of the set of integers between 1 and 10" ***************************************************************************) EXTENDS IntegersCONSTANT Animal VARIABLE OwnerId TypeOK ==  /\ OwnerId \in [Animal -> 1 .. 10] (***************************************************************************Assume that initially all animals are owned by 9 ***************************************************************************) Init == /\ OwnerId = [a \in Animal |-> 9] (***************************************************************************This is horrible way of specifying that the new value of OwnerId can be anyinteger in 1 .. 10 (but it works!). It's a good job it's not 1 .. 100. ***************************************************************************) ChangeX1(a) ==  \/ OwnerId' = [OwnerId EXCEPT ![a] = 10]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 9]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 8]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 7]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 6]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 5]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 4]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 3]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 2]                              \/ OwnerId' = [OwnerId EXCEPT ![a] = 1]               (***************************************************************************What I really want to be able to say is something like this. But it givesa compilation error ***************************************************************************)(* ChangeX1(a) == OwnerId' = [OwnerId EXCEPT ![a] \in 1 .. 10] *)            Next == \E a \in Animal :        \/ ChangeX1(a)        =============================================================================As the comment at the bottom says, I'm trying to say that the new state of the function for a particular "animal", a, is any value in 1 .. 10. I've tried various ways of expressing this without syntactic success. Any help would be appreciated.Chris Hobbs -- 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/b5e325fe-3a8f-439b-9a69-b04c7eae844en%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/7CF9E1EA-370E-4582-8728-A53CABE4D8F6%40gmail.com.