[tlaplus] Re: Understanding relation between pluscal and tla

[Shiyao MA <i@xxxxxxxxx>]

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.

 

-- 
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.