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

Re: [tlaplus] TLAPS: ENABLEDrules depends on assumptions of level > 1



You are exploring mostly uncharted territory here, and I encourage you to file this as an issue on GitHub so that it won't get lost.

Logically, your proof should only rely on a state-level assumption, i.e. you should be able to prove

ASSUME terminate = TRUE
PROVE  (ENABLED <<NextDown>>_cvars => ENABLED <<CNext>>_cvars)

which implies your actual proposition. But I see why you find it unwieldy that the proof fails with temporal-level hypotheses.

Stephan

On 28 Nov 2023, at 18:05, Ramon Snir <ramonsnir@xxxxxxxxx> wrote:

I am using TLAPS from branch "updated_enabled_cdot".

If there is any temporal assumption in the context, ENABLEDrules fails. This is true even if that assumption is irrelevant to the current step (but was needed for previous steps). I have not found a way to hide an unnamed assumption from a step. I've attached various attempts I've made below.

What I am trying to prove is: ASSUME [](terminate = TRUEPROVE (ENABLED <<NextDown>>_cvars => ENABLED <<CNext>>_cvars)

which requires me to have a temporal assumption in context,  because the statement is not true if the assumption is not true. I am not sure how to prove this lemma given this limitation.

I don't believe there is a way for me to restructure this without any assumptions, even by moving the lemma into the theorem, but even if I could it would be very unreadable.

Various attempts:

Q == terminate' = FALSE
P == terminate' = terminate

\* Example 1 - works */

LEMMA ENABLED Q => ENABLED P
PROOF
<1>. Q => P
  OMITTED
<1>. QED
  BY ENABLEDrules

\* Example 2 - works */

LEMMA ASSUME TRUE PROVE ENABLED Q => ENABLED P
PROOF
<1>. Q => P
  OMITTED
<1>. QED
  BY ENABLEDrules

\* Example 3 - doesn't work */

LEMMA ASSUME []TRUE PROVE ENABLED Q => ENABLED P
PROOF
<1>. Q => P
  OMITTED
<1>. QED
  BY ENABLEDrules
\*ENABLEDrules depends on assumptions of level > 1 
\*
\*
\*Obligation:
\*
\*ASSUME NEW VARIABLE x,
\*       NEW VARIABLE terminate,
\*       []TRUE ,
\*       Q => P ,
\*       TRUE 
\*PROVE  ENABLED Q => ENABLED P

\* Example 4 - doesn't work */

LEMMA ASSUME Q => P
      PROVE ENABLED Q => ENABLED P
PROOF BY ENABLEDrules
\*ENABLEDrules depends on assumptions of level > 1 
\*
\*
\*Obligation:
\*
\*ASSUME NEW VARIABLE x,
\*       NEW VARIABLE terminate,
\*       Q => P ,
\*       TRUE 
\*PROVE  ENABLED Q => ENABLED P

\* Example 5 - doesn't work */

LEMMA ASSUME ((terminate = TRUE) => (terminate' = FALSE))
      PROVE (ENABLED (terminate = TRUE) => ENABLED (terminate' = FALSE))
PROOF
<1>. QED
  BY ENABLEDrules
\*ENABLEDrules depends on assumptions of level > 1 
\*
\*
\*Obligation:
\*
\*ASSUME NEW VARIABLE x,
\*       NEW VARIABLE terminate,
\*       terminate = TRUE => terminate' = FALSE ,
\*       TRUE 
\*PROVE  ENABLED (terminate = TRUE) => ENABLED (terminate' = FALSE)

\* Example 6 - doesn't work */

PROPOSITION ASSUME [](terminate = TRUE)
            PROVE (ENABLED (terminate' = TRUE) => ENABLED (UNCHANGED terminate))
PROOF
<1>. (terminate = TRUE) /\ (terminate = TRUE)'
  BY PTL
<1>. (terminate' = TRUE) => (UNCHANGED terminate)
  OBVIOUS
<1>. QED \* fails, see status below
  BY ENABLEDrules
\*ENABLEDrules depends on assumptions of level > 1 
\*
\*
\*Obligation:
\*
\*ASSUME NEW VARIABLE x,
\*       NEW VARIABLE terminate,
\*       [](terminate = TRUE) ,
\*       terminate = TRUE /\ (terminate = TRUE)' ,
\*       terminate' = TRUE => UNCHANGED terminate ,
\*       TRUE 

\*PROVE  ENABLED (terminate' = TRUE) => ENABLED UNCHANGED terminate

--
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/0cda95d7-7d8a-4ce3-b8b4-b4f761e363fdn%40googlegroups.com.

--
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/FC9E59E1-949E-48AE-9E8D-09947BD07A98%40gmail.com.