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

Re: [tlaplus] About a Theorem in the Raw TLA

The implication


is indeed valid for any action A. Semantically, the proof is obvious from the definition of ENABLED and ordinary predicate logic. If you refer to proofs in the TLA+ Proof System, ENABLED is not yet supported [1]. We are currently reimplementing TLAPS, and one of our main motivations for doing so is to provide the basis for supporting reasoning about ENABLED.


[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html

On 30 Apr 2017, at 17:42, belout...@xxxxxxxxx wrote:

Hi all,

In the Raw TLA can we state the following Theorem :

Theorem : For any action A, A ==> Enabled(A)

If it is valid , How we can prove it ?. If it is invalid , let me know the counterexample.

Once again, if the suggested statement is a theorem, can we add the following inference rule : For any A in Raw TLA.

                     A ==> Enabled(A)  

Thanks In advance

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.