[tlaplus] Re: Best practices / advise on (de)structuring specs (modularize)

[Muhammad El-Hindi <mu7eh7@xxxxxxxxx>]

I'll try to update/answer my own question as I learn more things, maybe learners of TLA+ will find this helpful.

I learned two things that are important for my question above:

1) State variables should only be updates once:
E.i. each primed variable (x') in an action definition must be assigned exactly once. This means the action must specify exactly one new value for each variable it changes.

In contrast to that, earlier I used methods/operators to update primed values multiple times (i.e., by invoking the method/operator with different variables)

2) TLA+ defines operators not methods:
I used to thing of operators as known from traditional programming languages where methods contain executable code that modifies the state directly. 

In TLA+, operators are used to define expressions or actions in a more modular and reusable way. An operator is essentially a parameterized _expression_ or a formula. When you define an operator and then use it within an action, you're not executing anything per se; rather, you're expanding that operator with specific arguments into its definition at that place in the action.
By also considering 1) from above, operators should not modify state variables, but be used as a modular way to compute potential state updates. E.g.:

Add(x, y) == x + y

IncreaseAction == a' = Add(a, 1)
A helpful section to learn more about Operators in TLA+ is Section 6.4 Functions versus Operators in the Book Specifying Systems.

On Wednesday, April 24, 2024 at 8:14:30 PM UTC+2 Muhammad El-Hindi wrote:

Hi,

I am still new to TLA+. I started by watching the Video Course and plan to read the book Specifying Systems next.

While playing around with a toy specification I made the following observation:

Why do the following two variants results in different numbers of states although they seem identical?
Variant 1 (Destructured/Decoupled):
\* Inform others what our current LSN is
GossipCurrentLSN(receiving_nodes, currentLSN) ==
    /\ LSNGossipReceived' = [node \in Nodes |-> IF node \in receiving_nodes THEN LSNGossipReceived[node] \union {CurrentLSN} ELSE LSNGossipReceived[node] ]

\* Create a LSNRequest from the source
RequestLSNs(requester) ==
    \E receiving_nodes \in SUBSET (Nodes \ {requester}): \* can be empty set, simulating that nobody might receive the request
        \* request contains our NodeId, the currentLSN and any gaps
        LET request == <<requester, Gaps[requester]>>
        IN
        /\ ReceivedLSNRequests' = [node \in Nodes |-> IF node \in receiving_nodes THEN ReceivedLSNRequests[node] \union {request} ELSE ReceivedLSNRequests[node] ]
        \* Model that currentLSN gossip is piggy-backed when requesting LSNs
        /\ GossipCurrentLSN(receiving_nodes, LSNs[requester])
        /\ UNCHANGED <<CurrentLSN, LSNs, Gaps, LSNsReceived>>

Variant 2:

\* Create a LSNRequest
RequestLSNs(requester) ==
\E receiving_nodes \in SUBSET (Nodes \ {requester}): \* can be empty set, simulating that nobody might receive the request
\* request contains our NodeId, the currentLSN and any gaps
LET request == <<requester, Gaps[requester]>>
IN
/\ ReceivedLSNRequests' = [node \in Nodes |-> IF node \in receiving_nodes THEN ReceivedLSNRequests[node] \union {request} ELSE ReceivedLSNRequests[node] ]
\* Model that currentLSN gossip is piggy-backed when requesting LSNs
/\ LSNGossipReceived' = [node \in Nodes |-> IF node \in receiving_nodes THEN LSNGossipReceived[node] \union {LSNs[requester]} ELSE LSNGossipReceived[node] ]
/\ UNCHANGED <<CurrentLSN, LSNs, Gaps, LSNsReceived>>

 I noticed that in TLC first (destructured) variant results in 400 distinct states while Variant 2 results in 384 distinct states.

My expectation was that both variants result in the same number of states.
My understanding is that while both variants have the same number of theoretical states, TLC applies different state space pruning techniques and ends up with a different number of distinct states.

This is also the case for the following simple spec, with which I tried to reproduce my above observation:
------------------------------ MODULE testSpec ------------------------------
EXTENDS Naturals, FiniteSets, Integers

CONSTANTS MaxCounter
ASSUME MaxCounter > 0

VARIABLES CounterA, CounterB

IncB(value) ==
    /\ CounterB' = value
   
IncA ==
    /\ CounterA < MaxCounter
    /\ CounterA' = CounterA + 1
    \* /\ CounterB' = CounterA + 1
    /\ IncB(CounterA +1)

FinalStateAction ==
    /\ CounterA = MaxCounter
    /\ UNCHANGED <<CounterA, CounterB>>
   
Init ==
    /\ CounterA = 0
    /\ CounterB = 0
   
Next ==
    \/ IncA
    \/ FinalStateAction
=============================================================================

My high-level question at this point would be when it is advisable to split state updates to separate actions (as done in variant 1). When would this be semantically different or identical to doing state updates in the same action.

Thanks in advance for your help and advise!

-- 
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/356c65af-2209-4bc9-8bdd-35cc0ca5b4c8n%40googlegroups.com.