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
--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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d1ec508d-f21e-4240-be68-a573b31a2744n%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.
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/42c9549d-db6a-4dff-b72d-a8efbd5ada79n%40googlegroups.com.