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

I was one of the student's making this mistake. Destructuring did resolve some issues and improved my specification performance.

However true, I did find it unfortunate. The primary purpose of the record is to group associated data together. You can point out the isomorphism all day but that doesn't change the fact that it is easier to reason about related data when it is in the same place. Neither object oriented or functional programming languages really encourage destructuring data in this way. It goes against the grain of most programmers training for modularity and encapsulation. It also likely makes the TLA+ specification diverge from the code that it is trying to describe so verifying equivalent states between a production system and the tla spec will now need another translation step to either destructure or restructure the data for comparison.

I suppose the problem is actually that from the perspective of TLA+/TLC is that they are not isomorphic They handle the two cases differently.

Perhaps PlusCal could provide a key word to handle the conversion automatically. I can see either nested records or set unions creating complications, but maybe this would be good enough for most situations.


WorkerState == DESTRUCTURE [queue: Seq(Msg), online: BOOLEAN]
state = DESTRUCTURE [worker \in Worker |-> [queue: <<>>, online: TRUE]]
TypeOK ==
state \in [Worker -> WorkerState]

Transforms into something like
WorkerState#queue == Seq(Msg)
WorkerState#_online_ == BOOLEAN

state#queue == [worker \in Worker |-> <<>>]
state#_online_ == [worker \in Worker |-> TRUE]

TypeOK ==
/\ state#queue \in [Worker -> WorkerState#queue]
/\ state#online \in [Worker -> WorkerState#online]

On Monday, June 7, 2021 at 7:34:01 AM UTC-7 Stephan Merz wrote:
TLAPS relies on type information for optimizing the encoding for back-end reasoners, and a typing invariant such as

/\ x \in Nat
/\ y \in {"foo", "bar"}
/\ z \in [ Client -> Int ]

is easier to handle than

state \in [ x : Nat, y : {"foo", "bar"}, z : [Client -> Int] ]

Stephan

On 7 Jun 2021, at 13:44, Karolis Petrauskas <k.petr...@xxxxxxxxx> wrote:

I was used to using the structured version, until I started to play with TLAPS.
The things are easier to prove in the case of the structure split to multiple variables.
Not sure why. Maybe the prover can easier resolve the actions that do not change a variable used in a property to prove.

Karolis

On Sun, Jun 6, 2021 at 11:34 PM Hillel Wayne <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

--
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+u...@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+u...@xxxxxxxxxxxxxxxx.

--
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/b08e7a94-7557-4980-a90a-65b7f498e37en%40googlegroups.com.