I experienced this as well: I defined a procedure with a label (as required) and attempted to translate it. No matter what I did, the translator complained "A label may not appear in a macro." When I restarted the TLA+ Toolbox, the translator succeeded on the same spec.
On Saturday, November 24, 2018 at 3:04:09 PM UTC-5, rar...@xxxxxxxx wrote:
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!