------------------------------- MODULE EUCLID -------------------------------
EXTENDS GCD, Integers,TLC
CONSTANT M,N
ASSUME {M, N} \subseteq Nat \ {0}
(***************************************************************************
--algorithm Euclid {
variables x \in 1..N, y \in 1..N, x0=x, y0=y;
{ while (x # y) { if (x < y) { y := y - x }
else { x := x - y }
};
};
assert (x = y) /\ (x = GCD(x0, y0))
}
***************************************************************************)
Translator reports "Expected "}" but found ";" line 11, column2
Is it a translator bug?
Tool kit version:
This is Version 1.7.1 of 31 December 2020 and includes:
- SANY Version 2.2 of 20 April 2020
- TLC Version 2.16 of 31 December 2020
- PlusCal Version 1.11 of 31 December 2020
- TLATeX Version 1.0 of 20 September 2017