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

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

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?



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.