Skip to content

GitLab

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

Closed
Open
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).

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