| Dear Nahida,
I previously answered your question about stuttering. Thank you for your TLA+ specification; I have the following stylistic remarks:
. You enforce liveness by the conjunct "[]eventually" in your specification – by the way, the [] operator is superfluous here because ~> already is boxed since F ~> G abbreviates [](F => <>G), and since [] commutes with \A. This is a "global" condition, and it is more interesting to replace it in your specification by an appropriate fairness condition on the Acquire action, then prove your "eventually" formula to be a property of the specification.
. Leading "/\" operators are used in TLA+ for aligning multi-line conjunctions (and disjunctions), they are not necessary in one-line formulas such as in the definition of Spec. When you write multi-line conjunctions, make sure you properly align them, otherwise you may run into unpleasant surprises.
. Certainly you want to check a more interesting property of your specification than just type invariance.
Best regards, Stephan
I am just a beginner of using TLA+ having difficulties.
I have a query is:
In my code I have a line like
Spec == /\ Init /\ [][PNext]_stateP /\ []eventually
where [][PNext]_stateP represent PNext will be also true if stateP'=stateP but I don't want to add this conditiontion here, so when I am trying to change the code by replacing []PNext it's saying "followed by action not of form [A]_v".
In this situation what I am supposed to do, also correct me if I am assuming something wrong.
*The source code is attached here.
Best Regards,
Nahida
Nahida Sultana Chowdhury Dept. of Computer Science and Engineering, University of Asia Pacific, Dhaka, Bangladesh.
--
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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
<mutexEX.tla>
|