Yeah destructuring is the way to go. Knowing which variables are changed vs unchanged in a given step is a very important component of documentation, in my opinion. Greatly eases translation into actual code. It also reads a lot nicer having primed variable expressions in different conjunction bullets. Plus the state traces are much easier to read.
On Sunday, June 6, 2021 at 4:34:58 PM UTC-4 hwa...@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