In the following example, the engine allows states that do not satisfy the property to be in the trace.
Created attachment 211 [details]
Created attachment 212 [details]
Created attachment 232 [details]
another example with counter example to A<>
the following model from Danny & Jiri seems to suffer from the same problem.
it seems that at least the last symbolic state is not completely stabilized.
or maybe the loop part of the trace is not stabilized?
the query for this model is: