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

*From*: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>*Date*: Tue, 8 Jun 2021 12:13:32 -0700*References*: <f71490a1-015b-c6f0-a24f-efe11a7757e4@gmail.com> <CAM3xQxF1rK3vC7LTYFHzyHoeb28zc4=r1f2PyVXvTt65QyddZw@mail.gmail.com>

On 06.06.21 15:57, Isaac DeFrain wrote:

To manage the amount of names I have to write following UNCHANGED, Iusually write several /inclusive/ and /exclusive/ variable tuples; e.g.say we have the variables x1, x2, ..., xN and I have a few actions whichchange only x1 and x2 and leave x3, ..., xN unchanged (this wouldsuggest an exclusive variable tuple to me). I'll define a tuple, call itnon_x1_x2_vars == <<x3, ..., xN>>, and then just write UNCHANGEDnon_x1_x2_vars in the aforementioned actions. As long as you write allyour actions in one module, this seems to work really well. Not tomention when you have 10+ variables in a spec, it becomes next toimpossible to visually inspect whether you have included all theunchanged variables.I first saw this little trick in the raft spec<https://github.com/ongardie/raft.tla/blob/master/raft.tla> where theyuse several (what I would call) inclusive variable tuples.

Hi,

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/211edb41-3abe-ea5c-80a5-445d36872205%40lemmster.de.

**Follow-Ups**:**Re: [tlaplus] How do you do functions of structures?***From:*Leslie Lamport

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

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

- Prev by Date:
**[tlaplus] A thought when buying coffee today** - Next by Date:
**Re: [tlaplus] How do you do functions of structures?** - 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):