Hello,--if I understand correctly, you generate two (or more) specifications of the formS1 == Init /\ P /\ [Next]_vars /\ LS2 == Init /\ Q /\ [Next]_vars /\ Lsuch that Init => P \/ Q, and verify that both S1 and S2 have some property F. Your question is if this ensures thatS == Init /\ [Next]_vars /\ Lalso 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.StephanOn 22 Feb 2022, at 00:45, Jones Martins <jonesmvc@xxxxxxxxx> wrote:Hi everyone,This question might have an obvious answer, but I'd like to make sure.To clarify: Instead of running an hour-long verification process, I split my initial states in groups so that I could tackle the fastest groups first.Suppose that verifying all such groups returns no errors, is it possible for TLC not to find a mistake because it didn't run with the entire state space at once?Thanks,Jones--
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/7641afb2-87d3-4829-880c-c944f89a4826n%40googlegroups.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/MYgXSTKbcwg/unsubscribe.
To unsubscribe from this group and all its topics, 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.