two-automata emptiness check
Currently aut1->intersects(aut2)
calls !otf_product(aut1, aut2)->is_empty()
, so the emptiness check runs on a single automaton, whose number of acceptance sets is the sum of the acceptance sets of aut1
and aut2
.
- This can be an issue in
ltlcross
whereaut1
andaut2
may require more than 16 sets, and the sum exceed our 32-set limit. - This way of computing the intersection using the
otf_product()
function causes the emptiness check to rely on the abstract interface for exploring automata, even when the original two automata are stored astwa_graph
. So we spend a lot of time allocating and deallocating iterators and states.
So we want to write an emptiness check procedure that would work on two automata at once, and compute the "product" as it goes (but without needing to combine the acceptance conditions). This procedure should use the same tricks that @max used to implement couvreur99_new_check()
so that it would work with both interface (except that we now have to deal with a 2x2 combinations of interfaces). Obviously this should not inherit from the spot::emptiness_check
class (since this assumes a single automaton to check), but it should be written in a way that we can use it to implement twa::intersects()
and twa::intersecting_run()
.
Also related to #127 and #197 .
Eventually we will also want to support the refinement of the emptiness check in case of weak or terminal automata, and maybe a generalization to n-automata emptiness check (but this very last point is not a priority at all).
Suggested breakdown of the tasks:
-
implement an emptiness check that works on two Fin-less twa, using a variation of the couvreur99_new_check()
algorithm. This needs to be instantiated 4 times to support the on-the-fly and explicit interfaces for each automata; but those instance should be hidden behind a unique public symbol. -
adjust twa::intersects()
to use this new algorithm. -
I suggest writing tests in Python using randomly generated automata, and comparing the output of the new intersects()
method with the output ofproduct(a,n).is_empty()
. -
benchmark the difference between the old twa::intersects()
and the new one (this requires writing a new benchmark, probably using random automata). -
adjust the new algorithm so that it can return a counterexample when needed. Use it in twa::intersecting_run()
. -
specialize the new algorithm for weak and terminal automata, as well as for Kripke structures.