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