I think there is a misunderstanding. First, the example given by Hillel doesn't have two processes but is just a sequential program (a while loop), so there can be no interleaving of instructions. Second, there is no tree structure of labels where lower-level labels are somehow controlled by higher-level ones. Labels indicate possible breakpoints in the execution of sequential code. The rewrite Hillel provided into unstructured code with goto statements makes this very explicit.StephanOn 17 Nov 2020, at 20:10, p.to...@xxxxxxxxxxxxxxxxx <p.to...@xxxxxxxxxxxxxxxxx> wrote:
Thanks for the answers,the example represents exactly what I meant for nested labels,so in the example, it is true to say that if I had two processes defined in that way:Reader:
while Cond do
skip;
B:
skip;
end while;
After:
skip;I can have interleaving of the labels "Reader" and "B" (defined as above) of the two processes, right?Il giorno lunedì 16 novembre 2020 alle 01:59:54 UTC+1 hwa...@gmail.com ha scritto: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;
On 11/15/2020 12:06 PM, Stephan Merz wrote:
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.to...@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+u...@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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/234AFF4D-1C65-4C50-AFB0-6D2D8402126A%40gmail.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/6c095a11-5272-4f95-b12a-3160b1e8d625n%40googlegroups.com.