GitLab

The use of

bool res = product(l->translation, g->translation)->is_empty();

in language_containment_checker::incompatible_(l,g) is bad for two reasons:

1. 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.
2. 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.