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