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