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.