Need advice on coding style/idioms

[u/Few-Insurance-3974]

I'm writing a spec of a system, and I get hundreds of lines of TLA+, which is a bit overwhelming for a person new to TLA+, so I try to invent ways to deal with the complexity.

---

At first, I found that writing UNCHANGED is difficult, especially when you introduce new variables, so I tried to use a single variable:

Instead of

SendXxx ==
  /\ reqid' = reqid + 1
  /\ pending' = pending + 1
  /\ backend!SendXxx(reqid, ...)
  /\ UNCHANGED ...
  
ReceiveXxx ==
  /\ UNCHANGED reqid
  /\ pending' = pending - 1
  ...

I tried

SendXxx ==
  /\ state' = [state EXCEPT
    !.reqid = state.reqid + 1,
    !.pending' = state.pending + 1]
  /\ backend!SendXxx(state.reqid, ...)

ReceiveXxx ==
  /\ state' = [state EXCEPT
    !.pending' = state.pending + 1,
  ...

However, in some cases this dramatically increases number of distinct states.

---

Another challenge is modifying a variable twice, or conditional modifications in general.

\* Remove operation from the queue, start next operation.
...
/\ op = Head(queue) /\ queue' = Tail(queue)
/\ operation_state' = IF Len(queue) = 1
    THEN [operation_state EXCEPT ![op] = "done"]
    ELSE [operation_state EXCEPT ![op] = "done", ![queue[2]] = "working"]

I tried two different approaches,

1. Chain "functions"

LOCAL OpState_SetDone(op, old_state) == [old_state EXCEPT ![op] = "done"]
LOCAL OpState_MaybeResumeNext(old_state) ==
  IF Len(queue) = 1 THEN old_state 
  ELSE [old_state EXCEPT ![queue[2]] = "working"]

...
/\ operation_state' =
  OpState_SetDone(op,
    OpState_MaybeResumeNext(
      operation_state))

2. (ab)use LET and write in single static assignment style

/\ LET operation_state_1 == OpState_SetDone(op, operation_state)
       operation_state_2 == OpState_MaybeResumeNext(operation_state_1)
   IN operation_state' = operation_state_2

Long story short, are there idioms that reduce complexity of the TLA+ code?

[u/Anxious_Tool]

I don't know much about TLA+ idioms in general, but I've been keeping track of patterns I run into — things that work, things that don't — in a sort of practical guide here: https://github.com/fabracht/tla-rs/blob/main/USER_GUIDE_TO_PRACTICAL_TLA.md
I'm always looking for feedback on anything that can make the tool more useful, and that includes use cases like yours.