Re: [tlaplus] Re: Interpreting the DieHarder error trace

[ston...@xxxxxxxxx]

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?
> > 
> > --