[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: How does TLC expand search?

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>>

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/a970adcf-3791-4835-b6c8-ac024b5c9cef%40googlegroups.com.