[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: bal...@xxxxxxxxx*Date*: Fri, 27 Dec 2013 02:58:42 -0800 (PST)

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

**Follow-Ups**:**Re: Errors running euclid model from hyperbook***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] TLA+ Toolbox java exception** - Next by Date:
**Re: Errors running euclid model from hyperbook** - Previous by thread:
**Re: [tlaplus] TLA+ Toolbox java exception** - Next by thread:
**Re: Errors running euclid model from hyperbook** - Index(es):