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

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.