Spinroot

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.