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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 26 Nov 2023 09:01:13 +0100*References*: <0d5368ca-6221-404a-a144-362e874a1431n@googlegroups.com> <6883916B-8B2D-426C-90C9-E7AC3781E981@gmail.com> <CAGNViOMZFg-7EEeH9xFMHGdoqiwVgXPq=kJ33d324Xm4T+GHHw@mail.gmail.com>

Hi Ramon, not entirely sure what you mean when you say you proved everything except for the final theorem (whose QED proof was included in yesterday's message). For what it's worth, here is the proof of the first of the intermediate steps, the two others are similar: LEMMA RedBlue == Spec => []((x = "red") => <>(~(x = "red") /\ (x = "blue"))) <1>1. x = "red" => ENABLED <<Next>>_x BY ExpandENABLED DEF Next <1>2. x = "red" /\ [Next]_x => (x = "red")' \/ (~(x = "red") /\ (x = "blue"))' BY DEF Next <1>3. x = "red" /\ <<Next>>_x => (~(x = "red") /\ (x = "blue"))' BY DEF Next <1>. QED BY <1>1, <1>2, <1>3, PTL DEF Spec About validity checking for temporal logic, there used to be a number of online tools for LTL that could help you with that. A quick search brought up Owl [1], a tool that converts LTL formulas to different forms of automata. For example, you can paste the formula "!(G(a -> b) -> (G a -> G b))" into the input box (note that you need to negate the formula for validity checking) and generate an NBA (non-deterministic Büchi automaton). You'll see that the automaton is trivial and has no acceptance cycle (marked in green), which means that the formula is unsatisfiable, therefore the formula without the outermost negation is valid. Concerning your question: the "updated_enabled_cdot" branch contains two more proof primitives for reasoning about ENABLED that have not yet made it into the main branch: - ENABLEDrewrites applies simplification rules such as ENABLED (A \/ B) <=> (ENABLED A) \/ (ENABLED B) ENABLED (A /\ B) <=> (ENABLED A) /\ (ENABLED B) if A and B do not share primed variables ENABLED (x' = e) <=> TRUE if e is a state function with the purpose of simplifying an ENABLED _expression_ before applying ExpandENABLED (which introduces existential quantification that may be difficult for the backends to prove). - ENABLEDRules allows reasoning about monotonicity of ENABLED: ASSUME A => B PROVE (ENABLED A) => (ENABLED B) ASSUME A <=> B PROVE (ENABLED A) <=> (ENABLED B) For example, this is useful to reduce ENABLED <<A>>_v to ENABLED A if A is an action that cannot stutter (as is often the case), since the latter is easier to reason about. These additional primitives sometimes make proofs easier but they are not essential. Stephan [1] https://owl.model.in.tum.de
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/6178623B-7D82-4711-854B-26091E6EF685%40gmail.com. |

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

**References**:**[tlaplus] Proving eventualities with TLAPS (1.5.0)***From:*Ramon Snir

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

**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)***From:*Ramon Snir

- Prev by Date:
**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)** - Next by Date:
**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)** - Previous by thread:
**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)** - Next by thread:
**Re: [tlaplus] Proving eventualities with TLAPS (1.5.0)** - Index(es):