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 133
    • Issues 133
    • 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
  • #53
Closed
Open
Issue created Jan 24, 2015 by Alexandre Duret-Lutz@adlOwner

rename atomic propositions before calling ltl3ba

ltl3ba, like ltl2ba and spin, require atomic propositions to start with a lowercase letter. As a consequence, the ltl2tgba.html page fails to translate the formula F(A) with ltl3ba.

We could however relabel all the atomic propositions before calling ltl3ba and then map the labels of the resulting automaton back to their original name before we display the automaton.

Rather than doing this in the CGI script, maybe this service could be provided by a command-line tool that can wrap ltl3ba, ltl2ba, or spin, and allow these tools to take many formulas as input, and output the result in all the format we supports.

Assignee
Assign to
Time tracking