|Unlike static analysis, standard model checkers such as TLC do not apply abstractions to the input model, and in this sense they do not produce false positives. However, the specification given to the model checker is always an abstraction of the real system and therefore counter-examples found by the model checker need not correspond to actual system executions. In those cases, either the property must be reformulated or the model must be refined to exclude such spurious counter-examples, and the latter may lead to state explosion and may render verification infeasible.|
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/1E526B44-D52C-4877-AA8A-FCC447C42272%40gmail.com.