Regarding TLA+ coding

99 views
Skip to first unread message

Nahida Sultana Nahida Sultana

unread,
Feb 24, 2017, 9:56:42 AM2/24/17
to tla...@googlegroups.com
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. 

mutexEX.tla

Stephan Merz

unread,
Feb 24, 2017, 10:12:42 AM2/24/17
to tla...@googlegroups.com
Dear Nahida,

TLA+ specifications always allow for stuttering, and in particular you have to write your next-state in the form [][A]_v. As the error message tells you, the formula []A is not well-formed when A is an action formula.

The intuition behind this restriction is that your specification describes a universe containing in particular the system that you care about, and variables that are outside the scope of your system may change at any time without affecting the system. Admitting for stuttering invariance is instrumental for expressing refinement as implication and composition as conjunction. Please see the TLA+ documentation available on the TLA+ Web site, in particular the hyperbook.

Best regards,

Stephan


--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
<mutexEX.tla>

Nahida Sultana Nahida Sultana

unread,
Mar 6, 2017, 1:43:43 AM3/6/17
to tla...@googlegroups.com
 
​H​
i,
mutexEX.tla

Stephan Merz

unread,
Mar 6, 2017, 2:41:12 AM3/6/17
to tla...@googlegroups.com
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


Reply all
Reply to author
Forward
0 new messages