get rid of twa::transition_annotation() ?
This is only used in replay_twa_run() and its interface is not compatible with for (auto& t: aut->out(s))
.
I think it should be better that each formalism that want to supply better information about counterexamples should provide a function that takes a run prints the annotated counterexample.