Re: [tlaplus] Re: "A label may not appear in a macro"

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

On 24.11.18 10:30, Richard Artoul wrote:
> On Saturday, November 24, 2018 at 1:28:56 PM UTC-5, Richard Artoul wrote:
>> I'm working my way through the hyperbook and trying to solve the 1-bit clock alternation problem.
>>
>> The code I have is:
>>
>> ```pluscal
>> ------------------------- MODULE TickTockAlternate -------------------------
>> EXTENDS TLC
>>
>> (***************************************************************************
>> --algorithm TickTockAlternate 
>>     variable b = 0;
>>         
>>     process Tick = 0
>>     begin   
>>         while TRUE do
>>             await b = 0;
>>             b := 1;
>>         end while; 
>>     end process
>>     
>>     process Tock = 1
>>     begin 
>>         while TRUE do
>>             await b = 1;
>>             b := 0;
>>         end while;
>>     end process
>>     
>> end algorithm
>>  ***************************************************************************)
>> =============================================================================
>> ```
>>
>> When I try to run the PlusCal translator on this code I receive the error: `A label may not appear in a macro`, however, when I modify the code to add a label as below:
>>
>>
>> ```pluscal
>> ------------------------- MODULE TickTockAlternate -------------------------
>> EXTENDS TLC
>>
>> (***************************************************************************
>> --algorithm TickTockAlternate 
>>     variable b = 0;
>>         
>>     process Tick = 0
>>     begin   
>>         t0: while TRUE do
>>             await b = 0;
>>             b := 1;
>>         end while; 
>>     end process
>>     
>>     process Tock = 1
>>     begin 
>>         t1: while TRUE do
>>             await b = 1;
>>             b := 0;
>>         end while;
>>     end process
>>     
>> end algorithm
>>  ***************************************************************************)
>> =============================================================================
>>
>> ```
>>
>> I receive the error: `A label may not appear in a macro`
>>
>> I assume I'm just making some kind of silly mistake, but I can't figure it out for the life of me
> 
> Sorry, to clarify the first error message is:
> 
> ```
> Missing labels at the following locations:
>     line 10, column 9
>     line 18, column 9
> ```
> 

Hi Richard,

it is hard to tell what is going on but your PlusCal algorithm with
labels translates just fine here when copied verbatim.  I suggest to
create a new specification and start anew.

If possible, please first zip up the directory of the broken
specification and send it to me privately.  You will find the location
of the directory by selecting the TickTockAlternate spec in the Spec
Explorer and hitting Alt+Enter to open the properties.

Thanks
Markus