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  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.
 see section 2.7 of the PlusCal manual--
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.