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

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 18.03.2018 09:08, Stephan Merz wrote:
> 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; }}}
>> *)
>>
>> ===========================================================================
Hi,

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

Cheers
Markus