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

*From*: ston...@xxxxxxxxx*Date*: Sat, 27 May 2017 11:50:52 -0700 (PDT)*Cc*: ston...@xxxxxxxxx*References*: <1b8021e4-4bfa-4d26-bddb-64cf28e4f27d@googlegroups.com> <1a901e44-2e43-4f52-ac55-07cce0b5e256@googlegroups.com>

Yes, not posting the spec was definitely an error on my part (appears below) This is the section highlighted by the Toolbox when I double click the error trace \/ /\ \E j \in Jugs: \E k \in Jugs \{j}: LET poured == Min(injug[j] + injug[k], Capacity[k] - injug[k]) IN injug' = [injug EXCEPT ![j] = injug[j] - poured, ![k] = injug[k] + poured] I can see "mechanically" how that happens aka poured = 2. However looking at the specification, I would have thought that it was working in the domain of Nat \ {0} Therefore, wouldn't have thought the value of -2 could be successfully assigned and an error would have been signaled before the Invariant was evaluated. It also appears to me (I'm not confident that I'm reading the spec correctly) that there's an error in the spec that doesn't specify a from-to relationship for the pour, so the pour occurs from a jug with nothing in it. Again, I'm not sure that either of these interpretations are appropriate & am trying to get aligned with how tlaplus actually works. _____________spec____________________ ----------------------------- MODULE DieHarder ----------------------------- EXTENDS Integers Min(m,n) == IF m<n THEN m ELSE n CONSTANTS Goal, Jugs, Capacity ASSUME /\ Goal \in Nat /\ Capacity \in [Jugs -> Nat \ {0}] (*************************************************************************** --algorithm DieHarder { variable injug = [j \in Jugs |-> 0 ]; { while (TRUE) {either with (j \in Jugs) \* fill jug j {injug[j] := Capacity [j]} or with (j \in Jugs) \* empty jug j {injug[j] := 0} or with (j \in Jugs, k \in Jugs \{j}) \* pour from jug j into jug k { with ( poured = Min(injug[j] + injug[k], Capacity[k] - injug[k])) { injug[j] := injug[j] - poured || injug[k] := injug[k] + poured } } } } } ***************************************************************************) \* BEGIN TRANSLATION VARIABLE injug vars == << injug >> Init == (* Global variables *) /\ injug = [j \in Jugs |-> 0 ] Next == \/ /\ \E j \in Jugs: injug' = [injug EXCEPT ![j] = Capacity [j]] \/ /\ \E j \in Jugs: injug' = [injug EXCEPT ![j] = 0] \/ /\ \E j \in Jugs: \E k \in Jugs \{j}: LET poured == Min(injug[j] + injug[k], Capacity[k] - injug[k]) IN injug' = [injug EXCEPT ![j] = injug[j] - poured, ![k] = injug[k] + poured] Spec == Init /\ [][Next]_vars \* END TRANSLATION ============================================================================= On Saturday, May 27, 2017 at 10:19:25 AM UTC-4, Leslie Lamport wrote: > You are asking for an explanation of why your specification causes TLC to produce a particular output without showing us your specification. I presume that's why no one bothered to answer your question. If you double-click on the line in the error trace between the last two states, the Toolbox will show you what part of the next-state relation permitted the step from state 4 to state 5. Understanding why that formula allowed that step should allow you to answer your question yourself. > > On Wednesday, May 24, 2017 at 1:27:05 PM UTC-7, stonebits@... wrote:My "value" error trace when there's a solution (the /= Goal is violated) is the following > > State (num = 1) > > (small :> 0 @@ big :> 0) > > > > State (num = 2) > > (small :> 0 @@ big :> 5) > > > > State (num = 3) > > (small :> 3 @@ big :> 2) > > > > State (num = 4) > > (small :> 0 @@ big :> 2) > > > > State (num = 5) > > (small :> -2 @@ big :> 4) > > > > I'm confused as to why "small" is ever negative as it is in state 5 -- any ideas?

**Follow-Ups**:**Re: [tlaplus] Re: Interpreting the DieHarder error trace***From:*Stephan Merz

**References**:**Interpreting the DieHarder error trace***From:*ston . . .

**Re: Interpreting the DieHarder error trace***From:*Leslie Lamport

- Prev by Date:
**Re: Modeling memory barriers** - Next by Date:
**Re: [tlaplus] Re: Interpreting the DieHarder error trace** - Previous by thread:
**Re: Interpreting the DieHarder error trace** - Next by thread:
**Re: [tlaplus] Re: Interpreting the DieHarder error trace** - Index(es):