add an intersect() method to twa_graph
The use of
bool res = product(l->translation, g->translation)->is_empty();
in language_containment_checker::incompatible_(l,g)
is bad for two reasons:
-
product()
builds the entire product, even in the cases where the product is non-empty andis_empty()
does not need to explore it fully. -
is_empty()
calls an emptiness checks that uses the "on-the-fly" interface, therefore allocating states and iterators all over the place.
The product could be done on-the-fly with otf_product()
. But otf_product()
would also use the on-the-fly interface of the two input automata, so allocating memory. In the case where is_empty()
has to explore the entire product, this would be a net loss.
So the proposal is to implement a function
bool intersects(const twa_graph_ptr& left, const twa_graph_ptr& right);
that would do an emptiness check over the product of left and right, computed on-the-fly. Because the two automata are twa_graph_ptr
, the emptiness check will be easier to implement efficiently, because it can refer to states by their numbers. Then we would also add a method bool twa_graph::intersect(const twa_graph_ptr& right)
.
This should be useful in other contexts. For instance ltlcross
and autfilt --intersect
would benefit from that as well (although in the case of ltlcross
, a counterexample would be better than bool
).
For benchmarking, reduc.test
seems to be a nice candidate. This test currently takes several minutes
and the checks for LTL equivalence spend approx 20% of time building products, and 13% testing those products for emptiness.