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
  • #282
Closed
Open
Issue created Sep 15, 2017 by Alexandre Duret-Lutz@adlOwner

another case where ltl2tgba produces different outputs depending on the history

The last line of the output of each of the following three commands ought to be the same. Those large discrepancies are alarming.

% genltl --ms-phi-r=2 --ms-phi-s=2 | ltl2tgba -G -D --stats=%s
25
642
% genltl --ms-phi-s=2 | ltl2tgba -G -D --stats=%s
1238
% genltl --ms-phi-s=1..2 | ltl2tgba -G -D --stats=%s
7
1322

I can't reproduce the issue without -G -D so I'm inclined to think it's related to the way tgba_determinize() works. Maybe it relies on some BDD order that has been altered by a previous translation?

Edited Sep 16, 2017 by Alexandre Duret-Lutz
Assignee
Assign to
Time tracking