[tlaplus] what is wrong with this pluscal spec?

["'Michal Jaszczyk' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

Below is a distilled version of something I ran into while writing my spec. PlusCal complains that a label is missing. It is a minimal reproduction, in the sense that changing almost anything is enough to fix this:

* insert a label before the `if` statement

* insert a label after the `assert` statement

* remove the `assert` statement

* replace `with` statement with a simpler `x := x + 1`

I believe that the spec is correct with respect to the rules about where labels are required. This is corroborated by the fact that simply removing the assert is enough to fix it.

What is going on - am I doing something wrong, or is this a bug in PlusCal?

My PlusCal version is: pcal.trans Version 1.9 of 10 July 2019

---- MODULE foo ----

EXTENDS TLC

(* --algorithm foo

variables

x = 0;

begin
 A:
  x := x + 1;
  if x # 0
  then
 B:
    assert TRUE;
    with
      new_x = x + 1
    do
      x := new_x;
    end with;
  end if;
end algorithm; *)

====

Cheers,

M.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c00ed59e-10f5-46be-a988-a75022b820e2n%40googlegroups.com.