[tlaplus] Proving eventualities with TLAPS (1.5.0)

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.

For a concrete example, see this module which is inspired by https://github.com/tlaplus/tlapm/blob/dc344b6d6e92332ba4a54f4cc86c577a9a137ecd/examples/SimpleEventually.tla

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