Hi Ramon,
thank you for your question and indeed, documentation for the more recent features of the prover is sorely lacking. The only examples using the ENABLED backends that I am aware of are
In order to answer your question, the PTL backend is not based on axioms but on a decision procedure for propositional temporal logic. The details are described in our "coalescing" paper [1]. This has two fundamental consequences:
1. In first approximation, PTL does not handle sequents (ASSUME / PROOF constructs), except for constant-level assumptions [2]. I recommend only invoking it in such contexts. The "non-[]" warnings that you see in the proof output are an indication of this: they tell you that these ASSUME / PROOF steps should be rewritten as plain implications.
2. PTL only handles propositions and does not perform even trivial first-order reasoning. It will abstract atomic formulas such as `x = "red"' into a proposition, but sometimes it may be helpful to introduce propositional abstractions yourself, and it won't know that trivialities such as
x = "red" => ~(x = "blue")
holds. (I believe it doesn't even know that `x # "red"' is equivalent to `~(x = "red")'.)
Below is your proof rewritten with these caveats in mind, and an outline of your "main" theorem whose QED step is checked by PTL. Note in particular that it is really necessary in that proof to write
<1>1. Spec => []((x = "red") => <>(~(x = "red") /\ (x = "blue")))
due to observation (2) above, otherwise PTL won't know that the step from red to blue cannot just be a stuttering step. The missing proofs for steps <1>1 to <1>3 should be similar to the proof of your lemma that x will eventually be blue. (I'd actually recommend setting up the lemma in the way that it fits the steps required in the main proof so that you can use lemmas there.)
In the proof of your first real liveness theorem, besides rewriting ASSUME / PROOF to implications I also had to add the step
<1>4. Init /\ [Next]_x => Init' \/ (x = "blue")'
BY DEF Init, Next
Without it, the conclusion wouldn't hold: weak fairness ensures that a <<Next>>_x transition will be taken only if it remains enabled, not if it just happens to be enabled at some point.
Besides, I made a few cosmetic changes to your proofs, in particular by reformulating the type-correctness lemma so that it can be used within the liveness proof.
I do hope this helps you to make progress: feel free to come back with further questions that will invariably arise.
Best,
Stephan
[2] More generally, all assumptions of lemmas should be "boxed" formulas, i.e., trivially equivalent to []F for some F.
--------------------------- MODULE RingEventually ---------------------------
EXTENDS TLAPS
VARIABLE x
Init == x = "red"
Next ==
\/ (x = "red" /\ x' = "blue")
\/ (x = "blue" /\ x' = "green")
\/ (x = "green" /\ x' = "blue")
Spec == Init /\ [][Next]_x /\ WF_x(Next)
TypeOK == x \in {"red", "green", "blue"}
LEMMA TypeSafety == Init /\ [][Next]_x => []TypeOK
PROOF
<1> USE DEF TypeOK
<1>1. Init => TypeOK
BY DEF Init
<1>2. ASSUME TypeOK /\ [Next]_x
PROVE TypeOK'
BY <1>2 DEF Next
<1> QED
BY <1>1, <1>2, PTL DEF Spec
LEMMA EventuallyRed == Spec => <>(x = "red")
PROOF BY PTL DEF Spec, Init
THEOREM Spec => <>(x = "blue")
PROOF
<1>2. TypeOK /\ Init => ENABLED <<Next>>_x
BY ExpandENABLED DEF Init, Next
<1>3. Init /\ <<Next>>_x => (x = "blue")'
BY DEF Init, Next
<1>4. Init /\ [Next]_x => Init' \/ (x = "blue")'
BY DEF Init, Next
<1> QED
BY <1>2, <1>3, <1>4, TypeSafety, PTL DEF Spec
\* And my actual goal: how should _this_ proof be structured?
THEOREM Spec => []<>(x = "red")
<1>1. Spec => []((x = "red") => <>(~(x = "red") /\ (x = "blue")))
<1>2. Spec => []((x = "blue") => <>(~(x = "blue") /\ (x = "green")))
<1>3. Spec => []((x = "green") => <>(~(x = "green") /\ (x = "red")))
<1>. QED BY <1>1, <1>2, <1>3, EventuallyRed, PTL
=============================================================================
Hi,
I am trying to overcome some property-checking limitations of TLC by learning TLAPS, specifically using the unreleased features regarding ENABLED and \cdot.
I am using TLAPM built from source from this commit:
https://github.com/tlaplus/tlapm/tree/dc344b6d6e92332ba4a54f4cc86c577a9a137ecd (From the master branch, but not the latest commit)
I have experience with Coq and I think I understand the general idea of how to use TLAPS, up to the PTL/sl4 solver. I'm not sure what proof rules and axioms it has access to and most results I found online are 2+ years old so they focus on proving safety, without ENABLED usage.
--------------------------- MODULE RingEventually ---------------------------
EXTENDS TLAPS
VARIABLE x
Init == x = "red"
Next ==
\/ (x = "red" /\ x' = "blue")
\/ (x = "blue" /\ x' = "green")
\/ (x = "green" /\ x' = "blue")
Spec == Init /\ [][Next]_x /\ WF_x(Next)
TypeOK == x \in {"red", "green", "blue"}
LEMMA TypeSafety == Spec => []TypeOK
PROOF
<1> USE DEF TypeOK
<1>1. Init => TypeOK
BY DEF Init
<1>2. ASSUME TypeOK /\ [Next]_x
PROVE TypeOK'
BY <1>2 DEF Next
<1> QED
BY <1>1, <1>2, PTL DEF Spec
LEMMA Spec => <>(x = "red")
PROOF BY PTL DEF Spec, Init
\* The QED step fails
THEOREM Spec => <>(x = "blue")
PROOF
<1>1. (Init /\ [][Next]_x) => []TypeOK
<2>1. Init => TypeOK
BY DEF Init, TypeOK
<2>2. ASSUME TypeOK /\ [Next]_x
PROVE TypeOK'
BY <2>2 DEF TypeOK, Next
<2> QED
BY <2>1, <2>2, PTL
<1>2. ASSUME TypeOK /\ Init
PROVE ENABLED <<Next>>_x
BY <1>2, ExpandENABLED DEF Init, Next
<1>3. ASSUME Init /\ <<Next>>_x
PROVE (x = "blue")'
BY <1>3 DEF Init, Next
<1> QED \* failed
BY <1>1, <1>2, <1>3, PTL DEF Spec, Init
(*
The proof state at the failing QED:
ASSUME NEW VARIABLE x,
x = "red" /\ [][Next]_x => []TypeOK ,
ASSUME TypeOK /\ x = "red" (* non-[] *)
PROVE ENABLED <<Next>>_x ,
ASSUME x = "red" /\ <<Next>>_x (* non-[] *)
PROVE (x = "blue")' ,
TRUE
PROVE x = "red" /\ [][Next]_x /\ (WF_(x) (Next)) => <>(x = "blue")
*)
\* How should this proof be structured?
THEOREM Spec => <>(x = "green")
PROOF OMITTED
\* And my actual goal: how should _this_ proof be structured?
THEOREM Spec => []<>(x = "red")
PROOF OMITTED
=============================================================================
There are three theorems that I think are within reach for TLAPS but I don't know what PTL would need to prove them.
THEOREM Spec => <>(x = "blue") \* Witness: after one non-stuttering action, it will be blue
THEOREM Spec => <>(x = "green") \* Witness: after two non-stuttering actions, it will be green
THEOREM Spec => []<>(x = "red") \* Depending on the current state, the witness would be zero/one/two non-stuttering actions
Any hints on how I could approach these?
--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/0d5368ca-6221-404a-a144-362e874a1431n%40googlegroups.com.