From 4855d3c8778e6fc51ce2483f6eef8cf637a51a66 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 2 Sep 2021 22:43:22 +0200 Subject: [PATCH] dot: add an option to output id= attributes This will be handy latter to develop widgets with interactive highlighting of automata. * spot/twaalgos/dot.cc: Implement it. * bin/common_aoutput.cc, NEWS, doc/org/oaut.org, doc/org/spot.css: Document it. * tests/core/alternating.test, tests/core/readsave.test, tests/core/sccdot.test: Test it. --- NEWS | 8 +++ bin/common_aoutput.cc | 6 +- doc/org/oaut.org | 63 ++++++++++++++---- doc/org/spot.css | 4 ++ spot/twaalgos/dot.cc | 48 ++++++++++++-- tests/core/alternating.test | 124 +++++++++++++++++++----------------- tests/core/readsave.test | 28 ++++---- tests/core/sccdot.test | 61 ++++++++++-------- 8 files changed, 230 insertions(+), 112 deletions(-) diff --git a/NEWS b/NEWS index 121990d4d..6f4d7d37f 100644 --- a/NEWS +++ b/NEWS @@ -129,6 +129,14 @@ New in spot 2.9.8.dev (not yet released) - print_dot() will display states from player 1 using a diamond shape. + - print_dot() has a new option "i" to define id=... attributes for + states (S followed by the state number), edges (E followed by the + edge number), and SCCs (SCC followed by SCC number). The option + "i(graphid)" will also set the id of the graph. These id + attributes are useful if an automaton is converted into SVG and + one needs to refer to some particular state/edge/SCC with CSS or + javascript. See https://spot.lrde.epita.fr/oaut.html#SVG-and-CSS + - spot::postproc has new configuration variables that define thresholds to disable some costly operation in order to speedup the processing of large automata. (Those variables are typically diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index 3d1802dbb..665fafc67 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -97,7 +97,8 @@ static const argp_option options[] = /**************************************************/ { nullptr, 0, nullptr, 0, "Output format:", 3 }, { "dot", 'd', - "1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT|get_graph().index_of_edge(t); os_ << '"'; } + if (opt_id_) + { + unsigned index = aut_->get_graph().index_of_edge(t); + os_ << ", id=\"E" << index << '"'; + // Somehow \E must appear as \\E in tooltip in + // graphviz 2.43.0; this looks like a bug. + os_ << ", tooltip=\"\\\\E\\n#" << index << '"'; + } } - std::string highlight; int color_num = -1; if (highlight_edges_) @@ -966,6 +1004,8 @@ namespace spot // May only occur if the call to // determine_unknown_acceptance() above is removed. os_ << " color=orange\n"; + if (opt_id_) + os_ << " id=\"SCC" << i << "\"\n"; if (name_ || opt_show_acc_) { diff --git a/tests/core/alternating.test b/tests/core/alternating.test index ec6b8a511..17f012675 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -55,76 +55,87 @@ EOF test "1 2 4" = "`autfilt --stats='%u %[s]u %[e]u' alt.hoa`" -autfilt --has-univ-branch --has-exist-branch --dot=bans alt.hoa >alt.dot +autfilt --has-univ-branch --has-exist-branch --dot=bansi alt.hoa >alt.dot +aho='arrowhead=onormal' +b='style=bold,' +tE='tooltip="\\E' cat >expect.dot < -11 [arrowhead=onormal] + I -> -11 [$aho] subgraph cluster_0 { color=green + id="SCC0" label="" 2 [label="G(a)"] } subgraph cluster_1 { color=red + id="SCC1" label="" 1 [label="FG(a)\n⓿"] } subgraph cluster_2 { color=green + id="SCC2" label="" 6 [label="t"] } subgraph cluster_3 { color=red + id="SCC3" label="" 4 [label="F(b)\n⓿"] } subgraph cluster_4 { color=green + id="SCC4" label="" 3 [label="GF(b)"] -8 [label=<>,shape=point,width=0.05,height=0.05] } subgraph cluster_5 { color=red + id="SCC5" label="" 5 [label="((a) U (b))\n⓿"] } subgraph cluster_6 { color=black + id="SCC6" label="" 0 [label="((((a) U (b)) && GF(b)) && FG(a))"] } -11 [label=<>,shape=point,width=0.05,height=0.05] - -11 -> 0 - -11 -> 2 - 0 -> -1 [label="b", arrowhead=onormal] + -11 -> 0 [id="E-11E0"] + -11 -> 2 [id="E-11E2"] + 0 -> -1 [label="b", id="E1", $tE\n#1", $aho] -1 [label=<>,shape=point,width=0.05,height=0.05] - -1 -> 1 - -1 -> 3 - 0 -> -4 [label="a & !b", style=bold, color="#E31A1C", arrowhead=onormal] + -1 -> 1 [id="E-1E1"] + -1 -> 3 [id="E-1E3"] + 0 -> -4 [label="a & !b", id="E2", $tE\n#2", $b color="#E31A1C", $aho] -4 [label=<>,shape=point,width=0.05,height=0.05] - -4 -> 1 [style=bold, color="#E31A1C"] - -4 -> 3 [style=bold, color="#E31A1C"] - -4 -> 5 [style=bold, color="#E31A1C"] - 1 -> 2 [label="a"] - 1 -> 1 [label="1"] - 2 -> 2 [label="a"] - 3 -> 3 [label="b"] - 3 -> -8 [label="!b", style=bold, color="#FF7F00", arrowhead=onormal] - -8 -> 3 [style=bold, color="#FF7F00"] - -8 -> 4 [style=bold, color="#FF7F00"] - 4 -> 6 [label="b"] - 4 -> 4 [label="!b"] - 5 -> 6 [label="b"] - 5 -> 5 [label="a & !b"] - 6 -> 6 [label="1"] + -4 -> 1 [$b color="#E31A1C",id="E-4E1"] + -4 -> 3 [$b color="#E31A1C",id="E-4E3"] + -4 -> 5 [$b color="#E31A1C",id="E-4E5"] + 1 -> 2 [label="a", id="E3", $tE\n#3"] + 1 -> 1 [label="1", id="E4", $tE\n#4"] + 2 -> 2 [label="a", id="E5", $tE\n#5"] + 3 -> 3 [label="b", id="E6", $tE\n#6"] + 3 -> -8 [label="!b", id="E7", $tE\n#7", $b color="#FF7F00", $aho] + -8 -> 3 [$b color="#FF7F00",id="E-8E3"] + -8 -> 4 [$b color="#FF7F00",id="E-8E4"] + 4 -> 6 [label="b", id="E8", $tE\n#8"] + 4 -> 4 [label="!b", id="E9", $tE\n#9"] + 5 -> 6 [label="b", id="E10", $tE\n#10"] + 5 -> 5 [label="a & !b", id="E11", $tE\n#11"] + 6 -> 6 [label="1", id="E12", $tE\n#12"] } EOF @@ -502,7 +513,6 @@ EOF run 0 autfilt --dot='baryf(Lato)' ex6 > ex6.dot -style='arrowhead=onormal' cat >expect6.dot< -1 [arrowhead=onormal] + I -> -1 [$aho] -1 [label=<>,shape=point,width=0.05,height=0.05] -1 -> 0 -1 -> 1 0 [label=<0>] 0 -> 0 [label=] - 0 -> -1.1 [label=, style=bold, color="#FF4DA0", $style] + 0 -> -1.1 [label=, $b color="#FF4DA0", $aho] -1.1 [label=<>,shape=point,width=0.05,height=0.05] - -1.1 -> 0 [style=bold, color="#FF4DA0"] - -1.1 -> 1 [style=bold, color="#FF4DA0"] - 0 -> -1.2 [label=, style=bold, color="#FF7F00", arrowhead=onormal] + -1.1 -> 0 [$b color="#FF4DA0"] + -1.1 -> 1 [$b color="#FF4DA0"] + 0 -> -1.2 [label=, $b color="#FF7F00", $aho] -1.2 [label=<>,shape=point,width=0.05,height=0.05] - -1.2 -> 0 [style=bold, color="#FF7F00"] - -1.2 -> 1 [style=bold, color="#FF7F00"] + -1.2 -> 0 [$b color="#FF7F00"] + -1.2 -> 1 [$b color="#FF7F00"] 1 [label=<1>] 1 -> 1 [label=] } @@ -608,16 +618,16 @@ digraph "SLAA for c R (c | G(a & b) | (F!b & F!a))" { } 0 -> 4 [label=] 0 -> 0 [label=] - 0 -> -1 [label=, arrowhead=onormal] + 0 -> -1 [label=, $aho] -1 -> 0 -1 -> 1 - 0 -> -4 [label=, arrowhead=onormal] + 0 -> -4 [label=, $aho] -4 -> 0 -4 -> 2 - 0 -> -7 [label=, arrowhead=onormal] + 0 -> -7 [label=, $aho] -7 -> 0 -7 -> 3 - 0 -> -10 [label=, arrowhead=onormal] + 0 -> -10 [label=, $aho] -10 -> 0 -10 -> 2 -10 -> 3 @@ -701,17 +711,17 @@ digraph "SLAA for c R (c | G(a & b) | (F!b & F!a))" { } 0 -> 4 [label=] 0 -> 0 [label=] - 0 -> -1 [label=, arrowhead=onormal] + 0 -> -1 [label=, $aho] -1 -> 0 -1 -> 1 - 0 -> -4 [label=, arrowhead=onormal] + 0 -> -4 [label=, $aho] -4 -> 0 -4 -> 2 - 0 -> -7 [label=, arrowhead=onormal] + 0 -> -7 [label=, $aho] -7 -> 0 -7 -> 3 1 -> 1 [label=] - 1 -> -10 [label=, arrowhead=onormal] + 1 -> -10 [label=, $aho] -10 -> 0 -10 -> 2 -10 -> 3 @@ -756,17 +766,17 @@ digraph "" { I [label="", style=invis, width=0] I -> 0 0 [label=<0>] - 0 -> -1.1 [label=, style=bold, color="#FF4DA0", arrowhead=onormal] + 0 -> -1.1 [label=, $b color="#FF4DA0", $aho] -1.1 [label=<>,shape=point,width=0.05,height=0.05] - -1.1 -> 1 [style=bold, color="#FF4DA0"] - -1.1 -> 2 [style=bold, color="#FF4DA0"] + -1.1 -> 1 [$b color="#FF4DA0"] + -1.1 -> 2 [$b color="#FF4DA0"] 1 [label=<1>] - 1 -> -1.1 [label=, style=bold, color="#FF4DA0", arrowhead=onormal] + 1 -> -1.1 [label=, $b color="#FF4DA0", $aho] 2 [label=<2>] - 2 -> -1.2 [label=, style=bold, color="#FF7F00", $style] + 2 -> -1.2 [label=, $b color="#FF7F00", $aho] -1.2 [label=<>,shape=point,width=0.05,height=0.05] - -1.2 -> 1 [style=bold, color="#FF7F00"] - -1.2 -> 2 [style=bold, color="#FF7F00"] + -1.2 -> 1 [$b color="#FF7F00"] + -1.2 -> 2 [$b color="#FF7F00"] } EOF @@ -803,20 +813,20 @@ digraph "" { I [label="", style=invis, width=0] I -> 0 0 [label=<0>] - 0 -> -1.1 [label=, style=bold, color="#FF4DA0", arrowhead=onormal] + 0 -> -1.1 [label=, $b color="#FF4DA0", $aho] -1.1 [label=<>,shape=point,width=0.05,height=0.05] - -1.1 -> 1 [style=bold, color="#FF4DA0"] - -1.1 -> 2 [style=bold, color="#FF4DA0"] + -1.1 -> 1 [$b color="#FF4DA0"] + -1.1 -> 2 [$b color="#FF4DA0"] 1 [label=<1>] - 1 -> -1.3 [label=, style=bold, color="#6A3D9A", arrowhead=onormal] + 1 -> -1.3 [label=, $b color="#6A3D9A", $aho] -1.3 [label=<>,shape=point,width=0.05,height=0.05] - -1.3 -> 1 [style=bold, color="#6A3D9A"] - -1.3 -> 2 [style=bold, color="#6A3D9A"] + -1.3 -> 1 [$b color="#6A3D9A"] + -1.3 -> 2 [$b color="#6A3D9A"] 2 [label=<2>] - 2 -> -1.2 [label=, style=bold, color="#FF7F00", $style] + 2 -> -1.2 [label=, $b color="#FF7F00", $aho] -1.2 [label=<>,shape=point,width=0.05,height=0.05] - -1.2 -> 1 [style=bold, color="#FF7F00"] - -1.2 -> 2 [style=bold, color="#FF7F00"] + -1.2 -> 1 [$b color="#FF7F00"] + -1.2 -> 2 [$b color="#FF7F00"] } EOF @@ -881,10 +891,10 @@ digraph "SLAA for G((b & Fa) | (!b & G!a))" { -4 [label=<>,shape=point,width=0.05,height=0.05] } 0 -> 0 [label=] - 0 -> -1 [label=, arrowhead=onormal] + 0 -> -1 [label=, $aho] -1 -> 0 -1 -> 1 - 0 -> -4 [label=, arrowhead=onormal] + 0 -> -4 [label=, $aho] -4 -> 0 -4 -> 2 1 -> 3 [label=] diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 55006b712..400d55d9a 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -314,34 +314,38 @@ EOF autfilt -H input | SPOT_DEFAULT_FORMAT=dot \ - SPOT_DOTDEFAULT=vcsnaA \ + SPOT_DOTDEFAULT=vcsnaAi \ SPOT_DOTEXTRA='/* hello world */' \ autfilt >output cat >expected < 3 subgraph cluster_0 { color=green + id="SCC0" 1 [label="s1", peripheries=2] } subgraph cluster_1 { color=green + id="SCC1" 0 [label="s0", peripheries=2] } subgraph cluster_2 { color=black + id="SCC2" 3 [label="s3"] } - 0 -> 0 [label="b"] - 1 -> 1 [label="a"] + 0 -> 0 [label="b", id="E1", tooltip="\\\\E\n#1"] + 1 -> 1 [label="a", id="E2", tooltip="\\\\E\n#2"] 2 [label="s2"] - 2 -> 0 [label="b"] - 3 -> 1 [label="a"] - 3 -> 0 [label="b"] + 2 -> 0 [label="b", id="E3", tooltip="\\\\E\n#3"] + 3 -> 1 [label="a", id="E4", tooltip="\\\\E\n#4"] + 3 -> 0 [label="b", id="E5", tooltip="\\\\E\n#5"] } EOF @@ -371,7 +375,7 @@ digraph "G(Fa & Fb)" { EOF diff output expected -ltl2tgba -dban 'GFa & GFb' >output +ltl2tgba -d'bani(foo)' 'GFa & GFb' >output cat output cat >expected < 0 0 [label="0"] - 0 -> 0 [label="!a & !b"] - 0 -> 0 [label="a & !b\n⓿"] - 0 -> 0 [label="!a & b\n❶"] - 0 -> 0 [label="a & b\n⓿❶"] + 0 -> 0 [label="!a & !b", id="E1", tooltip="\\\\E\n#1"] + 0 -> 0 [label="a & !b\n⓿", id="E2", tooltip="\\\\E\n#2"] + 0 -> 0 [label="!a & b\n❶", id="E3", tooltip="\\\\E\n#3"] + 0 -> 0 [label="a & b\n⓿❶", id="E4", tooltip="\\\\E\n#4"] } EOF diff output expected diff --git a/tests/core/sccdot.test b/tests/core/sccdot.test index 1c3049cd7..68a4aedee 100755 --- a/tests/core/sccdot.test +++ b/tests/core/sccdot.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2015, 2017, 2018, 2020 Laboratoire de Recherche et -# Développement de l'Epita +# Copyright (C) 2015, 2017, 2018, 2020, 2021 Laboratoire de Recherche +# et Développement de l'Epita # # This file is part of Spot, a model checking library. # @@ -68,7 +68,7 @@ State: 10 --END-- EOF -run 0 autfilt --dot=as in.hoa > out.dot +run 0 autfilt --dot=asi in.hoa > out.dot # The important stuff is the color=xxx lines cat <expected @@ -77,79 +77,88 @@ digraph "" { label="(Inf(0)&Inf(1)) & Fin(2)\n[Streett-like 3]" labelloc="t" node [shape="ellipse",width="0.5",height="0.5"] + node [id="S\N"] I [label="", style=invis, width=0] I -> 1 subgraph cluster_0 { color=grey + id="SCC0" label="" 5 [label="5"] 6 [label="6"] } subgraph cluster_1 { color=grey + id="SCC1" label="" 0 [label="0"] } subgraph cluster_2 { color=green + id="SCC2" label="" 9 [label="9"] 10 [label="10"] } subgraph cluster_3 { color=green + id="SCC3" label="" 8 [label="8"] } subgraph cluster_4 { color=green + id="SCC4" label="" 7 [label="7"] } subgraph cluster_5 { color=black + id="SCC5" label="" 2 [label="2"] } subgraph cluster_6 { color=red + id="SCC6" label="" 4 [label="4"] } subgraph cluster_7 { color=green + id="SCC7" label="" 1 [label="1"] 3 [label="3"] } - 0 -> 0 [label="a & b\n{0,1,2}"] - 0 -> 0 [label="!a & !b\n{2}"] - 0 -> 5 [label="a\n{2}"] - 1 -> 4 [label="b"] - 1 -> 3 [label="a & !b"] - 2 -> 0 [label="a"] - 2 -> 7 [label="b"] - 3 -> 1 [label="a & b\n{0,1}"] - 4 -> 4 [label="!b\n{1,2}"] - 4 -> 2 [label="b"] - 5 -> 6 [label="1"] - 6 -> 5 [label="1"] - 7 -> 7 [label="!a & b\n{0,1}"] - 7 -> 7 [label="a & b\n{0,2}"] - 7 -> 8 [label="1"] - 8 -> 8 [label="!a & b\n{0,2}"] - 8 -> 8 [label="a & b\n{0,1}"] - 8 -> 9 [label="1"] - 9 -> 9 [label="!a & b\n{0,2}"] - 9 -> 10 [label="a & b\n{0,1}"] - 10 -> 9 [label="!a & b\n{0,1}"] - 10 -> 10 [label="a & b\n{0,2}"] + 0 -> 0 [label="a & b\n{0,1,2}", id="E1", tooltip="\\\\E\n#1"] + 0 -> 0 [label="!a & !b\n{2}", id="E2", tooltip="\\\\E\n#2"] + 0 -> 5 [label="a\n{2}", id="E3", tooltip="\\\\E\n#3"] + 1 -> 4 [label="b", id="E4", tooltip="\\\\E\n#4"] + 1 -> 3 [label="a & !b", id="E5", tooltip="\\\\E\n#5"] + 2 -> 0 [label="a", id="E8", tooltip="\\\\E\n#8"] + 2 -> 7 [label="b", id="E9", tooltip="\\\\E\n#9"] + 3 -> 1 [label="a & b\n{0,1}", id="E10", tooltip="\\\\E\n#10"] + 4 -> 4 [label="!b\n{1,2}", id="E6", tooltip="\\\\E\n#6"] + 4 -> 2 [label="b", id="E7", tooltip="\\\\E\n#7"] + 5 -> 6 [label="1", id="E11", tooltip="\\\\E\n#11"] + 6 -> 5 [label="1", id="E12", tooltip="\\\\E\n#12"] + 7 -> 7 [label="!a & b\n{0,1}", id="E13", tooltip="\\\\E\n#13"] + 7 -> 7 [label="a & b\n{0,2}", id="E14", tooltip="\\\\E\n#14"] + 7 -> 8 [label="1", id="E15", tooltip="\\\\E\n#15"] + 8 -> 8 [label="!a & b\n{0,2}", id="E16", tooltip="\\\\E\n#16"] + 8 -> 8 [label="a & b\n{0,1}", id="E17", tooltip="\\\\E\n#17"] + 8 -> 9 [label="1", id="E18", tooltip="\\\\E\n#18"] + 9 -> 9 [label="!a & b\n{0,2}", id="E19", tooltip="\\\\E\n#19"] + 9 -> 10 [label="a & b\n{0,1}", id="E20", tooltip="\\\\E\n#20"] + 10 -> 9 [label="!a & b\n{0,1}", id="E21", tooltip="\\\\E\n#21"] + 10 -> 10 [label="a & b\n{0,2}", id="E22", tooltip="\\\\E\n#22"] } EOF diff out.dot expected -# While we are here, make sure scc_filter remove those grey SCCs. +# While we are here, make sure scc_filter removes those grey SCCs. autfilt --small -x simul=0 in.hoa -H > out.hoa cat >expected.hoa <