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

*From*: Brian Beckman <bc.be...@xxxxxxxxx>*Date*: Fri, 14 Feb 2014 18:09:49 -0800 (PST)

Following the instructions on page 39 of main.pdf, concerning an assert in Euclid's algorithm,

I find that the PlusCal translator, when processing this:

--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 (pc = "Done") => (x = y) /\ (x = GCD(x0, y0));

} }

produces (keeping only the relevant part)

...

ELSE /\ Assert((pc = "Done") => (x = y) /\ (x = GCD(x0, y0)),

"Failure of assertion at line 16, column 7.")

/\ pc' = "Done"

/\ UNCHANGED << x, y >>

...

Notice the Assert is before the update of pc (via pc'). Doesn't this mean that the Assert never sees

(pc = "Done"), so its predicate is vapidly true, i.e., it doesn't actually check the stuff we want,

namely that (x=y)/\(x=GCD(x0,y0))?

I found this while following the instructions and attempting to change the consequent of

(pc = "Done")

to something false, and finding that TLA+ never produced an error.

I find that the PlusCal translator, when processing this:

--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 (pc = "Done") => (x = y) /\ (x = GCD(x0, y0));

} }

produces (keeping only the relevant part)

...

ELSE /\ Assert((pc = "Done") => (x = y) /\ (x = GCD(x0, y0)),

"Failure of assertion at line 16, column 7.")

/\ pc' = "Done"

/\ UNCHANGED << x, y >>

...

Notice the Assert is before the update of pc (via pc'). Doesn't this mean that the Assert never sees

(pc = "Done"), so its predicate is vapidly true, i.e., it doesn't actually check the stuff we want,

namely that (x=y)/\(x=GCD(x0,y0))?

I found this while following the instructions and attempting to change the consequent of

(pc = "Done")

to something false, and finding that TLA+ never produced an error.

**Follow-Ups**:**Re: position of PlusCal assert in Euclid from Hyperbook?***From:*Leslie Lamport

**Re: position of PlusCal assert in Euclid from Hyperbook?***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Toolbox not finding pdflatex -- Mac** - Next by Date:
**Re: position of PlusCal assert in Euclid from Hyperbook?** - Previous by thread:
**Re: [tlaplus] first steps in TLA - recursive functions don't work** - Next by thread:
**Re: position of PlusCal assert in Euclid from Hyperbook?** - Index(es):