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?
If so you'd have the same problem; you can't assign to queue twice. But now you could do something like this:
--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d1ec508d-f21e-4240-be68-a573b31a2744n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f1789ef3-97c1-41ec-9cf3-2effe3eeaaf0n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f1789ef3-97c1-41ec-9cf3-2effe3eeaaf0n%40googlegroups.com.
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.
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.