Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Spot Spot
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 132
    • Issues 132
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 2
    • Merge requests 2
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Spot
  • SpotSpot
  • Issues
  • #127
Closed
Open
Created Dec 09, 2015 by Alexandre Duret-Lutz@adlOwner

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:

  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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking