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

[Felipe Oliveira Carvalho <felipekde@xxxxxxxxx>]

I like to group all related state variables in the same struct and
then I define pure functions that return a copy with the state with
the intended changes.

This makes my action formulas look like

/\ workerState' = RecvMessage(workerState, ...)

On Sun, Jun 6, 2021 at 10: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/CAOC8YXZ-rvxttBdfChxn7t_g6CCA9hWfQH-rhKOVtXq6%2BARqPw%40mail.gmail.com.