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.