How does TLC expand search?

43 views
Skip to first unread message

Shiyao MA

unread,
Sep 19, 2019, 2:48:30 AM9/19/19
to tlaplus
Hi,

Give a next statement like:
Next == OP1 \/ OP2 \/ OP3

where OPx are further defined by other constructs, e.g., OP1 = OP1Sub1 \/ OP1Sub2


The question is, in what order does TLC verify all the behaviors?

The doc says TLC searches in a BFS order by default.  So TLC will enumerate all the direct child states given a parent state. But in what order/logic does TLC enumerate all the direct child states?

Thanks.

Shiyao MA

unread,
Sep 19, 2019, 3:30:13 AM9/19/19
to tla...@googlegroups.com
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 directly* 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>>



Hillel Wayne

unread,
Sep 19, 2019, 12:29:07 PM9/19/19
to tla...@googlegroups.com
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 IncreaseMaxBal specifies 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 tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a970adcf-3791-4835-b6c8-ac024b5c9cef%40googlegroups.com.

Shiyao MA

unread,
Sep 19, 2019, 11:01:10 PM9/19/19
to tlaplus
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 IncreaseMaxBal specifies 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.

Hillel Wayne

unread,
Sep 20, 2019, 12:53:32 AM9/20/19
to tla...@googlegroups.com

I'm having some trouble coming up with a valid spec where that would matter. You're saying that OP1, OP2, and OP1 /\ OP2 are all valid actions, but also that the conjunction includes transitions that aren't included in either individual action. As far as I know, the semantics of TLA+, in particular that the next-state relation must completely specify all variables, make that impossible. But I'd be happy to be proven wrong on this!

With that in mind, I suspect that TLC doesn't check those transitions. You'd have to ask Markus to know for sure, though.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/18c0b8b6-1fe6-40b8-8560-d808d6bc7dc6%40googlegroups.com.

Stephan Merz

unread,
Sep 22, 2019, 2:35:13 AM9/22/19
to tla...@googlegroups.com
Let me rephrase Hillel's intuition: suppose we have a next-state relation

Next == A \/ B \/ ...

Given state s, TLC will process action A by computing the set

Post(s,A) == { t : (s,t) |= A }     [1]

Clearly, we have that

Post(s, A /\ B) \subseteq Post(s,A)

and therefore any state u such that (s,u) |= A /\ B is a member of Post(s,A) and will be generated by TLC. Because it is also a member of Post(s,B), the state u will be regenerated when TLC processes action B.

Stephan

[1] The restrictions that TLC imposes ensure that Post(s,A) is effectively computable and finite. In particular, it is well defined, which is all that matters here.


Message has been deleted

Stephan Merz

unread,
Sep 23, 2019, 3:06:14 AM9/23/19
to tla...@googlegroups.com
It is very common that actions are disjoint, i.e. Post(s,A) \cap Post(s,B) = {}, but my explanation also covers the case where this is not so.

Hope this helps,
Stephan

On 23 Sep 2019, at 04:35, Shiyao MA <i...@introo.me> wrote:

Hi Merz,

What I understand from Hillel's reply is that,
If Post(s, A) /= Post(s, B).

Then Post(s, A/\B) =  φ

Best,
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/18c0b8b6-1fe6-40b8-8560-d808d6bc7dc6%40googlegroups.com.

-- 
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/4e8eaa89-0e5c-8d82-2982-105426e39f84%40gmail.com.


-- 
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+u...@googlegroups.com.
Reply all
Reply to author
Forward
0 new messages