Re: [tlaplus] Pluscal able to translate my spec. However, after translation, the spec status becomes error

[Stephan Merz <stepha...@xxxxxxxxx>]

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

Stephan

> On 18 Mar 2018, at 08:50, Charly Abraham <char...@xxxxxxxxx> wrote:
> 
> 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; }}}
> *)
> 
> ===========================================================================
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.