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

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

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.


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.


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.