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.
This commit is contained in:
Alexandre Duret-Lutz
parent
91bb93eeaa
commit
348f7cce0b
4 changed files with 126 additions and 35 deletions
|
|
@ -117,6 +117,8 @@ extern "C" int strverscmp(const char *s1, const char *s2);
|
|||
int plus;
|
||||
int minus;
|
||||
std::vector<std::string>* state_names = nullptr;
|
||||
std::map<unsigned, unsigned>* highlight_edges = nullptr;
|
||||
std::map<unsigned, unsigned>* highlight_states = nullptr;
|
||||
std::map<unsigned, unsigned> states_map;
|
||||
std::set<int> 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 <str> IDENTIFIER "identifier"; // also used by neverclaim
|
||||
%token <str> HEADERNAME "header name";
|
||||
%token <str> 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<unsigned, unsigned>; }
|
||||
highlight-edges
|
||||
| "spot.highlight.states:"
|
||||
{ res.highlight_states = new std::map<unsigned, unsigned>; }
|
||||
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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -59,6 +59,8 @@ namespace spot
|
|||
bool opt_state_labels_ = false;
|
||||
const_twa_graph_ptr aut_;
|
||||
std::vector<std::string>* sn_ = nullptr;
|
||||
std::map<unsigned, unsigned>* highlight_edges_ = nullptr;
|
||||
std::map<unsigned, unsigned>* highlight_states_ = nullptr;
|
||||
std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
|
||||
std::set<unsigned>* incomplete_;
|
||||
std::string* name_ = nullptr;
|
||||
|
|
@ -482,8 +484,6 @@ namespace spot
|
|||
escape_html(os_ << "<br/>", 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<std::map<unsigned, unsigned>>("highlight-edges");
|
||||
highlight_states_ =
|
||||
aut->get_named_prop<std::map<unsigned, unsigned>>("highlight-states");
|
||||
incomplete_ =
|
||||
aut->get_named_prop<std::set<unsigned>>("incomplete-states");
|
||||
if (opt_name_)
|
||||
|
|
|
|||
|
|
@ -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 <<EOF
|
||||
HOA: v1
|
||||
name: "a U (b U c)"
|
||||
States: 3
|
||||
Start: 2
|
||||
AP: 3 "a" "b" "c"
|
||||
acc-name: Buchi
|
||||
Acceptance: 1 Inf(0)
|
||||
properties: trans-labels explicit-labels state-acc deterministic
|
||||
properties: stutter-invariant terminal
|
||||
spot.highlight.edges: 1 0 2 1 3 2 4 3
|
||||
spot.highlight.states: 0 0 2 3
|
||||
--BODY--
|
||||
State: 0 {0}
|
||||
[t] 0
|
||||
State: 1
|
||||
[2] 0
|
||||
[1&!2] 1
|
||||
State: 2
|
||||
[2] 0
|
||||
[!0&1&!2] 1
|
||||
[0&!2] 2
|
||||
--END--
|
||||
EOF
|
||||
autfilt -d input9 > output9
|
||||
cat >expected9 <<EOF
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue