Use of labels in PlusCal

[p.to...@studenti.unipi.it]

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

[Stephan Merz]

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

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5f1f5524-8cd7-446f-b454-66db181c998an%40googlegroups.com.

[Hillel Wayne]

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; 

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/234AFF4D-1C65-4C50-AFB0-6D2D8402126A%40gmail.com.

[p.to...@studenti.unipi.it]

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?

[Stephan Merz]

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.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6c095a11-5272-4f95-b12a-3160b1e8d625n%40googlegroups.com.

[p.to...@studenti.unipi.it]

Ok now is clear, 

yes i'm not a good english writer, what I meant was if I had two processes each of one defined as in the example...

Thanks for the answers 

Pietro

[Michael Leuschel]

Hi,

I just downloaded and installed TLAPS 1.4.5 on macOS Mojave using the latest TLA+ Toolbox 1.7.0.

I wanted to try out TLAPS on some simple maths theorems and chose SimpleMath.tla (that comes with TLC, I think).

However, there was the error message below.

When clicking on the Link to submit the bug report and then clicking on “Bug tracker for TLAPS/tlapm" I get an error “requested URL was not found”.

Hence my message to this group, maybe somebody knows what is happening.

I was able to start TLAPS for the DieHard.tla example (but it has not theorems).

Greetings,

Michael

[Michael Leuschel]

Hi,

I think I found the problem:, line 76 of SimpleMath.tla contains a comment that TLAPS does not seem to like
(*{a, b} \in {{a, b}, c, {d, e}}*)

Greetings,
Michael

> <Screenshot 2020-11-19 at 13.23.59.png>
>
> <Screenshot 2020-11-19 at 13.31.39.png>

[Stephan Merz]

Hi Michael,

thanks for reporting this. No idea why the TLAPS parser get confused by this, even more so in a comment. Could you please file an issue at https://github.com/tlaplus/tlapm/issues?

Regards,

Stephan

On 19 Nov 2020, at 13:37, Michael Leuschel <michael....@gmail.com> wrote:

Hi,

I think I found the problem:, line 76 of SimpleMath.tla contains a comment that TLAPS does not seem to like
(*{a, b} \in {{a, b}, c, {d, e}}*)

Greetings,
Michael

On 19 Nov 2020, at 13:33, Michael Leuschel <michael....@gmail.com> wrote:

Hi,

I just downloaded and installed TLAPS 1.4.5 on macOS Mojave using the latest TLA+ Toolbox 1.7.0.
I wanted to try out TLAPS on some simple maths theorems and chose SimpleMath.tla (that comes with TLC, I think).
However, there was the error message below.
When clicking on the Link to submit the bug report and then clicking on “Bug tracker for TLAPS/tlapm" I get an error “requested URL was not found”.
Hence my message to this group, maybe somebody knows what is happening.

I was able to start TLAPS for the DieHard.tla example (but it has not theorems).

Greetings,
Michael

<Screenshot 2020-11-19 at 13.23.59.png>

<Screenshot 2020-11-19 at 13.31.39.png>

-- 
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...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/F828AFD2-EAD5-460B-9B57-08762EB87D92%40gmail.com.

[Stephan Merz]

P.S.: The error disappears when you insert a space after '(*' – not that this is expected behavior. -s