Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
Spot
Spot
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 117
    • Issues 117
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 1
    • Merge Requests 1
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Spot
  • SpotSpot
  • Issues
  • #207

Closed
Open
Opened Jan 26, 2017 by Alexandre Duret-Lutz@adlOwner

fix highlighting of edges in automata

Spot knows how to highlight some specific edges in automata. For instance:

% cat >foo2.hoa <<EOF
HOA: v1.1
name: "(Gb | F!a) W c"
States: 5
Start: 1
AP: 3 "b" "a" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc !complete
properties: !deterministic stutter-invariant !terminal
spot.highlight.edges: 2 1 5 1 7 2  /* <----------- NOTE */
--BODY--
State: 0
[0] 0 {0}
State: 1
[0&1&!2] 0
[!1&!2] 1 {0}
[1&!2] 2
[2] 3
State: 2
[!1&!2] 1 {0}
[1&!2] 2
[!1&2] 3
[1&2] 4
State: 3
[t] 3 {0}
State: 4
[!1] 3
[1] 4
--END--
EOF
% autfilt foo2.hoa --dot='barf(Lato)' | dot -Tpng > foo2.png

foo2

The custom spot.highlight.edges: header is described on the HOA support page.

Highlight edges in alternating automata, this does not work as well. For instance this is ok:

% cat >foo3.hoa <<EOF
HOA: v1.1
name: "SLAA for c R (c | Gb | F!a)"
States: 4
Start: 0
AP: 3 "c" "b" "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc
properties: !complete !deterministic
spot.highlight.edges: 3 1 4 2
--BODY--
State: 0 "c R (c | Gb | F!a)"
[0] 3
[!0&!2] 0
[!0&1&2] 0&1
[!0&2] 0&2
State: 1 "Gb"
[1] 1
State: 2 "F!a"
[!2] 3
[2] 2 {0}
State: 3 "t"
[t] 3
--END--
% autfilt foo3.hoa --dot='barf(Lato)' | dot -Tpng >foo3.png
EOF

foo3

However if two edges have the same universal destination, the coloring cannot cover the entire universal edge, as the destinations are shared:

% cat >foo4.hoa <<EOF
HOA: v1.1
States: 2
Start: 0&1
AP: 3 "c" "b" "a"
Acceptance: 1 Fin(0)
spot.highlight.edges: 2 1 3 2
--BODY--
State: 0
[!0&!2] 0
[!0&1&2] 0&1
[!0&2] 0&1
State: 1
[1] 1
--END--
% autfilt foo4.hoa --dot='barf(Lato)' | dot -Tpng >foo4.png
EOF

foo4

We need an additional option to "unshare" the destinations that have different colors. Let's call this option 'y' (because it evokes the shape of the universal edges). On this example we would have this:

autfilt foo4.hoa --dot='baryf(Lato)' | dot -Tpng > foo5.png

foo5

A simple implementation, that still allows sharing destination groups for transitions that have the same color, would be to include the color number in the name the intermediate node representing destination groups.

digraph G {
  rankdir=LR
  label=<Fin(<font color="#5DA5DA">⓿</font>)>
  labelloc="t"
  node [shape="circle"]
  fontname="Lato"
  node [fontname="Lato"]
  edge [fontname="Lato"]
  I [label="", style=invis, width=0]
  I -> -1 [arrowhead=onormal]
    -1 [label=<>,shape=point]
    -1 -> 0
    -1 -> 1
  0 [label=<0>]
  0 -> 0 [label=<!a &amp; !c>]
  0 -> -1.1 [label=<a &amp; b &amp; !c>, style=bold, color="#F17CB0", arrowhead=onormal]
    -1.1 [label=<>,shape=point]
    -1.1 -> 0 [style=bold, color="#F17CB0"]
    -1.1 -> 1 [style=bold, color="#F17CB0"]
  0 -> -1.2 [label=<a &amp; !c>, style=bold, color="#FAA43A", arrowhead=onormal]
    -1.2 [label=<>,shape=point]
    -1.2 -> 0 [style=bold, color="#FAA43A"]
    -1.2 -> 1 [style=bold, color="#FAA43A"]
  1 [label=<1>]
  1 -> 1 [label=<b>]
}

Here -1 is the uncolored destination group 1, -1.1 is the same group with color 1, and -1.2 is that group with color 2.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Spot 2.3.1
Milestone
Spot 2.3.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: spot/spot#207