[tlaplus] Macros don't compose with the parallel assignment operator

["J.D. Meadows" <tr1pl3.d3v@xxxxxxxxx>]

I've defined this helper macro in my PlusCal (C-syntax) algorithm:

macro send(channel, msg) {    
    queue := Append(channel, msg)
}

In my initial step inside my processes I need to send two messages. But for now I want to send both atomically, without introducing additional labels. I thought of using the '||' operator, and thus I didn't add a semicolon in the sentence inside the macro, so that I could do this:

process (id \in {1,2,3}) {
    begin:  send(ch1, "hello") ||
            send(ch2, "hi");
   
    loop:   while(TRUE){                
                skip;
            }        
}

But the translator complains saying that a ';' should go instead of the '||'.

But if I do that then the translator gives an error saying that I should put a label inside the macro. Which of course it is forbidden, as macros can't contain labels. 

After losing a lot of time on this circular parsing error I realised that what the translator wants is that I put a label on the second send. But that has implications. I want to compose both assignments, which is totally possible in non-macro code. Eg.:

x := 1 || y := 2;

What I really need is a simple "text replacement" macro previous to the PlusCal to TLA+ translation. I don't even need multi-line macros for this project, just something like C's defines, or aliases in other programming languages.

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7071d762-b363-45de-8b20-ab20c8edc228n%40googlegroups.com.