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

[rar...@xxxxxxxx]

On Saturday, November 24, 2018 at 2:12:39 PM UTC-5, Markus Alexander Kuppe wrote:
> 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

Hey Markus,

I ended up solving the issue by just restarting the TLA+ toolbox, maybe I just got it into a weird state. Thanks for your help!