[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Understanding relation between pluscal and tla

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.