[tlaplus] How do you do functions of structures?

[Hillel Wayne <hwayne@xxxxxxxxx>]

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.