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
  • #208
Closed
Open
Issue created Jan 26, 2017 by Alexandre Duret-Lutz@adlOwner

better highlighting of SCCs in alternating automata

The problem is where to put the intermediate node relative to the SCC cluster.

Compare:

ltl3hoa -p1 -f '(Ga <-> Gb) W c' | autfilt --dot='barf(Lato)' | dot -Tpng > out1.png

out1

which is quite readable, to this:

ltl3hoa -p1 -f '(Ga <-> Gb) W c' | autfilt --dot='sbarf(Lato)' | dot -Tpng > out2.png

out2

which is a mess, because the intermediate nodes of universal edges are kept out of the SCC clusters.

It seems it would be more readable if, when an universal edge has a destination that is in the same SCC as its source, then we output the intermediate node in the SCC's cluster. E.g.:

out3

Doing this, we will have a problem similar to #207 (closed), were an intermediate node may be shared by different edges, and might need to be in several clusters (or no cluster at all). We want to duplicate them in the same way. It seems it is enough to include the name of the SCC cluster in label the intermediate node, as suggested for the colors in #207 (closed).

Assignee
Assign to
Time tracking