Hi Bala,
First of all, I apologize for the lack of a helpful error message.
TLC's error reporting should be improved. Improving it is a project
that someone familiar with Java could do in a few weeks. We would
welcome a volunteer.
Now to answer your question of how to go about debugging the problem.
The error message said that evaluating the invariant
(pc = "Done") => (x = y) /\ (x = GCD(x0, y0))
failed. You should first figure out what part of the invariant TLC
couldn't evaluate. You do that by removing pieces of the invariant and trying
again. For example, with experimentation you might have found that
TLC was able to evaluate the invariant
(pc = "Done") => (x = y) /\ (x = <<x0, y0>>[2])
(It would have reported that it wasn't an invariant, but not failure
to evaluate the invariant.) This would have told you that it failed
trying to evaluate GCD. So, you would have had it just try to evaluate
GCD--for example, by putting GCD(22, 33) in the Evaluate Constant
_expression_ part of the Model Checking Results page. This would have
produced the following error:
The `Evaluate Constant _expression_� section�s evaluation failed.
Attempted to enumerate { x \in S : p(x) } when S:
Int
is not enumerable
This tells you that to evaluate GCD, TLC has to enumerate the elements
in the set Int, which it can't do because Int is an infinite set.
This should have led you to re-read the hyperbook section, which will
reveal that you failed to follow the instructions to make the TLC
model substitute a finite set of integers for Int.
----
I'm afraid that, until TLC's error reporting is improved, tracking
down the source of an error may require this kind of detective work.
But don't let this discourage you. With experience, you'll quickly
spot most such mistakes and will rarely have to puzzle out the proximate
cause of an error.
Leslie
On Friday, December 27, 2013 2:58:42 AM UTC-8, bal...@xxxxxxxxx wrote:
Hi all,I am running the Eculid model for computing GCD from the hyperbook and facing errors. The model I am using is from the hyperbook and I have reproduced it below [1]. The error is happening when I run the second version of the model mentioned in page 38. I cloned the second model and added a new invariant (pc = "Done") => (x = y) /\ (x = GCD(x0, y0)) instead of PartialCorrectness. That is failing to execute with the error: Evaluating invariant (pc = "Done") => (x = y) /\ (x = GCD(x0, y0)) failed.
How do I go about debugging this?
Thanks,
Bala.
[1] Model
------------------------------- MODULE Euclid -------------------------------
EXTENDS GCD, Integers
CONSTANTS M, N
ASSUME /\ M \in Nat \ {0}
/\ N \in Nat \ {0}(***************************************************************************
--algorithm Euclid {
variables x \in 1..M, y \in 1..N, x0 = x, y0 = y;
{
while (x # y) {
if (x < y) {y := y - x}
else {x := x - y}
}
}
} ***************************************************************************)
PartialCorrectness ==
(pc = "Done") => (x = y) /\ (x = GCD(M, N))