Search code examples
nusmv

how to find out all possible counter examples Nusmv


i have model in NuSMV and after check ltl specification NuSMV give me a Counter Example is it possible to find out all path that contain counter example not one of them?


Solution

  • You can use your counter-example to refine your LTL specification, then use the refined specification for modelchecking again. repeat this until NuSMV find no more counterexamples, but in some case, it may never end.

    Basically, this is called CEGAR -- counterexample guided abstraction refinement, except that it's not the abstraction model, but the specification is refined at every iteration.