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

------------------------------- 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)

=============================================================================