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.
