| 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 <tr1pl3.d3v@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?
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?
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.
--
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/5523c23b-7f8e-4856-a328-542aaa0b1d5dn%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/43C1FDC0-3194-4F69-A38A-0DAB12A87857%40gmail.com.
|