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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.