After some playing, it seems to me,
For Next == OP1 \/ OP2 \/ OP3
For \/ connected OPs, TLC will only transit from either OP1, OP2, ..., but *never* transition to a state of both OP1 and OP2 applied.
In the above figure, either IncreaseMaxBal is applied or VoteFor, but never both.
related code:
VoteFor(a, b, v) ==
/\ maxBal[a] =< b
/\ \A vt \in votes[a] : vt[1] /= b
/\ \A c \in Acceptor \ {a} :
\A vt \in votes[c] : (vt[1] = b) => (vt[2] = v)
/\ \E Q \in Quorum : ShowsSafeAt(Q, b, v)
/\ votes' = [votes EXCEPT ![a] = votes[a] \cup {<<b, v>>}]
/\ maxBal' = [maxBal EXCEPT ![a] = b]
(***************************************************************************)
(* The rest of the spec is straightforward. *)
(***************************************************************************)
Next == \E a \in Acceptor, b \in Ballot :
\/ IncreaseMaxBal(a, b)
\/ \E v \in Value : VoteFor(a, b, v)
Spec == Init /\ [][Next]_<<votes, maxBal>>
