A forum for Spin users

You are not logged in.

- Topics: Active | Unanswered

**m_tabaei****Member**- Registered: 2011-06-21
- Posts: 2

Hi,

I tried to verify this LTL property ([]<>dl) on a model in SPIN. SPIN generated a never claim for the negation of this property which is ![]<>dl. I set parameters in SPIN to generate all the possible counterexamples up to the depth of 10,000. I expected to see only infinite counterexamples but to my surprise a large number of the generated counterexamples to this LTL property are finite. I can’t explain how these finite traces are generated.

Offline

the finite traces are considered a special case of infinite traces, using the so-called 'stutter-extension rule' (this is fairly standard when dealing with omega-automata theory). basically, the final state is assumed to repeat forever on a 'stutter' step (a no-op), thus allowing us to treat it as a special 'infinite' trace.

in your case ![]<>dl is the same as <>[]!dl, so if dl is false in the final state, the negated property holds on that trace

Offline