[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] ENABLED Operator Theorems
> On 3 May 2017, at 10:46, kacem belout <belout...@xxxxxxxxx> wrote:
> I noticed the following theorems concerning the ENABLED Operator that I hopefully would like to prove them in a formal way ( i.e Formally ( Logically and/or symbolically) as using Inference Rules)
as I tried to explain before, in order to give a precise meaning to your notion of "formal" proof, you would need to give clear definitions.
> In the context of the Raw Logic (RTLA), for any Action A, we assert the following valid statements.
I don't understand why you insist on Raw TLA: the difference between RTLA and TLA only exists at the temporal level, and you don't consider any temporal formulas. Also, it would help if you used actual TLA syntax.
> Let me know if any one is not valid by giving a counterexample, thanks !.
> Theorem 1 : A ==> ENABLED(A)
> Proof : Now, I don't know How To formally and mechanically derive ENABLED(A) From A which is expressed in terms of primed variables and unprimed variables.
See my previous answer: the implication holds for the same reason why F => \E X: F is a theorem of first-order logic.
> Theorem 2 : \Not ENABLED(A) ==> \Not A
> Proof : Is equivalent to Theorm1 by propositional logic rule (implication equivalente to its contrapositive).
Yes, so it's just a corollary to the previous theorem.
> Theorem 3 : \Not A ==> \Not ENABLED(A)
Wrong. Consider A == x = 0 /\ x' = 1 and a state s that assigns 0 to x. Then the stuttering step (s,s) satisfies ~ A and ENABLED A.
> Theorem 4 : \Not (ENABLED(A)) ==> ENABLED( \Not (A))
Consequence of Theorems 1 and 2.
> Theorem 5 : ENABLED(A) <==> ENABLED(-1(A)) , where -1(A) == (A)-1 ; inverse of A. (A)-1 == A ( v ' <- v , v <- v ')
Wrong, take again A == x=0 /\ x'=1. then
ENABLED A \equiv x = 0
ENABLED (A)-1 \equiv x = 1
> Theorem 6 : For any state predicate P. P <==> ENABLED(P)
> Theorem 7 : For any state predicate P. P ==> ENABLED((P) '), where ' == Prime operator.
Correct. (ENABLED P' is true iff P is satisfiable.)
> Theorem 8 : For any state predicate P. P ==> ENABLED(((p)')-1)
Isn't (P')-1 = P, so this is the same as theorem 6?