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.