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.
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.
Nahida Sultana Chowdhury
Dept. of Computer Science and Engineering,
University of Asia Pacific,
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