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

Re: [tlaplus] Fwd: Regarding TLA+ coding

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,

On 6 Mar 2017, at 07:43, Nahida Sultana Nahida Sultana <nchow...@xxxxxxxxxx> wrote:

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 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.