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

*From*: Stephan Merz <stepha...@xxxxxxxxx>*Date*: Sun, 28 May 2017 08:08:26 +0200*References*: <1b8021e4-4bfa-4d26-bddb-64cf28e4f27d@googlegroups.com> <1a901e44-2e43-4f52-ac55-07cce0b5e256@googlegroups.com> <ef1f5ae5-b1a2-4204-9f17-b85412b6b6d4@googlegroups.com>

Your ASSUME clause restricts the constant capacities of the jugs to be positive integers, but nothing is said about the values of the variable injury. In fact, TLA+ is an untyped formalism, and there is no way to rely on a type declaration for restricting the values of variables. I do not understand the line with ( poured = Min(injug[j] + injug[k], Capacity[k] - injug[k])) How can you pour more than the contents of jug j from j to k? Hope this helps, Stephan > On 27 May 2017, at 20:50, ston...@xxxxxxxxx wrote: > > 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? > > -- > 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...@xxxxxxxxxxxxxxxx. > To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. > Visit this group at https://groups.google.com/group/tlaplus. > For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**Re: [tlaplus] Re: Interpreting the DieHarder error trace***From:*ston . . .

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

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

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

- Prev by Date:
**Re: Interpreting the DieHarder error trace** - Next by Date:
**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):