Re: [tlaplus] Re: How does TLC expand search?

Hi Hillel,

I was thinking about how the TLC checker searches for all the possible states *regardless* what exactly an OP refers to.

So for example,

Given a spec:

Next == OP1 \/ OP2 \/ OP3

Spec == Init /\ [][Next]_vars

and consider the case where the checker is at state S. The checker now proceeds to search all the *direct* child states (in a BFS style).

My question and predication is, for the above Next operation which contains a set of operations joined with *\/*, a state transition will never be conducted by applying both OP1 and OP2 (or any two of the three) on the current state S.

The checker enumerates the possible direct child states by applying OP1, OP2, and OP3 separately.

Best,

On Friday, 20 September 2019 00:29:07 UTC+8, Hillel Wayne wrote:

Hi Shiyao

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]

If VoteFor specifies maxBal', and IncreaseMaxBalspecifies maxBal', then they can only be true that the same time if there is some value for maxBal' that satisfies both actions.

Given TLC isn't giving you an error, I'm guessing you also have UNCHANGED votes in IncreaseMaxBal? Then they definitely both can't be true at the same time, as VoteFor would specify that votes changes and IncreaseMaxBal does not.

H

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a970adcf-3791-4835-b6c8-ac024b5c9cef%40googlegroups.com.