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 134
    • Issues 134
    • 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
  • #290
Closed
Open
Issue created Oct 02, 2017 by Alexandre Duret-Lutz@adlOwner

ltl2tgba --parity and autfilt --parity

Currently ltl2tgba -G -D can return deterministic generalized Büchi or parity. For people who absolutely need parity automata, it would be nice to have a --parity option.

This means adding parity output to spot::postprocessor, and then of course we also want --parity in autfilt. So we cannot just assume the input will be generalized Büchi or parity.

It seems @max has some code for converting Rabin or Streett to parity, can this be adapted to generalized Rabin and generalized Streett? (It would be horrible if our conversion for arbitrary acceptance to parity had to go through NBA).

Ideally, I'd also like to be able to say that I want a special type of parity (like max even, or that I don't care). @lxu wrote several functions to convert one type of parity to another, so this part would be just devising the spot::postprocessor interface to specify those desires and the calling the right functions.

Assignee
Assign to
Time tracking