Re: [tlaplus] Does verifying parts of the initial state separately affect correctness?

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

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