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

• From: Isaac DeFrain <isaacdefrain@xxxxxxxxx>
• Date: Sun, 6 Jun 2021 16:57:48 -0600
• References: <f71490a1-015b-c6f0-a24f-efe11a7757e4@gmail.com>

Hey Hillel,

I've been burned too many times by trying to write variables as records of multiple things that could rightfully be variables (like you showed in the first module). The main issue is that you lose the ability to compose actions that only change a few variables each when the actions try to change different fields of the same variable. E.g.

---- MODULE ex ----

EXTENDS Naturals

VARIABLE x

Init == x = [ "fst" |-> 0, "snd" |-> 0 ]

TypeOK == x \in [ "fst" : Nat, "snd" : Nat ]

Incr_fst == x' = [ x EXCEPT !.fst = @ + 1 ]

Incr_snd == x' = [ x EXCEPT !.snd = @ + 1 ]

\* Unfortunately, this doesn't make sense here as both (sub)actions attempt to set the successor value of x... bummer :(
Incr_both ==
/\ Incr_fst
/\ Incr_snd

\* ...

Next ==
\/ Incr_both
\/ ...

\* ...

====

So I'll always choose to have more variables + composability of (sub)actions + control over less variables.

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 where they use several (what I would call) inclusive variable tuples.

Best,

Isaac DeFrain

On Sun, Jun 6, 2021 at 2:34 PM Hillel Wayne <hwayne@xxxxxxxxx> wrote:
Say you have a spec like this:

---- MODULE foo ----

EXTENDS Sequences
CONSTANT Worker, Msg
ASSUME Worker # {} /\ Msg # {}

VARIABLE state

WorkerState == [queue: Seq(Msg), online: BOOLEAN]
TypeOK ==
state \in [Worker -> WorkerState]

\* ...

====

I've noticed that a lot of my students start by writing things that way,
where we have a single state variable that is a function from Worker to
WorkerState. I generally encourage them to instead write it as

VARIABLES worker_queue, worker_online

TypeOK ==
/\ worker_queue \in [Worker -> Seq(Msg)]
/\ worker_online \in [Worker -> BOOLEAN]

\* ...

====

The reason why I prefer this is because you can define worker_queue' and
worker_online' in separate actions, while you can only (easily) define
state' in a single action. Also, it's easier to do things like
worker_queue' = [w \in Worker |-> (* ... *)]. The downside is your
UNCHANGED statements get a little more cluttered, but IMO the benefits
are worth it.

What do you all do? Do "destructure" your state or prefer to keep it all
in one variable?

H

--
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/f71490a1-015b-c6f0-a24f-efe11a7757e4%40gmail.com.

--
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/CAM3xQxF1rK3vC7LTYFHzyHoeb28zc4%3Dr1f2PyVXvTt65QyddZw%40mail.gmail.com.