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

*From*: "Grundmann, Matthias (KASTEL)" <matthias.grundmann@xxxxxxx>*Date*: Fri, 31 May 2024 13:03:00 +0200*User-agent*: Mozilla Thunderbird

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"

============================================================================= 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))

<1>1 Init /\ [Next]_States => Init' BY DEF Init, Next, Terminate

<1>2 Init /\ [Next]_States => \A i \in DOMAIN States : HasTerminated(i) => HasTerminated(i)' BY DEF Init, Next, Terminate, HasTerminated

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

**Follow-Ups**:**Re: [tlaplus] Proving temporal property in TLAPS***From:*Stephan Merz

- Prev by Date:
**[tlaplus] Re: Invariant violated, no state trace** - Next by Date:
**Re: [tlaplus] Proving temporal property in TLAPS** - Previous by thread:
**[tlaplus] Re: Invariant violated, no state trace** - Next by thread:
**Re: [tlaplus] Proving temporal property in TLAPS** - Index(es):