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 117
    • Issues 117
    • 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
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Spot
  • SpotSpot
  • Issues
  • #348

Closed
Open
Opened May 14, 2018 by Alexandre Duret-Lutz@adlOwner

autfilt -B --product should not run out of acceptance sets

Jeroen Meijer reports that if we do many products with autfilt, as in:

autfilt -B 1.hoa --product 2.hoa --product 3.hoa ... --product 40.hoa

you can run out of acceptance sets, despite the fact that we are building a Büchi automaton (-B). This is because autfilt builds a GBA for the whole product sequence before degeneralizing it.

We should probably degeneralize as we progress (or whenever we detect that a product will fail) when option -B is given. BTW, I suspect it's better to use transition-based BA as intermediate automata even if the final result will be state-based.

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
Reference: spot/spot#348