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

[tlaplus] what is wrong with this pluscal spec?

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


(* --algorithm foo


x = 0;

  x := x + 1;
  if x # 0
    assert TRUE;
      new_x = x + 1
      x := new_x;
    end with;
  end if;
end algorithm; *)




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.