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

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:

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!