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

*From*: Ramon Snir <ramonsnir@xxxxxxxxx>*Date*: Fri, 24 Nov 2023 08:17:26 -0800 (PST)

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.

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

(*

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.

**Follow-Ups**:**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Re: Practice questions and answers for TLA+** - Next by Date:
**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)** - Previous by thread:
**Re: [tlaplus] TLA+ Community Survey** - Next by thread:
**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)** - Index(es):