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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 18 Apr 2021 11:31:07 +0200*References*: <5985a9d4-fa8f-47e2-90a5-fa75cde9a736n@googlegroups.com>

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. 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1E526B44-D52C-4877-AA8A-FCC447C42272%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] False positives during model checking***From:*alex.t...@xxxxxxxxx

**References**:**[tlaplus] False positives during model checking***From:*alex.t...@xxxxxxxxx

- Prev by Date:
**[tlaplus] False positives during model checking** - Next by Date:
**Re: [tlaplus] False positives during model checking** - Previous by thread:
**[tlaplus] False positives during model checking** - Next by thread:
**Re: [tlaplus] False positives during model checking** - Index(es):