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

*From*: ston...@xxxxxxxxx*Date*: Sun, 28 May 2017 10:39:12 -0700 (PDT)*References*: <1b8021e4-4bfa-4d26-bddb-64cf28e4f27d@googlegroups.com> <1a901e44-2e43-4f52-ac55-07cce0b5e256@googlegroups.com> <ef1f5ae5-b1a2-4204-9f17-b85412b6b6d4@googlegroups.com> <58A6F070-9CCC-4654-AFC9-5C3708E1CD1C@gmail.com>

Thanks, that helps a great deal! ---rdf On Sunday, May 28, 2017 at 2:08:28 AM UTC-4, Stephan Merz wrote: > 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? > > > > --

**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 . . .

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

- Prev by Date:
**Re: Paramaterized Instantiation and Universal Quantification** - Next by Date:
**Re: Interpreting the DieHarder error trace** - Previous by thread:
**Re: [tlaplus] Re: Interpreting the DieHarder error trace** - Next by thread:
**Re: Interpreting the DieHarder error trace** - Index(es):