Skip to content
GitLab
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 133
    • Issues 133
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • 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
  • SpotSpot
  • SpotSpot
  • Issues
  • #231
Closed
Open
Issue created Feb 16, 2017 by Alexandre Duret-Lutz@adlOwner

implement sum_or() and sum_and()

Just like we have autfilt --product-and and autfilt --product-or, we should have autfilt --sum-or and autfilt --sum-and that put the two automata side-by-side and play with the initial states to implement union (non-deterministic initial states) or intersection (universal initial state). See slide 17 of this for an example.

Note that Spot does not support multiple initial states, so we need fake it as already done in the HOA parser. Also another trap is that two two operations requires labeling the one automaton with a set of marks that does not satisfy the acceptance of the other automaton. If the acceptance is a tautology, the acceptance has to be changed (e.g., to Büchi, as done in the complete_here() function).

Assignee
Assign to
Time tracking