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

[Stephan Merz <stepha...@xxxxxxxxx>]

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.