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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 22 Feb 2022 08:28:18 +0100*References*: <7641afb2-87d3-4829-880c-c944f89a4826n@googlegroups.com>

Hello, if I understand correctly, you generate two (or more) specifications of the form S1 == Init /\ P /\ [][Next]_vars /\ L S2 == Init /\ Q /\ [][Next]_vars /\ L such that Init => P \/ Q, and verify that both S1 and S2 have some property F. Your question is if this ensures that S == Init /\ [][Next]_vars /\ L also ensures property F, and this is clearly the case. Note however that the two separate model checking runs for S1 and S2 may (collectively) take longer than a single model checking run for S because the state spaces of S1 and S2 may (and in general will) overlap. Stephan
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/81472667-D5EE-4CBA-8E2D-2FED212A2761%40gmail.com. |

**Follow-Ups**:

**References**:

- Prev by Date:
**Re: [tlaplus] TLA+ extensions for user-defined procedure writing by programming language** - Next by Date:
**Re: [tlaplus] TLA+ extensions for user-defined procedure writing by programming language** - Previous by thread:
**[tlaplus] Does verifying parts of the initial state separately affect correctness?** - Next by thread:
**Re: [tlaplus] Does verifying parts of the initial state separately affect correctness?** - Index(es):