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
  • #357
Closed
Open
Issue created Jun 29, 2018 by Alexandre Duret-Lutz@adlOwner

two formulas that cannot be translated one after the other

Translating these two formulas fails on the second one. However translating each formula separately works. Also adding -xgf-guarantee=0 gets rid of the issue.

% ltl2tgba  -D 'a | Fb' 'GF((!c | XXc) & d)'
HOA: v1
name: "a | Fb"
States: 3
Start: 2
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic stutter-invariant terminal
--BODY--
State: 0 {0}
[t] 0
State: 1
[1] 0
[!1] 1
State: 2
[0 | 1] 0
[!0&!1] 1
--END--
ltl2tgba: print_hoa(): automaton is not universal but prop_universal()==true
Assignee
Assign to
Time tracking