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

[tlaplus] How do you do functions of structures?

Say you have a spec like this:

---- MODULE foo ----

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


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?


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.