[tlaplus] Use of labels in PlusCal

["p.to...@xxxxxxxxxxxxxxxxx" <p.tollot@xxxxxxxxxxxxxxxxx>]

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.