Hi Alexandre, Suppose one calls ltl2tgba with the option --check=stutter-invariant. Would it be possible to print a warning with diagnostics, like the online tool does? Something like: Warning: The property is stutter-sensitive - the following words are a proof, as they differ only by some stuttering: Accepted word: a & b; a & b; cycle{!a & !b} Rejected word: a & b; cycle{!a & !b} Motivation: * by passing the option --check=stutter-invariant the user tells the tool that stutter-invariance is important for them, hence a warning/diagnostics is desirable if the check fails (this warning does not have to be printed if this option is not passed) * it's not easy to get these traces from the final automaton - my understanding is that some potentially costly operations are required, which are performed during the check anyway * the current way of getting this diagnostics (python + libraries; maybe there is a better way I don't know about?) creates many dependencies, thus making it difficult to integrate this functionality into toolchains - ideally one would want just a single executable ltl2tgba * my (perhaps naive) understanding is that this is not difficult to implement and does not incur much extra run-time as the check has to be performed anyway Best regards, Victor.