Errors running euclid model from hyperbook

[bal...@xxxxxxxxx]

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