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

*From*: Shiyao MA <i@xxxxxxxxx>*Date*: Sun, 22 Sep 2019 19:35:48 -0700 (PDT)*References*: <49ec89c4-e18a-48fa-bb0b-2b499379fdee@googlegroups.com> <a970adcf-3791-4835-b6c8-ac024b5c9cef@googlegroups.com> <277f303e-5cfe-8607-6789-99686a50099c@gmail.com> <18c0b8b6-1fe6-40b8-8560-d808d6bc7dc6@googlegroups.com> <4e8eaa89-0e5c-8d82-2982-105426e39f84@gmail.com> <DD701347-831E-4195-BA20-8DBA94DDBB95@gmail.com>

Hi Merz,

-- What I understand from Hillel's reply is that,

If Post(s, A) /= Post(s, B).

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

Best,

On Sunday, 22 September 2019 14:35:13 UTC+8, Stephan Merz wrote:

On Sunday, 22 September 2019 14:35:13 UTC+8, Stephan Merz wrote:

Let me rephrase Hillel's intuition: suppose we have a next-state relationNext == A \/ B \/ ...Given state s, TLC will process action A by computing the setPost(s,A) == { t : (s,t) |= A } [1]Clearly, we have thatPost(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.On 20 Sep 2019, at 06:53, Hillel Wayne <hwa...@xxxxxxxxx> wrote:I'm having some trouble coming up with a valid spec where that would matter. You're saying that

OP1,OP2, andOP1 /\ OP2are 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.

On 9/19/19 10:01 PM, Shiyao MA wrote:

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

VoteForspecifiesmaxBal', andIncreaseMaxBalspecifiesmaxBal', then they can only be true that the same time if there is some value formaxBal'that satisfies both actions.Given TLC isn't giving you an error, I'm guessing you also have

UNCHANGED votesinIncreaseMaxBal? Then they definitely both can't be true at the same time, asVoteForwould specify thatvoteschanges andIncreaseMaxBaldoes 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...@xxxxxxxxxxxxxxxx.

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/396b14f6-bfa6-4a25-86a4-06099ecc80e0%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] How does TLC expand search?***From:*Stephan Merz

**References**:**[tlaplus] Re: How does TLC expand search?***From:*Shiyao MA

**Re: [tlaplus] Re: How does TLC expand search?***From:*Hillel Wayne

**Re: [tlaplus] Re: How does TLC expand search?***From:*Shiyao MA

**Re: [tlaplus] Re: How does TLC expand search?***From:*Hillel Wayne

**Re: [tlaplus] How does TLC expand search?***From:*Stephan Merz

- Prev by Date:
**[tlaplus] non-atomic Peterson in TLA+** - Next by Date:
**Re: [tlaplus] non-atomic Peterson in TLA+** - Previous by thread:
**Re: [tlaplus] How does TLC expand search?** - Next by thread:
**Re: [tlaplus] How does TLC expand search?** - Index(es):