[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]

Stephan

On 4 May 2023, at 14:36, Chris Hobbs <cwlhobbs@xxxxxxxxx> 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 Integers

CONSTANT 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 any
integer 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 gives
a 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.