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

Re: [tlaplus] How do you do functions of structures?



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