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
  • #1
Closed
Open
Issue created Dec 05, 2014 by Alexandre Duret-Lutz@adlOwner

get rid of the TGBA parser

The parser in src/tgbaparse/ was implemented very early in the history of Spot as a quick way to input TGBA to perform tests. Its implementation and syntax is gross.

Now that Spot can read TGBA as HOA files, there is no reason to keep this parser around. We should update all our tests to read and write HOA instead, and get rid of the parser.

Unfortunately there is one public use of the old format: ltl3ba has an option to output its intermediate TGBA in this format, and we use it in the oneline ltl2tgba.html interface. We should ask the ltl3ba authors to upgrade to HOA. I know they plan to do it for ltl3dra, and patches exists for ltl2ba to output HOA, so they should not have a problem updating ltl3ba.

Assignee
Assign to
Time tracking