To build on what Stephan said, if you see
Reader:
while Cond do
skip;
B:
skip;
end while;
After:
skip;
It should have the same behavior as
Reader:
if ~Cond then goto After; end if;
skip;
B:
skip;
goto Reader;
After:
skip;
Hi,--
on your first question: what do you mean by "nested labels"?
Concerning the second question, while the overall idea is that the statements in between two labels are executed atomically, the PlusCal translator imposes some restrictions where labels must (and must not) appear [1] in order to obtain a simple correspondence between the PlusCal algorithm and the TLA+ specification that it is translated to. For example, a while statement has to be labeled, and (assuming that there is no other label inside the loop body) every execution of the loop body will be executed atomically. Think of the label as labeling the loop condition rather than the entire loop.
I guess the rationale is that it is unrealistic for all iterations of a loop to execute in an atomic step. Note however that TLA+ operators give you a lot of expressiveness to define complex expressions, including those that you would use a loop for in a standard programming language. For example, you can easily define a multicast operator that sends a message to a set of recipients rather than writing a loop that sends the message to each destination process one by one.
Stephan
[1] see section 2.7 of the PlusCal manual--
On 15 Nov 2020, at 18:48, p.to...@xxxxxxxxxxxxxxxxx <p.tollot@xxxxxxxxxxxxxxxxx> wrote:
Hi, i'm new to TLA+ and PlusCal, i'm learning how to use labels, i have read that the content of a label is executed atomically in one step by the model checker, my doubts are about nested labels. How nested labels deal with the fact that the content is executed atomically, that is what sanse would have to have label nested? The other doubt is about cycles and processes, for instance in the case of the while cycle as body of a process like this:process reader = "reader"
begin
Read:
while TRUE do
...
end while;
end process;
The behaviour that i would expect is that the whole cycle is executed and ended in a single step of the model checker while what i get is that only a single iteration is executes as a step. I am missing something?
Thanks
--
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/5f1f5524-8cd7-446f-b454-66db181c998an%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/234AFF4D-1C65-4C50-AFB0-6D2D8402126A%40gmail.com.