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