add an intersect() method to twa_graph
The use of
bool res = product(l->translation, g->translation)->is_empty();
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 and
is_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() 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
autfilt --intersect would benefit from that as well (although in the case of
ltlcross, a counterexample would be better than
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.