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 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
  • #315

Closed
Open
Opened Jan 05, 2018 by Alexandre Duret-Lutz@adlOwner

bogus acceptance simplification

This simplification seems incorrect. In the first automaton, the self-loop on state 0 is accepting (thanks to Fin(1)) but in the second it is rejecting.

% ltl2tgba -G -D 'FGa' | autfilt --complement

in

% ltl2tgba -G -D 'FGa' | autfilt --complement | autfilt --simplify-acceptance

out

To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information
Assignee
Assign to
Spot 2.5
Milestone
Spot 2.5
Assign milestone
Time tracking
None
Due date
None
Reference: spot/spot#315