[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

> 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. 

On Friday, November 10, 2023 at 8:48:39 AM UTC+1 Stephan Merz wrote:
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


On 9 Nov 2023, at 20:59, J.D. Meadows <tr1pl...@xxxxxxxxx> wrote:

> 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.

On Thursday, November 9, 2023 at 6:06:01 PM UTC+1 Hillel Wayne wrote:

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

On 11/9/2023 6:47 AM, J.D. Meadows wrote:
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 :)
On Wednesday, November 8, 2023 at 4:31:58 PM UTC+1 Hillel Wayne wrote:
Can you provide a complete spec I can look at?

On Wed, Nov 8, 2023, 7:17 AM J.D. Meadows <tr1pl...@xxxxxxxxx> wrote:
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.


On Wednesday, November 8, 2023 at 6:22:50 AM UTC+1 Hillel Wayne wrote:
If the macro isn't modifying x, does composing them with `;` work?

On Tue, Nov 7, 2023, 6:17 PM J.D. Meadows <tr1pl...@xxxxxxxxx> wrote:
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+u...@xxxxxxxxxxxxxxxx.
--
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/f1789ef3-97c1-41ec-9cf3-2effe3eeaaf0n%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+u...@xxxxxxxxxxxxxxxx.

--
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.

--
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/d59617c7-3e6f-43e9-9b2b-98c13dca0223n%40googlegroups.com.