Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
Spot
Spot
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 111
    • Issues 111
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 2
    • Merge Requests 2
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Spot
  • SpotSpot
  • Issues
  • #127

Closed
Open
Opened 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 admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: spot/spot#127