Interpreting the DieHarder error trace

82 views
Skip to first unread message

ston...@gmail.com

unread,
May 24, 2017, 4:27:05 PM5/24/17
to tlaplus
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?

Leslie Lamport

unread,
May 27, 2017, 10:19:25 AM5/27/17
to tlaplus, ston...@gmail.com
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.

ston...@gmail.com

unread,
May 28, 2017, 1:32:12 AM5/28/17
to tlaplus, ston...@gmail.com
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
=============================================================================

Stephan Merz

unread,
May 28, 2017, 2:08:28 AM5/28/17
to tla...@googlegroups.com
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
> --
> 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

Leslie Lamport

unread,
May 28, 2017, 2:31:44 AM5/28/17
to tlaplus, ston...@gmail.com
This incorrect version of DieHarder is in the HyperBook.  My apologies for being so careless.  Thank you for pointing it out.  I will correct it when I get a chance--which will not be right away.  Meanwhile, finding a correct algorithm is a good exercise.

It is disheartening that the error was not discovered until now.  It seems to indicate that there is no point in my doing further work on the HyperBook.

Leslie

ston...@gmail.com

unread,
May 28, 2017, 2:04:33 PM5/28/17
to tlaplus, ston...@gmail.com
Well, in fairness to previous readers, the result is as expected, and my prior experience of having done two global optimizers makes me sensitive to the visibility of intermediate results (especially in the presence of an error condition).

ston...@gmail.com

unread,
May 28, 2017, 2:04:33 PM5/28/17
to tlaplus
Thanks, that helps a great deal!

---rdf

fl

unread,
May 29, 2017, 1:26:08 PM5/29/17
to tlaplus, ston...@gmail.com
 
It is disheartening that the error was not discovered until now.

Personnaly I learned TLA+ by reading "Specifying Systems". But I suppose that if people knows how to use TLA+ they have read something:
either the "HyperBook" or "Specifying Systems". Simply examples or exercices are rarely worked out thoroughly. 

-- 
FL
Reply all
Reply to author
Forward
0 new messages