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

*From*: Chris Hobbs <cwlhobbs@xxxxxxxxx>*Date*: Thu, 4 May 2023 05:36:42 -0700 (PDT)

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)

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

(***************************************************************************

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.

**Follow-Ups**:**Re: [tlaplus] New state is function range 1 .. 10***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Unknown Location Error** - Next by Date:
**Re: [tlaplus] New state is function range 1 .. 10** - Previous by thread:
**Re: [tlaplus] Unknown Location Error** - Next by thread:
**Re: [tlaplus] New state is function range 1 .. 10** - Index(es):