Pluscal able to translate my spec. However, after translation, the spec status becomes error

[Charly Abraham]

Pluscal code before transalation
https://ibb.co/hrLw5H

Pluscal code after translation

https://ibb.co/fy8G5H


Raw code pluscal code


----------------MODULE mutex------------------------------------------------
EXTENDS Naturals, TLC
CONSTANT N
(*--algorithm FastMutex {
variables x, y = 0, b = [ i \in 1..N |-> FALSE];
process (proc \in 1..N)
variable j;
{ ncs: while (TRUE) {
skip; \* The non critical section
start: b[self] := TRUE;
11: x:= self;
12: if (y /= 0) { l3: b[self] := FALSE;
l4: await y = 0;
goto start };
l5: y:= self;
l6: if(x /= self) { l7: b[self] := FALSE;
j := 1;
l8: while (j <= N) { await ~b[j];
j := j + 1;
};
l9: if (y /= self) { l10: await y = 0;
goto start }};
cs: skip; \* The critical section
l11: y:=0;
l12: b[self]:= FALSE; }}}
*)

===========================================================================

[Stephan Merz]

Don't use numbers as labels, rename 11 and 12 to l1 and l2.

Stephan

> --
> 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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Markus Kuppe]

Hi,

I filed an enhancement request to improve error reporting:
https://github.com/tlaplus/tlaplus/issues/151

Cheers
Markus