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

[Jones Martins <jonesmvc@xxxxxxxxx>]

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.