[tlaplus] Proving temporal property in TLAPS

["Grundmann, Matthias (KASTEL)" <matthias.grundmann@xxxxxxx>]

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.

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature