Re: [tlaplus] Proving temporal property in TLAPS

[Stephan Merz <stephan.merz@xxxxxxxxx>]

Hi Matthias,

that’s an interesting problem in that you’ve hit what appears to be a limitation of the "coalescing" technique that underlies the interplay of predicate logic and temporal logic reasoning in TLAPS. The problem is that you mix quantifier reasoning and temporal logic reasoning, and the bound of the quantifier is a state function, not a constant. Your theorem is correct because the domain of the sequence is in fact unchanged along the execution, but the prover doesn’t "see" this, and even if you add "UNCHANGED (DOMAIN States)" as a conjunct to the right-hand side of step <1>1 of your proof, the coalescing procedure is not smart enough to exploit this when pushing the quantifier over [].

The workaround I suggest is to make the domain of the "States" function explicit, as in the module below. In the proof, step <1>2 introduces a constant for the bound variable and uses PTL to establish the property for that fixed constant i. Step <1>3 then introduces the quantifier, and coalescing knows that it may push the quantifier across [] as long as the domain of the quantifier is a constant.

Best regards,
Stephan

-------------------------- MODULE TerminationSpec --------------------------
EXTENDS TLAPS

CONSTANT Proc

VARIABLE States
Init == States \in [Proc -> {"INIT", "DONE"}]
Terminate(i) ==
   States' = [States EXCEPT ![i] = "DONE"]
Next == \E i \in Proc : Terminate(i)
Spec == Init /\ [][Next]_States

HasTerminated(i) ==
   States[i] = "DONE"

THEOREM Spec => [](\A i \in Proc : HasTerminated(i) => [] HasTerminated(i))
      \* Init is an invariant
   <1>1 Init /\ [Next]_States => Init'
       BY DEF Init, Next, Terminate
       \* Each step leaves terminated states unchanged
   <1>2 ASSUME NEW i \in Proc
        PROVE  Spec => [](HasTerminated(i) => []HasTerminated(i))
     <2>1 Init /\ [Next]_States /\ HasTerminated(i) => HasTerminated(i)'
       BY DEF Init, Next, Terminate, HasTerminated
     <2> QED  BY <1>1, <2>1, PTL DEF Spec
   <1> QED
       BY <1>1, <1>2

=============================================================================


> On 31 May 2024, at 13:03, Grundmann, Matthias (KASTEL) <matthias.grundmann@xxxxxxx> wrote:
> 
> Can the theorem in the following exemplary specification be proven in TLAPS?
> 
> -------------------------- MODULE TerminationSpec --------------------------
> 
> EXTENDS Sequences, TLAPS
> 
> VARIABLE States
> Init == States \in Seq({"INIT", "DONE"})
> Terminate(i) ==
>    States' = [States EXCEPT ![i] = "DONE"]
> Next == \E i \in DOMAIN States : Terminate(i)
> Spec == Init /\ [][Next]_States
> 
> HasTerminated(i) ==
>    States[i] = "DONE"
>    THEOREM Spec => [](\A i \in DOMAIN States : HasTerminated(i) => [] HasTerminated(i))
> 
> =============================================================================
> 
> The theorem should state that once a state has been set to "DONE", the state will always equal "DONE" (and never be reverted to "INIT"). Have I formalized this correctly?
> 
> My attempt to prove the theorem follows. TLAPS successfully checks the steps <1>1 and <1>2 but not the QED step.
> 
> THEOREM Spec => [](\A i \in DOMAIN States : HasTerminated(i) => [] HasTerminated(i))
>        \* Init is an invariant
>    <1>1 Init /\ [Next]_States => Init'
>        BY DEF Init, Next, Terminate
>        \* Each step leaves terminated states unchanged
>    <1>2 Init /\ [Next]_States => \A i \in DOMAIN States : HasTerminated(i) => HasTerminated(i)'
>        BY DEF Init, Next, Terminate, HasTerminated
>        <1>3 QED
>        BY <1>1, <1>2, PTL DEF Spec, HasTerminated
> 
> -- 
> 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/7336ff89-595a-43ba-ba71-f373898da9e8%40kit.edu.

-- 
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/66A37E6A-7864-4EAF-AF7A-E31EE4D7C399%40gmail.com.