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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Fri, 27 Dec 2013 09:25:33 -0800 (PST)*Cc*: bal...@xxxxxxxxx*References*: <ab5ecc00-9bbf-470a-8644-66a8cbb2bbba@googlegroups.com>

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.

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

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

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:

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

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.

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.

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

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

**References**:**Errors running euclid model from hyperbook***From:*bal . . .

- Prev by Date:
**Errors running euclid model from hyperbook** - Next by Date:
**Re: [tlaplus] Re: my first tla program** - Previous by thread:
**Errors running euclid model from hyperbook** - Next by thread:
**Confusion in TLA+ model for access control** - Index(es):