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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Tue, 8 Jun 2021 12:40:15 -0700 (PDT)*Ironport-hdrordr*: A9a23:PdDhGq/7S3qOHY/2d7Fuk+ARI+orL9Y04lQ7vn2ZLiYlFvBw9vre+cjyt3fP4gr5PUtMpTnuAsm9qE3nhOFICOUqUYtLcmHdyRaVxatZnPPfKwSJIVyFyga2vZ0QD5SWceeAdmSS7vyKgjVQcexQo+Vvq5rY/Ns2pk0FJWpXgsdbjjuRJTzrbHGeLzMoOXNWLvShDgsunUvGRZyZBv7LYEU4Yw==*References*: <f71490a1-015b-c6f0-a24f-efe11a7757e4@gmail.com> <CAM3xQxF1rK3vC7LTYFHzyHoeb28zc4=r1f2PyVXvTt65QyddZw@mail.gmail.com> <211edb41-3abe-ea5c-80a5-445d36872205@lemmster.de>

I don't know if people realize that TLC can handle:

VARIABLES x, y, a, b, c

foo == <<x, y>>

bar == <<a, foo>>

boo == <<b, c>>

...

/\ UNCHANGED <<bar, d, boo>>

On Tuesday, June 8, 2021 at 12:13:42 PM UTC-7 Markus Alexander Kuppe wrote:

On 06.06.21 15:57, Isaac DeFrain wrote:

>

> To manage the amount of names I have to write following UNCHANGED, I

> usually write several /inclusive/ and /exclusive/ variable tuples; e.g.

> say we have the variables x1, x2, ..., xN and I have a few actions which

> change only x1 and x2 and leave x3, ..., xN unchanged (this would

> suggest an exclusive variable tuple to me). I'll define a tuple, call it

> non_x1_x2_vars == <<x3, ..., xN>>, and then just write UNCHANGED

> non_x1_x2_vars in the aforementioned actions. As long as you write all

> your actions in one module, this seems to work really well. Not to

> mention when you have 10+ variables in a spec, it becomes next to

> impossible to visually inspect whether you have included all the

> unchanged variables.

>

> I first saw this little trick in the raft spec

> <https://github.com/ongardie/raft.tla/blob/master/raft.tla> where they

> use several (what I would call) inclusive variable tuples.

Hi,

have you tried *simulating* the specs with TLC for a few seconds to find

any missing variables in UNCHANGED statements? I haven't yet, but I

would expect the trick to catch most of them.

Markus

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/96d60774-9895-43ec-a026-b31c7e12a2e6n%40googlegroups.com.

**References**:**[tlaplus] How do you do functions of structures?***From:*Hillel Wayne

**Re: [tlaplus] How do you do functions of structures?***From:*Isaac DeFrain

**Re: [tlaplus] How do you do functions of structures?***From:*Markus Kuppe

- Prev by Date:
**Re: [tlaplus] How do you do functions of structures?** - Next by Date:
**[tlaplus] Re: A thought when buying coffee today** - Previous by thread:
**Re: [tlaplus] How do you do functions of structures?** - Next by thread:
**Re: [tlaplus] How do you do functions of structures?** - Index(es):