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 132
    • Issues 132
    • 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
  • #270
Closed
Open
Issue created Jun 20, 2017 by Alexandre Duret-Lutz@adlOwner

remove_fin can trigger an assert in streett_to_generalized_buchi

@tmedioni, the Debian builds of next are failing core/ltl3dra.test, and I suspect this is due to some of your recent changes. This test is skipped by most other builds because ltl3dra is not installed, so I'm not surprised the issue went unnoticed.

The file foo.hoa was generated with

% ltl3dra -f '!(<>((((p0) && (!(<>(p2)))) || ((!(p0)) && (<>(p2)))) U ((((p0) && (!(<>(p2)))) || ((!(p0)) && (<>(p2)))) && (<>(((p0) && (!([](((!(p1)) && ([](p3))) || ((p1) && (!([](p3)))))))) || ((!(p0)) && ([](((!(p1)) && ([](p3))) || ((p1) && (!([](p3))))))))))))' | bin/autfilt --complement | fmt > foo.hoa

the failure can be reproduced with

% bin/autfilt --remove-fin foo.hoa
autfilt: streett_to_generalized_buchi() should only be called on automata with Streett-like acceptance

Could you have a look?

Edited Jun 21, 2017 by Alexandre Duret-Lutz
Assignee
Assign to
Time tracking