From 348f7cce0b80b800c9b9a3132239e37ab642e1e7 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 4 Feb 2016 23:02:28 +0100 Subject: [PATCH] parseaut, dot: install a highlighting framework * spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll: Parse "spot.highlight.edges" and "spot.highlight.states" to fill the "highlight-edges" and "highlight-states" properties. * spot/twaalgos/dot.cc: Use these properties to highlight states. * tests/core/readsave.test: Add a small test. --- spot/parseaut/parseaut.yy | 24 +++++++++ spot/parseaut/scanaut.ll | 2 + spot/twaalgos/dot.cc | 29 +++++++++-- tests/core/readsave.test | 106 +++++++++++++++++++++++++++----------- 4 files changed, 126 insertions(+), 35 deletions(-) diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index 1675b37a6..36ed1be40 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -117,6 +117,8 @@ extern "C" int strverscmp(const char *s1, const char *s2); int plus; int minus; std::vector* state_names = nullptr; + std::map* highlight_edges = nullptr; + std::map* highlight_states = nullptr; std::map states_map; std::set ap_set; unsigned cur_state; @@ -206,6 +208,8 @@ extern "C" int strverscmp(const char *s1, const char *s2); %token BODY "--BODY--" %token END "--END--" %token STATE "State:"; +%token SPOT_HIGHLIGHT_EDGES "spot.highlight.edges:"; +%token SPOT_HIGHLIGHT_STATES "spot.highlight.states:"; %token IDENTIFIER "identifier"; // also used by neverclaim %token HEADERNAME "header name"; %token ANAME "alias name"; @@ -665,6 +669,12 @@ header-item: "States:" INT res.aut_or_ks->set_named_prop("automaton-name", $2); } | "properties:" properties + | "spot.highlight.edges:" + { res.highlight_edges = new std::map; } + highlight-edges + | "spot.highlight.states:" + { res.highlight_states = new std::map; } + highlight-states | HEADERNAME header-spec { char c = (*$1)[0]; @@ -741,6 +751,16 @@ properties: | properties IDENTIFIER } delete $3; } + +highlight-edges: | highlight-edges INT INT + { + res.highlight_edges->emplace($2, $3); + } +highlight-states: | highlight-states INT INT + { + res.highlight_states->emplace($2, $3); + } + header-spec: | header-spec BOOLEAN | header-spec INT | header-spec STRING @@ -2202,6 +2222,10 @@ namespace spot return r.h; if (r.state_names) r.aut_or_ks->set_named_prop("state-names", r.state_names); + if (r.highlight_edges) + r.aut_or_ks->set_named_prop("highlight-edges", r.highlight_edges); + if (r.highlight_states) + r.aut_or_ks->set_named_prop("highlight-states", r.highlight_states); fix_acceptance(r); fix_initial_state(r); fix_properties(r); diff --git a/spot/parseaut/scanaut.ll b/spot/parseaut/scanaut.ll index 163dbc4b0..6fd5264ec 100644 --- a/spot/parseaut/scanaut.ll +++ b/spot/parseaut/scanaut.ll @@ -118,6 +118,8 @@ identifier [[:alpha:]_][[:alnum:]_.-]* "tool:" return token::TOOL; "name:" return token::NAME; "properties:" return token::PROPERTIES; + "spot.highlight.states:" return token::SPOT_HIGHLIGHT_STATES; + "spot.highlight.edges:" return token::SPOT_HIGHLIGHT_EDGES; "--BODY--" return token::BODY; "--END--" BEGIN(INITIAL); return token::END; "State:" return token::STATE; diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 24bba8cce..029c783c4 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -59,6 +59,8 @@ namespace spot bool opt_state_labels_ = false; const_twa_graph_ptr aut_; std::vector* sn_ = nullptr; + std::map* highlight_edges_ = nullptr; + std::map* highlight_states_ = nullptr; std::vector>* sprod_ = nullptr; std::set* incomplete_; std::string* name_ = nullptr; @@ -482,8 +484,6 @@ namespace spot escape_html(os_ << "
", state_label(s)); os_ << '>'; } - os_ << "]\n"; - } else { @@ -502,8 +502,16 @@ namespace spot // states. if (mark_states_ && aut_->state_acc_sets(s)) os_ << ", peripheries=2"; - os_ << "]\n"; } + if (highlight_states_) + { + auto iter = highlight_states_->find(s); + if (iter != highlight_states_->end()) + os_ << ", style=bold, color=\"" + << palette[iter->second % palette_mod] + << '"'; + } + os_ << "]\n"; if (incomplete_ && incomplete_->find(s) != incomplete_->end()) os_ << " u" << s << " [label=\"...\", shape=none, width=0, height=0" "]\n " << s << " -> u" << s << " [style=dashed]\n"; @@ -543,7 +551,16 @@ namespace spot os_ << '>'; } if (opt_numbered_trans) - os_ << ",taillabel=\"" << number << '"'; + os_ << ", taillabel=\"" << number << '"'; + if (highlight_edges_) + { + auto idx = aut_->get_graph().index_of_edge(t); + auto iter = highlight_edges_->find(idx); + if (iter != highlight_edges_->end()) + os_ << ", style=bold, color=\"" + << palette[iter->second % palette_mod] + << '"'; + } os_ << "]\n"; } @@ -584,6 +601,10 @@ namespace spot } } } + highlight_edges_ = + aut->get_named_prop>("highlight-edges"); + highlight_states_ = + aut->get_named_prop>("highlight-states"); incomplete_ = aut->get_named_prop>("incomplete-states"); if (opt_name_) diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 45bff75b8..f37b8869d 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -468,46 +468,46 @@ digraph G { I [label="", style=invis, width=0] I -> 0 0 [label="0"] - 0 -> 1 [label="!a & !b",taillabel="0"] - 0 -> 2 [label="a & !b",taillabel="1"] - 0 -> 3 [label="!a & b",taillabel="2"] - 0 -> 4 [label="a & b",taillabel="3"] + 0 -> 1 [label="!a & !b", taillabel="0"] + 0 -> 2 [label="a & !b", taillabel="1"] + 0 -> 3 [label="!a & b", taillabel="2"] + 0 -> 4 [label="a & b", taillabel="3"] 1 [label="test me\n⓿❸"] - 1 -> 1 [label="!a & !b",taillabel="0"] - 1 -> 2 [label="a & !b",taillabel="1"] - 1 -> 6 [label="!a & b",taillabel="2"] - 1 -> 7 [label="a & b",taillabel="3"] + 1 -> 1 [label="!a & !b", taillabel="0"] + 1 -> 2 [label="a & !b", taillabel="1"] + 1 -> 6 [label="!a & b", taillabel="2"] + 1 -> 7 [label="a & b", taillabel="3"] 2 [label="2\n⓿❷❸"] - 2 -> 1 [label="!a & !b",taillabel="0"] - 2 -> 2 [label="a & !b",taillabel="1"] - 2 -> 6 [label="!a & b",taillabel="2"] - 2 -> 7 [label="a & b",taillabel="3"] + 2 -> 1 [label="!a & !b", taillabel="0"] + 2 -> 2 [label="a & !b", taillabel="1"] + 2 -> 6 [label="!a & b", taillabel="2"] + 2 -> 7 [label="a & b", taillabel="3"] 3 [label="3\n❸"] - 3 -> 5 [label="1",taillabel="0"] + 3 -> 5 [label="1", taillabel="0"] 4 [label="hihi\n❷❸"] - 4 -> 5 [label="1",taillabel="0"] + 4 -> 5 [label="1", taillabel="0"] 5 [label="5\n❶❸"] - 5 -> 5 [label="1",taillabel="0"] + 5 -> 5 [label="1", taillabel="0"] 6 [label="6\n⓿"] - 6 -> 8 [label="!a & !b",taillabel="0"] - 6 -> 6 [label="!a & b",taillabel="1"] - 6 -> 9 [label="a & !b",taillabel="2"] - 6 -> 7 [label="a & b",taillabel="3"] + 6 -> 8 [label="!a & !b", taillabel="0"] + 6 -> 6 [label="!a & b", taillabel="1"] + 6 -> 9 [label="a & !b", taillabel="2"] + 6 -> 7 [label="a & b", taillabel="3"] 7 [label="7\n⓿❷"] - 7 -> 8 [label="!a & !b",taillabel="0"] - 7 -> 6 [label="!a & b",taillabel="1"] - 7 -> 9 [label="a & !b",taillabel="2"] - 7 -> 7 [label="a & b",taillabel="3"] + 7 -> 8 [label="!a & !b", taillabel="0"] + 7 -> 6 [label="!a & b", taillabel="1"] + 7 -> 9 [label="a & !b", taillabel="2"] + 7 -> 7 [label="a & b", taillabel="3"] 8 [label="8\n⓿❸"] - 8 -> 8 [label="!a & !b",taillabel="0"] - 8 -> 6 [label="!a & b",taillabel="1"] - 8 -> 9 [label="a & !b",taillabel="2"] - 8 -> 7 [label="a & b",taillabel="3"] + 8 -> 8 [label="!a & !b", taillabel="0"] + 8 -> 6 [label="!a & b", taillabel="1"] + 8 -> 9 [label="a & !b", taillabel="2"] + 8 -> 7 [label="a & b", taillabel="3"] 9 [label="9\n⓿❷❸"] - 9 -> 8 [label="!a & !b",taillabel="0"] - 9 -> 6 [label="!a & b",taillabel="1"] - 9 -> 9 [label="a & !b",taillabel="2"] - 9 -> 7 [label="a & b",taillabel="3"] + 9 -> 8 [label="!a & !b", taillabel="0"] + 9 -> 6 [label="!a & b", taillabel="1"] + 9 -> 9 [label="a & !b", taillabel="2"] + 9 -> 7 [label="a & b", taillabel="3"] } EOF @@ -961,3 +961,47 @@ State: 1 EOF test `autfilt -c --is-inherently-weak input8` = 0 test `autfilt -c --is-weak input8` = 0 + +cat >input9 < output9 +cat >expected9 < 2 + 0 [label="0", peripheries=2, style=bold, color="#5DA5DA"] + 0 -> 0 [label="1", style=bold, color="#5DA5DA"] + 1 [label="1"] + 1 -> 0 [label="c", style=bold, color="#F17CB0"] + 1 -> 1 [label="b & !c", style=bold, color="#FAA43A"] + 2 [label="2", style=bold, color="#B276B2"] + 2 -> 0 [label="c", style=bold, color="#B276B2"] + 2 -> 1 [label="!a & b & !c"] + 2 -> 2 [label="a & !c"] +} +EOF +diff output9 expected9