Re: Interpreting the DieHarder error trace

[ston...@xxxxxxxxx]

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?