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]]>

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.

]]>