Does verifying parts of the initial state separately affect correctness?

[Jones Martins]

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

[Stephan Merz]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7641afb2-87d3-4829-880c-c944f89a4826n%40googlegroups.com.

[Jones Martins]

Hi, Stephan.

I should've been more precise when writing my question, but you got it perfectly.

I split Init into two (or more) mutually-exclusive sets, such as

Init1 == var \in {0, 1, 2}

Init2 == var \in {4, 5, 6}

Init == Init1 \/ Init2

then run Spec == Init1 /\ [][Next]_vars /\ Fairness,

then run Spec == Init2 /\ [][Next]_vars /\ Fairness, etc;

such that running all specs would return the same as running Spec == Init /\ [][Next]_vars /\ Fairness + Temporal Properties

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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/81472667-D5EE-4CBA-8E2D-2FED212A2761%40gmail.com.