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

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

You are right in that my example is wrong. In the real project there were two different macros each one writing to a different queue. But this didn't work:

process (id \in {1,2,3}) {
    begin:  send1(ch1, "hello") ||
            send2(ch2, "hi");

    (...)

}

So I had to fuse the two sendings inside a macro. But then I tried to multiple-assign a macro call with a normal variable assignment and it didn't work either:

process (id \in {1,2,3}) {
    begin:  send1(ch1, "hello") ||
            x := 2;

    (...)

}

It is really inconvenient that macros are not simply replaced textually. There seems to be some other translation logic going on.  I've added way more states than needed after having been forced by the translator to introduce tags before and after the macro calls.

On Tuesday, November 7, 2023 at 3:11:03 AM UTC+1 Hillel Wayne wrote:

I think the problem here is that send is assigning to queue, so send || send assigns to queue twice (which isn't valid PlusCal). Also the snippet here isn't sending two messages, it's clobbering the first message. Did you instead mean this?

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

If so you'd have the same problem; you can't assign to queue twice. But now you could do something like this:

macro send(f) {
    queue := [ch \in DOMAIN f |-> Append(queue[ch], f[ch])] @@ queue;
}

Then write the process as send(ch1 :> "hello" @@ ch2 :> "hi").

H

On 11/6/2023 5:33 PM, J.D. Meadows wrote:

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

-- 
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/d1ec508d-f21e-4240-be68-a573b31a2744n%40googlegroups.com.