Commit 34859568 authored by Arthur Remaud's avatar Arthur Remaud

autfilt: add option (y) to --dot to split universal transitions

Fixes #207

* NEWS: Informations about the option 'y' for --dot added
* bin/common_aoutput.cc: Documentation for the option 'y'
for --dot added
* spot/twaalgos/dot.cc (print_dst, process_link): Functions
modified for the new option
* tests/core/alternating.test: Tests added
parent 5516209d
...@@ -9,6 +9,9 @@ New in spot 2.3.0.dev (not yet released) ...@@ -9,6 +9,9 @@ New in spot 2.3.0.dev (not yet released)
- The colors used in the output of ltlcross have been adjusted to - The colors used in the output of ltlcross have been adjusted to
work better with white backgrounds and black backgrounds. work better with white backgrounds and black backgrounds.
- The option (y) has been added to --dot. It splits the universal
edges with the same targets but different colors.
Library: Library:
- spot::twa_run::as_twa() has an option to preserve state names. - spot::twa_run::as_twa() has an option to preserve state names.
......
...@@ -85,7 +85,7 @@ static const argp_option options[] = ...@@ -85,7 +85,7 @@ static const argp_option options[] =
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Output format:", 3 }, { nullptr, 0, nullptr, 0, "Output format:", 3 },
{ "dot", 'd', { "dot", 'd',
"1|a|b|B|c|C(COLOR)|e|f(FONT)|h|k|n|N|o|r|R|s|t|v|+INT|<INT|#", "1|a|b|B|c|C(COLOR)|e|f(FONT)|h|k|n|N|o|r|R|s|t|v|y|+INT|<INT|#",
OPTION_ARG_OPTIONAL, OPTION_ARG_OPTIONAL,
"GraphViz's format. Add letters for " "GraphViz's format. Add letters for "
"(1) force numbered states, " "(1) force numbered states, "
...@@ -102,6 +102,7 @@ static const argp_option options[] = ...@@ -102,6 +102,7 @@ static const argp_option options[] =
"(R) color acceptance sets by Inf/Fin, (s) with SCCs, " "(R) color acceptance sets by Inf/Fin, (s) with SCCs, "
"(t) force transition-based acceptance, " "(t) force transition-based acceptance, "
"(v) vertical layout, " "(v) vertical layout, "
"(y) split universal edges by color, "
"(+INT) add INT to all set numbers, " "(+INT) add INT to all set numbers, "
"(<INT) display at most INT states, " "(<INT) display at most INT states, "
"(#) show internal edge numbers", 0 }, "(#) show internal edge numbers", 0 },
......
...@@ -37,6 +37,7 @@ ...@@ -37,6 +37,7 @@
#include <cstring> #include <cstring>
#include <algorithm> #include <algorithm>
#include <ctype.h> #include <ctype.h>
#include <utility>
namespace spot namespace spot
...@@ -95,6 +96,8 @@ namespace spot ...@@ -95,6 +96,8 @@ namespace spot
bool opt_want_state_names_ = true; bool opt_want_state_names_ = true;
unsigned max_states_ = -1U; // related to max_states_given_ unsigned max_states_ = -1U; // related to max_states_given_
bool opt_shared_univ_dest_ = true;
public: public:
unsigned max_states() unsigned max_states()
...@@ -244,6 +247,9 @@ namespace spot ...@@ -244,6 +247,9 @@ namespace spot
case 't': case 't':
opt_force_acc_trans_ = true; opt_force_acc_trans_ = true;
break; break;
case 'y':
opt_shared_univ_dest_ = false;
break;
default: default:
throw std::runtime_error throw std::runtime_error
(std::string("unknown option for print_dot(): ") + c); (std::string("unknown option for print_dot(): ") + c);
...@@ -360,17 +366,24 @@ namespace spot ...@@ -360,17 +366,24 @@ namespace spot
return bdd_format_formula(aut_->get_dict(), label); return bdd_format_formula(aut_->get_dict(), label);
} }
std::set<int> done; std::set<std::pair<int, int>> done;
void void
print_dst(int dst, const char* style = nullptr) print_dst(int dst, const char* style = nullptr, int color_num = -1)
{ {
if (!done.emplace(dst).second) std::ostringstream tmp_dst;
tmp_dst << dst;
if (scc_num >= 0)
tmp_dst << '.' << scc_num;
if (!done.emplace(std::make_pair(dst, color_num)).second)
return; return;
os_ << " " << dst << " [label=<>,shape=point]\n"; else if (!opt_shared_univ_dest_ && color_num > 0)
tmp_dst << '.' << color_num;
std::string dest = tmp_dst.str();
os_ << " " << dest << " [label=<>,shape=point]\n";
for (unsigned d: aut_->univ_dests(dst)) for (unsigned d: aut_->univ_dests(dst))
{ {
os_ << " " << dst << " -> " << d; os_ << " " << dest << " -> " << d;
if (style && *style) if (style && *style)
os_ << " [" << style << ']'; os_ << " [" << style << ']';
os_ << '\n'; os_ << '\n';
...@@ -574,6 +587,13 @@ namespace spot ...@@ -574,6 +587,13 @@ namespace spot
process_link(const twa_graph::edge_storage_t& t, int number) process_link(const twa_graph::edge_storage_t& t, int number)
{ {
os_ << " " << t.src << " -> " << (int)t.dst; os_ << " " << t.src << " -> " << (int)t.dst;
if (aut_->is_univ_dest(t.dst) && highlight_edges_
&& !opt_shared_univ_dest_)
{
auto idx = aut_->get_graph().index_of_edge(t);
auto iter = highlight_edges_->find(idx);
os_ << '.' << iter->second % palette_mod;
}
std::string label; std::string label;
if (!opt_state_labels_) if (!opt_state_labels_)
label = bdd_format_formula(aut_->get_dict(), t.cond); label = bdd_format_formula(aut_->get_dict(), t.cond);
...@@ -616,6 +636,7 @@ namespace spot ...@@ -616,6 +636,7 @@ namespace spot
} }
std::string highlight; std::string highlight;
auto color_num = -1;
if (highlight_edges_) if (highlight_edges_)
{ {
auto idx = aut_->get_graph().index_of_edge(t); auto idx = aut_->get_graph().index_of_edge(t);
...@@ -628,13 +649,20 @@ namespace spot ...@@ -628,13 +649,20 @@ namespace spot
<< '"'; << '"';
highlight = o.str(); highlight = o.str();
os_ << ", " << highlight; os_ << ", " << highlight;
if (!opt_shared_univ_dest_)
color_num = iter->second % palette_mod;
} }
} }
if (aut_->is_univ_dest(t.dst)) if (aut_->is_univ_dest(t.dst))
os_ << ", arrowhead=onormal"; os_ << ", arrowhead=onormal";
os_ << "]\n"; os_ << "]\n";
if (aut_->is_univ_dest(t.dst)) if (aut_->is_univ_dest(t.dst))
print_dst(t.dst, highlight.c_str()); {
if (color_num >= 0)
print_dst(t.dst, highlight.c_str(), color_num);
else
print_dst(t.dst, highlight.c_str());
}
} }
void print(const const_twa_graph_ptr& aut) void print(const const_twa_graph_ptr& aut)
......
...@@ -353,6 +353,343 @@ State: 0 ...@@ -353,6 +353,343 @@ State: 0
EOF EOF
diff out5 expect diff out5 expect
# Test if split option is correct
cat >ex6<<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--
EOF
run 0 autfilt --dot='baryf(Lato)' ex6 > ex6.dot
cat >expect6.dot<<EOF
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>]
}
EOF
diff ex6.dot expect6.dot
cat >ex7<<EOF
HOA: v1
tool: "LTL3HOA"
name: "SLAA for c R (c | G(a & b) | (F!b & F!a))"
States: 5
AP: 3 "c" "a" "b"
Start: 0
Acceptance: 2 Fin(1) & Fin(0)
--BODY--
State: 0 "c R (c | G(a & b) | (F!b & F!a))"
[(0)] 4
[(!0 & !1 & !2)] 0
[(!0 & 1 & 2)] 0&1
[(!0 & 1 & !2)] 0&2
[(!0 & !1 & 2)] 0&3
[(!0 & 1 & 2)] 0&2&3
State: 1 "G(a & b)"
[(1 & 2)] 1
State: 2 "F!a"
[(!1)] 4
[(1)] 2 {1}
State: 3 "F!b"
[(!2)] 4
[(2)] 3 {0}
State: 4 "t"
[t] 4
--END--
EOF
run 0 autfilt --dot='sbarf(Lato)' ex7 > ex7.dot
color='<font color="#5DA5DA">⓿</font>'
cat >expect7.dot<<EOF
digraph G {
rankdir=LR
label=<Fin(<font color="#F17CB0"></font>) &amp; Fin($color)>
labelloc="t"
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
I [label="", style=invis, width=0]
I -> 0
subgraph cluster_0 {
color=green
label=""
4 [label="t"]
4 -> 4 [label=<1>]
}
subgraph cluster_1 {
color=green
label=""
1 [label="G(a & b)"]
1 -> 1 [label=<a &amp; b>]
}
subgraph cluster_2 {
color=red
label=""
2 [label="F!a"]
2 -> 4 [label=<!a>]
2 -> 2 [label=<a<br/><font color="#F17CB0"></font>>]
}
subgraph cluster_3 {
color=red
label=""
3 [label="F!b"]
3 -> 4 [label=<!b>]
3 -> 3 [label=<b<br/><font color="#5DA5DA"></font>>]
}
subgraph cluster_4 {
color=green
label=""
0 [label="c R (c | G(a & b) | (F!b & F!a))"]
0 -> 4 [label=<c>]
0 -> 0 [label=<!a &amp; !b &amp; !c>]
0 -> -1.4 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-1.4 [label=<>,shape=point]
-1.4 -> 0
-1.4 -> 1
0 -> -4.4 [label=<a &amp; !b &amp; !c>, arrowhead=onormal]
-4.4 [label=<>,shape=point]
-4.4 -> 0
-4.4 -> 2
0 -> -7.4 [label=<!a &amp; b &amp; !c>, arrowhead=onormal]
-7.4 [label=<>,shape=point]
-7.4 -> 0
-7.4 -> 3
0 -> -10.4 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-10.4 [label=<>,shape=point]
-10.4 -> 0
-10.4 -> 2
-10.4 -> 3
}
}
EOF
diff ex7.dot expect7.dot
cat >ex8<<EOF
HOA: v1
tool: "LTL3HOA"
name: "SLAA for c R (c | G(a & b) | (F!b & F!a))"
States: 5
AP: 3 "c" "a" "b"
Start: 0
Acceptance: 2 Fin(1) & Fin(0)
--BODY--
State: 0 "c R (c | G(a & b) | (F!b & F!a))"
[(0)] 4
[(!0 & !1 & !2)] 0
[(!0 & 1 & 2)] 0&1
[(!0 & 1 & !2)] 0&2
[(!0 & !1 & 2)] 0&3
State: 1 "G(a & b)"
[(1 & 2)] 1
[(!0 & 1 & 2)] 0&2&3
State: 2 "F!a"
[(!1)] 4
[(1)] 2 {1}
State: 3 "F!b"
[(!2)] 4
[(2)] 3 {0}
State: 4 "t"
[t] 4
--END--
EOF
run 0 autfilt --dot='sbarf(Lato)' ex8 > ex8.dot
cat >expect8.dot<<EOF
digraph G {
rankdir=LR
label=<Fin(<font color="#F17CB0"></font>) &amp; Fin($color)>
labelloc="t"
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
I [label="", style=invis, width=0]
I -> 0
subgraph cluster_0 {
color=green
label=""
4 [label="t"]
4 -> 4 [label=<1>]
}
subgraph cluster_1 {
color=red
label=""
2 [label="F!a"]
2 -> 4 [label=<!a>]
2 -> 2 [label=<a<br/><font color="#F17CB0"></font>>]
}
subgraph cluster_2 {
color=red
label=""
3 [label="F!b"]
3 -> 4 [label=<!b>]
3 -> 3 [label=<b<br/><font color="#5DA5DA"></font>>]
}
subgraph cluster_3 {
color=green
label=""
0 [label="c R (c | G(a & b) | (F!b & F!a))"]
0 -> 4 [label=<c>]
0 -> 0 [label=<!a &amp; !b &amp; !c>]
0 -> -1.3 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-1.3 [label=<>,shape=point]
-1.3 -> 0
-1.3 -> 1
0 -> -4.3 [label=<a &amp; !b &amp; !c>, arrowhead=onormal]
-4.3 [label=<>,shape=point]
-4.3 -> 0
-4.3 -> 2
0 -> -7.3 [label=<!a &amp; b &amp; !c>, arrowhead=onormal]
-7.3 [label=<>,shape=point]
-7.3 -> 0
-7.3 -> 3
1 [label="G(a & b)"]
1 -> 1 [label=<a &amp; b>]
1 -> -10.3 [label=<a &amp; b &amp; !c>, arrowhead=onormal]
-10.3 [label=<>,shape=point]
-10.3 -> 0
-10.3 -> 2
-10.3 -> 3
}
}
EOF
diff ex8.dot expect8.dot
cat >ex9 <<EOF
HOA: v1.1
States:3
Start: 0
AP: 3 "c" "b" "a"
Acceptance: 1 Fin(0)
spot.highlight.edges: 1 1 2 1 3 2
--BODY--
State: 0
[0&1] 1&2
State: 1
[1&2] 1&2
State: 2
[!0&!1&!2] 1&2
--END--
EOF
run 0 autfilt --dot='baryf(Lato)' ex9 > ex9.dot
cat >expect9.dot <<EOF
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 -> 0
0 [label=<0>]
0 -> -1.1 [label=<b &amp; c>, style=bold, color="#F17CB0", arrowhead=onormal]
-1.1 [label=<>,shape=point]
-1.1 -> 1 [style=bold, color="#F17CB0"]
-1.1 -> 2 [style=bold, color="#F17CB0"]
1 [label=<1>]
1 -> -1.1 [label=<a &amp; b>, style=bold, color="#F17CB0", arrowhead=onormal]
2 [label=<2>]
2 -> -1.2 [label=<!a &amp; !b &amp; !c>, style=bold, color="#FAA43A", $style]
-1.2 [label=<>,shape=point]
-1.2 -> 1 [style=bold, color="#FAA43A"]
-1.2 -> 2 [style=bold, color="#FAA43A"]
}
EOF
diff ex9.dot expect9.dot
cat >ex10 <<EOF
HOA: v1.1
States:3
Start: 0
AP: 3 "c" "b" "a"
Acceptance: 1 Fin(0)
spot.highlight.edges: 1 1 2 3 3 2
--BODY--
State: 0
[0&1] 1&2
State: 1
[1&2] 1&2
State: 2
[!0&!1&!2] 1&2
--END--
EOF
run 0 autfilt --dot='baryf(Lato)' ex10 > ex10.dot
cat >expect10.dot <<EOF
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 -> 0
0 [label=<0>]
0 -> -1.1 [label=<b &amp; c>, style=bold, color="#F17CB0", arrowhead=onormal]
-1.1 [label=<>,shape=point]
-1.1 -> 1 [style=bold, color="#F17CB0"]
-1.1 -> 2 [style=bold, color="#F17CB0"]
1 [label=<1>]
1 -> -1.3 [label=<a &amp; b>, style=bold, color="#B276B2", arrowhead=onormal]
-1.3 [label=<>,shape=point]
-1.3 -> 1 [style=bold, color="#B276B2"]
-1.3 -> 2 [style=bold, color="#B276B2"]
2 [label=<2>]
2 -> -1.2 [label=<!a &amp; !b &amp; !c>, style=bold, color="#FAA43A", $style]
-1.2 [label=<>,shape=point]
-1.2 -> 1 [style=bold, color="#FAA43A"]
-1.2 -> 2 [style=bold, color="#FAA43A"]
}
EOF
diff ex10.dot expect10.dot
# Detect cases where alternation-removal cannot work. # Detect cases where alternation-removal cannot work.
cat >in <<EOF cat >in <<EOF
HOA: v1 HOA: v1
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment