# [tlaplus] New state is function range 1 .. 10

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.