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