Reimplementation of testing-automata in Spot
- Martin Huvelle
Spot is a library of model checking algorithms which can manage different kinds of -automata. It can also handle testing-automata since Spot 1.0. However, Spot 2.0 introduced a new data structure for automata with generic acceptance conditions that were not available when testing automata where developed. Our goal is to reimplement testing-automata using the more modern data structure. By doing so, we expect to reuse existing algorithms, to reduce the amount code specific to testing automata, and to make testing automata compatible with HOA format. Additionally, our preliminary implementation seems to produce smaller testing-automata than the original one.