For model generation in Z3-Noodler I sometimes need some random accepting word from NFA. We have the function aut.get_words(max_length), but that can be slow if aut has too many states (you need to call it with aut.get_words(aut.num_of_states()) to be sure you will get at least one word).
The implementation would probably be some simple DFS that finishes after reaching final state (assuming we have trimmed automaton).
For model generation in
Z3-Noodler
I sometimes need some random accepting word from NFA. We have the functionaut.get_words(max_length)
, but that can be slow ifaut
has too many states (you need to call it withaut.get_words(aut.num_of_states())
to be sure you will get at least one word).The implementation would probably be some simple DFS that finishes after reaching final state (assuming we have trimmed automaton).