It should be investigated whether the current generation process of replay information (i.e., nondeterministic choices) of counter examples is really necessary. During counter example generation, all transitions between all states of the counter example are checked again, looking for a matching transition and recording its nondeterministic choices.
This replay information gathering logic is complicated and easily gets out-of-sync with the rest of the model checking infrastructure. An alternative would be to collect replay information directly during model checking, however, that might be expensive performance-wise. It should therefore at least be investigated whether counter example generation can be implemented on top of the model checking infrastructure.
In particular, counter example generation does not take activation minimality into account, potentially generating a counter example that has the correct state but a non-activation-minimal transition.
It should be investigated whether the current generation process of replay information (i.e., nondeterministic choices) of counter examples is really necessary. During counter example generation, all transitions between all states of the counter example are checked again, looking for a matching transition and recording its nondeterministic choices.
This replay information gathering logic is complicated and easily gets out-of-sync with the rest of the model checking infrastructure. An alternative would be to collect replay information directly during model checking, however, that might be expensive performance-wise. It should therefore at least be investigated whether counter example generation can be implemented on top of the model checking infrastructure.
In particular, counter example generation does not take activation minimality into account, potentially generating a counter example that has the correct state but a non-activation-minimal transition.