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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information