Understanding relation between pluscal and tla

[Shiyao MA]

Hi.  This post contains three *correlated* questions from the same code snippet attached below.

Q1. Model checking the program gives 5 states and 3 distinct ones. What are the exact states?

Q2. The checker's state graph output is here: https://imgur.com/a/p81e77M           .  Why is there a loop (the green arrow)?

Q3. The tla translated code for the with statement is:

    with f \in Flags do
         flags[f] := TRUE;
    end with;

Lbl_1 == /\ pc = "Lbl_1"
         /\ \E f \in Flags:
              flags' = [flags EXCEPT ![f] = TRUE]
         /\ pc' = "Done"

The pcal with clause branches each possible Flags value. But the tla one, which seems to me, only works on one possible new state because of the \E (as long as there exists one) logical operator.

I must be understanding something wrong about the \E here.

Thanks.

---- MODULE simple ----
EXTENDS Integers, TLC, Sequences, FiniteSets


Flags == {"f1", "f2"}


(* --algorithm simple
variables
    flags = [f \in Flags |-> FALSE];
begin
    with f \in Flags do
         flags[f] := TRUE;
    end with;
end algorithm; *)




\* BEGIN TRANSLATION
VARIABLES flags, pc


vars == << flags, pc >>


Init == (* Global variables *)
        /\ flags = [f \in Flags |-> FALSE]
        /\ pc = "Lbl_1"


Lbl_1 == /\ pc = "Lbl_1"
         /\ \E f \in Flags:
              flags' = [flags EXCEPT ![f] = TRUE]
         /\ pc' = "Done"


Next == Lbl_1
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)


Spec == Init /\ [][Next]_vars


Termination == <>(pc = "Done")


\* END TRANSLATION


====

[david streader]

Hi A partial answer only.

  Q1. not sure what you mean as the State Graph (Q2) shows the states in all the detail I can think of.

  Q2. the Next loops are caused by the  TLA+  (pc = "Done" /\ UNCHANGED vars) clause as can be seen by commenting them out. Not sure though what you have to do the PlusCal to prevent  this clause being formed.

 Q3. the clause /\ \E f \in Flags: flags' = [flags EXCEPT ![f] = TRUE] is satisfied both when f = "f1" and when f = "f2" hence the step generates the two transitions of the State Graph.

regards david

[Shiyao MA]

Hi David,

Thanks for your reply.

On Wednesday, 27 March 2019 10:00:49 UTC+8, david streader wrote:

  Q2. the Next loops are caused by the  TLA+  (pc = "Done" /\ UNCHANGED vars) clause as can be seen by commenting them out. Not sure though what you have to do the PlusCal to prevent  this clause being formed.

I tried commenting out the clause (pc = "Done" /\ UNCHANGED vars).

Now the check complains there is deadlock.  Indeed, the comment in the generated tla code mentions that:

\*           \/ (* Disjunct to prevent deadlock on termination *)

\*              (pc = "Done" /\ UNCHANGED vars)

If I understand it correctly, pc' has become "Done" in Lbl_1, why is there still deadlock?

My another related question is about the clause:

Spec == Init /\ [][Next]_vars

How does tla execute the spec?  What's the execution logic when it encounters /\ and \/ ? Are they executed in a single step or not?

 Also, I don't quite what [Next]_vars means.

Right now, I am fine with the pluscal language.

 

[Jay Parlar]

It sounds like now would be a good time for you to start looking at “Specifying Systems” https://lamport.azurewebsites.net/tla/book-02-08-08.pdf

If you’re interested in what’s actually going on with the TLA+, then there’s no better place. And learning TLA+ will make your PlusCal better.


Jay P