Macros don't compose with the parallel assignment operator

[J.D. Meadows]

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.

[Hillel Wayne]

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

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

[J.D. Meadows]

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.

[Hillel Wayne]

If the macro isn't modifying x, does composing them with `;` work?

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d1ec508d-f21e-4240-be68-a573b31a2744n%40googlegroups.com.

[J.D. Meadows]

No, I've tried multiple combinations of adding ';' and nothing worked. I had to add a tag to separate the macro call from the other assignment.

[Stephan Merz]

For me, separating a send defined in a macro from an unrelated assignment works using `;' (see below), but using `||' produces a syntax error.

Stephan

----- MODULE PlusCalTest ----

EXTENDS Integers, Sequences

(*

--algorithm Test {

variables c = << >>, x = 0;

macro send(ch, msg) { ch := Append(ch, msg) }

{

start:

send(c, x);

x := x+1

} }

*)

\* BEGIN TRANSLATION (chksum(pcal) = "2813a0ba" /\ chksum(tla) = "395c2ea4")

VARIABLES c, x, pc

vars == << c, x, pc >>

Init == (* Global variables *)

/\ c = << >>

/\ x = 0

/\ pc = "start"

start == /\ pc = "start"

/\ c' = Append(c, x)

/\ x' = x+1

/\ pc' = "Done"

(* Allow infinite stuttering to prevent deadlock on termination. *)

Terminating == pc = "Done" /\ UNCHANGED vars

Next == start

\/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

=============================

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f1789ef3-97c1-41ec-9cf3-2effe3eeaaf0n%40googlegroups.com.

[Hillel Wayne]

Can you provide a complete spec I can look at?

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f1789ef3-97c1-41ec-9cf3-2effe3eeaaf0n%40googlegroups.com.

[J.D. Meadows]

Hillel, you don't need my complete spec, Stephan's sample can already show the problem with a little change. For instance, this doesn't compile:

-------------------------------- MODULE Test --------------------------------

EXTENDS Integers, Sequences

(*
--algorithm Test {
    variables c = << >>, x = 0;
    macro send(ch, msg) { ch := Append(ch, msg) }

{
start:

    x := x+1 ||
    send(c,2);
} }

and neither does this:

-------------------------------- MODULE Test --------------------------------

EXTENDS Integers, Sequences

(*
--algorithm Test {
    variables c = << >>, x = 0;
    macro send(ch, msg) { ch := Append(ch, msg) }

{
start:

    send(c,2) ||
    x := x+1;
} }

There is no reason we can't do this, as they are different variables and can be updated as part of the same step. It will also be benefitial in reducing the number of states.

Sorry about the C-syntax, I know from your book and site that you are a Pascal guy :)

[Hillel Wayne]

Hi,

I need a spec to understand your problem here:

> No, I've tried multiple combinations of adding ';' and nothing worked. I had to add a tag to separate the macro call from the other assignment.

in the Test you provided, you can compose them with `;`:

start:
    x := x+1;
    send(c,2);

That compiles just fine for me.

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/42c9549d-db6a-4dff-b72d-a8efbd5ada79n%40googlegroups.com.

[J.D. Meadows]

> in the Test you provided, you can compose them with `;`:

Actually that compiles and generates the correct TLA+ code, with both updates in a single action. However the '||' operator is more explicit to what I was trying to do.

I think the problem is that in my bigger spec I was calling two different macros inside the main block that under the hood "mutated" the same queue, like you said. And that produces the puzzling "label required inside the macro" error, which can only be solved by adding a label at the macro invocation. To be more precise, my code contained a 'read' macro call followed by a 'write' macro call. Since in TLA+ reading from a queue requires reassigning the queue to the same queue without one element, it ammounts to writing. My programmer mindset didn't allow me to see beyond the macro names :).

That error btw could be more clear, something like "you can't update the same variable twice in the same action". Right now the parser demands a tag inside the macro, which is illegal.

[Hillel Wayne]

Actually that compiles and generates the correct TLA+ code, with both updates in a single action. However the '||' operator is more explicit to what I was trying to do.

In general, you should only use the `||` operator when you want to update two parts of the same function in the same label. Even the example given in the pcal manual, swapping two values with u := v || v := u, is clearer if you use a with statement:

with tmp = u {
  u := v;
  v := tmp;
}

Otherwise, ; is "almost always" does everything simultaneously, with different steps in different labels. I say "almost always" because there's one exception: after you assign to a variable x, later instructions in the same label will use x' instead. IE if we do

foo:
  \* x = 1
  x := x + 1;
  y := x + 1;

Then y will be assigned to 3, not 2. I think there's some weirdness with how this interacts with defined operators, though, which I think can be a bit of a pitfall.

That error btw could be more clear, something like "you can't update the same variable twice in the same action". Right now the parser demands a tag inside the macro, which is illegal.

Yeah, I can definitely see why that'd be frustrating! I think there's a lot of room to improve the error messages we give. 

...Oh, also, since I don't think I gave you satisfactory explanation for this:

There is no reason we can't do this [compose macros with ||], as they are different variables and can be updated as part of the same step.

I agree it'd be nicer if macros automatically composed with ||. I don't work on the core language or the tooling, but I'm guessing it would be infeasible. That's because macros can be bigger than a single assignment:

macro foo {
   if some_conditional {
     with x \in set {
        seq[1] := x || seq[2] := seq[1];
     };
     z := FALSE;
     print q;
}

You can ||-compose two assignments but not a block and an assignment. Now it might be possible to check if the macro is a single assignment and in that case allow ||, but I think that would cause more confusion to people in the long-run.

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5523c23b-7f8e-4856-a328-542aaa0b1d5dn%40googlegroups.com.

[Stephan Merz]

This is somewhat tangential to your question about macros, but I actually prefer modeling network operations using a more "functional" style based on definitions where each operation yields the resulting network. This makes it easy to have several operations within a single step. Here is a contrived example:

--algorithm Test {

variables network = [p \in Proc |-> << >>];

define {

send(net, to, msg) == [net EXCEPT ![to] = Append(@, msg)]

recv(net, from) == <<Head(net[from]), [net EXCEPT ![from] = Tail(@)]>>

}

process (p \in Proc) {

run: either {

with (d \in Data, dest \in Proc) {

network := send(network, dest, d)

}

}

or {

await (Len(network[self]) > 0);

with (rcv = recv(network, self), d = rcv[1], _net = rcv[2]) {

\* handle received message d

with (reply \in Data \ {d}, dest \in Proc) {

network := send(_net, dest, reply)

}

}

}

}

}

In the "or" branch, the process performs both a receive and a send operation in a single atomic step. However, I'll admit that the definition of recv using a macro is more satisfactory, in particular because it can include the await statement, whereas it has to be written separately in this style of modeling communication. Also, the final update to the network needs to be an assignment whereas intermediate updates use "with" statements (corresponding to LET in TLA+) introducing auxiliary identifiers.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5523c23b-7f8e-4856-a328-542aaa0b1d5dn%40googlegroups.com.

[J.D. Meadows]

> I actually prefer modeling network operations using a more "functional" style based on definitions where each operation yields the resulting network.

That is a nice workaround.