# Errors running euclid model from hyperbook

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