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