Commit f7bbfd28 authored by Arthur Remaud's avatar Arthur Remaud Committed by Arthur Remaud

autfilt: Better display of cluster when universal edge loops in it

Fixes #208

* NEWS: Informations about the modifications
* spot/twaalgos/dot.cc (print): Gestion of cluster for
universal transitions
* tests/core/alternating.test: tests added
* tests/core/neverclaimread.test: tests changed for
new dot format
* tests/core/readsave.test: tests changed
* tests/core/sccdot.test: tests changed
* tests/python/_altscc.ipynb: tests changed
* tests/python/decompose.ipynb: tests changed
parent 34859568
...@@ -41,6 +41,10 @@ New in spot 2.3.0.dev (not yet released) ...@@ -41,6 +41,10 @@ New in spot 2.3.0.dev (not yet released)
caused any user-defined CPPFLAGS to be ignored while building caused any user-defined CPPFLAGS to be ignored while building
Spot. Spot.
- The display of clusters with universal edges was confused, because the
intermediate node was not in the cluster even if one of the target was
in the same one.
New in spot 2.3 (2017-01-19) New in spot 2.3 (2017-01-19)
Build: Build:
......
...@@ -369,7 +369,8 @@ namespace spot ...@@ -369,7 +369,8 @@ namespace spot
std::set<std::pair<int, int>> done; std::set<std::pair<int, int>> done;
void void
print_dst(int dst, const char* style = nullptr, int color_num = -1) print_dst(int dst, const char* style = nullptr, int scc_num = -1,
int color_num = -1)
{ {
std::ostringstream tmp_dst; std::ostringstream tmp_dst;
tmp_dst << dst; tmp_dst << dst;
...@@ -584,9 +585,14 @@ namespace spot ...@@ -584,9 +585,14 @@ namespace spot
} }
void void
process_link(const twa_graph::edge_storage_t& t, int number) process_link(const twa_graph::edge_storage_t& t, int number,
int scc_num = -1)
{ {
os_ << " " << t.src << " -> " << (int)t.dst; os_ << " " << t.src << " -> " << (int)t.dst;
if (scc_num >= 0)
{
os_ << '.' << scc_num;
}
if (aut_->is_univ_dest(t.dst) && highlight_edges_ if (aut_->is_univ_dest(t.dst) && highlight_edges_
&& !opt_shared_univ_dest_) && !opt_shared_univ_dest_)
{ {
...@@ -659,9 +665,9 @@ namespace spot ...@@ -659,9 +665,9 @@ namespace spot
if (aut_->is_univ_dest(t.dst)) if (aut_->is_univ_dest(t.dst))
{ {
if (color_num >= 0) if (color_num >= 0)
print_dst(t.dst, highlight.c_str(), color_num); print_dst(t.dst, highlight.c_str(), scc_num, color_num);
else else
print_dst(t.dst, highlight.c_str()); print_dst(t.dst, highlight.c_str(), scc_num);
} }
} }
...@@ -764,7 +770,29 @@ namespace spot ...@@ -764,7 +770,29 @@ namespace spot
os_ << " label=\"\"\n"; os_ << " label=\"\"\n";
} }
for (auto s: si->states_of(i)) for (auto s: si->states_of(i))
process_state(s); {
process_state(s);
int trans_num = 0;
for (auto& t : aut_->out(s))
{
if (aut_->is_univ_dest(t.dst))
{
bool to_write = false;
for (unsigned d: aut_->univ_dests(t.dst))
{
to_write = si->scc_of(d) == si->scc_of(s);
if (to_write)
break;
}
if (to_write)
process_link(t, trans_num++, i);
else
process_link(t, trans_num++);
}
else
process_link(t, trans_num++);
}
}
os_ << " }\n"; os_ << " }\n";
} }
} }
...@@ -772,10 +800,12 @@ namespace spot ...@@ -772,10 +800,12 @@ namespace spot
for (unsigned n = 0; n < ns; ++n) for (unsigned n = 0; n < ns; ++n)
{ {
if (!si || !si->reachable_state(n)) if (!si || !si->reachable_state(n))
process_state(n); {
int trans_num = 0; process_state(n);
for (auto& t: aut_->out(n)) int trans_num = 0;
process_link(t, trans_num++); for (auto& t: aut_->out(n))
process_link(t, trans_num++);
}
} }
end(); end();
} }
......
...@@ -69,37 +69,49 @@ digraph G { ...@@ -69,37 +69,49 @@ digraph G {
color=green color=green
label="" label=""
2 [label="G(a)"] 2 [label="G(a)"]
2 -> 2 [label="a"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=red color=red
label="" label=""
1 [label="FG(a)\n⓿"] 1 [label="FG(a)\n⓿"]
1 -> 2 [label="a"]
1 -> 1 [label="1"]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=green color=green
label="" label=""
6 [label="t"] 6 [label="t"]
6 -> 6 [label="1"]
} }
subgraph cluster_3 { subgraph cluster_3 {
color=red color=red
label="" label=""
4 [label="F(b)\n⓿"] 4 [label="F(b)\n⓿"]
4 -> 6 [label="b"]
4 -> 4 [label="!b"]
} }
subgraph cluster_4 { subgraph cluster_4 {
color=green color=green
label="" label=""
3 [label="GF(b)"] 3 [label="GF(b)"]
3 -> 3 [label="b"]
3 -> -8.4 [label="!b", style=bold, color="#FAA43A", arrowhead=onormal]
-8.4 [label=<>,shape=point]
-8.4 -> 3 [style=bold, color="#FAA43A"]
-8.4 -> 4 [style=bold, color="#FAA43A"]
} }
subgraph cluster_5 { subgraph cluster_5 {
color=red color=red
label="" label=""
5 [label="((a) U (b))\n⓿"] 5 [label="((a) U (b))\n⓿"]
5 -> 6 [label="b"]
5 -> 5 [label="a & !b"]
} }
subgraph cluster_6 { subgraph cluster_6 {
color=black color=black
label="" label=""
0 [label="((((a) U (b)) && GF(b)) && FG(a))"] 0 [label="((((a) U (b)) && GF(b)) && FG(a))"]
}
0 -> -1 [label="b", arrowhead=onormal] 0 -> -1 [label="b", arrowhead=onormal]
-1 [label=<>,shape=point] -1 [label=<>,shape=point]
-1 -> 1 -1 -> 1
...@@ -109,19 +121,7 @@ digraph G { ...@@ -109,19 +121,7 @@ digraph G {
-4 -> 1 [style=bold, color="#F15854"] -4 -> 1 [style=bold, color="#F15854"]
-4 -> 3 [style=bold, color="#F15854"] -4 -> 3 [style=bold, color="#F15854"]
-4 -> 5 [style=bold, color="#F15854"] -4 -> 5 [style=bold, color="#F15854"]
1 -> 2 [label="a"] }
1 -> 1 [label="1"]
2 -> 2 [label="a"]
3 -> 3 [label="b"]
3 -> -8 [label="!b", style=bold, color="#FAA43A", arrowhead=onormal]
-8 [label=<>,shape=point]
-8 -> 3 [style=bold, color="#FAA43A"]
-8 -> 4 [style=bold, color="#FAA43A"]
4 -> 6 [label="b"]
4 -> 4 [label="!b"]
5 -> 6 [label="b"]
5 -> 5 [label="a & !b"]
6 -> 6 [label="1"]
} }
EOF EOF
...@@ -353,7 +353,7 @@ State: 0 ...@@ -353,7 +353,7 @@ State: 0
EOF EOF
diff out5 expect diff out5 expect
# Test if split option is correct # Test if split option with color is correct
cat >ex6<<EOF cat >ex6<<EOF
HOA: v1.1 HOA: v1.1
States: 2 States: 2
...@@ -373,6 +373,7 @@ EOF ...@@ -373,6 +373,7 @@ EOF
run 0 autfilt --dot='baryf(Lato)' ex6 > ex6.dot run 0 autfilt --dot='baryf(Lato)' ex6 > ex6.dot
style='arrowhead=onormal'
cat >expect6.dot<<EOF cat >expect6.dot<<EOF
digraph G { digraph G {
rankdir=LR rankdir=LR
...@@ -389,11 +390,11 @@ digraph G { ...@@ -389,11 +390,11 @@ digraph G {
-1 -> 1 -1 -> 1
0 [label=<0>] 0 [label=<0>]
0 -> 0 [label=<!a &amp; !c>] 0 -> 0 [label=<!a &amp; !c>]
0 -> -1.1 [label=<a &amp; b &amp; !c>, style=bold, color="#F17CB0", arrowhead=onormal] 0 -> -1.1 [label=<a &amp; b &amp; !c>, style=bold, color="#F17CB0", $style]
-1.1 [label=<>,shape=point] -1.1 [label=<>,shape=point]
-1.1 -> 0 [style=bold, color="#F17CB0"] -1.1 -> 0 [style=bold, color="#F17CB0"]
-1.1 -> 1 [style=bold, color="#F17CB0"] -1.1 -> 1 [style=bold, color="#F17CB0"]
0 -> -1.2 [label=<a &amp; !c>, style=bold, color="#FAA43A", arrowhead=onormal] 0 -> -1.2 [label=<a &amp; !c>, style=bold, color="#FAA43A", $style]
-1.2 [label=<>,shape=point] -1.2 [label=<>,shape=point]
-1.2 -> 0 [style=bold, color="#FAA43A"] -1.2 -> 0 [style=bold, color="#FAA43A"]
-1.2 -> 1 [style=bold, color="#FAA43A"] -1.2 -> 1 [style=bold, color="#FAA43A"]
...@@ -690,6 +691,79 @@ EOF ...@@ -690,6 +691,79 @@ EOF
diff ex10.dot expect10.dot diff ex10.dot expect10.dot
cat >ex11 <<EOF
HOA: v1
tool: "LTL3HOA"
name: "SLAA for G((b & Fa) | (!b & G!a))"
States: 4
AP: 2 "b" "a"
Start: 0
Acceptance: 1 Fin(0)
--BODY--
State: 0 "G((b & Fa) | (!b & G!a))"
[(0 & 1)] 0
[(0 & !1)] 0&1
[(!0 & !1)] 0&2
State: 1 "Fa"
[(1)] 3
[(!1)] 1 {1}
State: 2 "G!a"
[(!1)] 2
State: 3 "t"
[t] 3
--END--
EOF
run 2 autfilt --dot='sbarf(Lato)' ex11 > ex11.dot
cat >expect11.dot <<EOF
digraph G {
rankdir=LR
label=<Fin(<font color="#5DA5DA"></font>)>
labelloc="t"
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
I [label="", style=invis, width=0]
I -> 0
subgraph cluster_0 {
color=green
label=""
3 [label="t"]
3 -> 3 [label=<1>]
}
subgraph cluster_1 {
color=green
label=""
1 [label="Fa"]
1 -> 3 [label=<a>]
1 -> 1 [label=<!a>]
}
subgraph cluster_2 {
color=green
label=""
2 [label="G!a"]
2 -> 2 [label=<!a>]
}
subgraph cluster_3 {
color=green
label=""
0 [label="G((b & Fa) | (!b & G!a))"]
0 -> 0 [label=<a &amp; b>]
0 -> -1.3 [label=<!a &amp; b>, arrowhead=onormal]
-1.3 [label=<>,shape=point]
-1.3 -> 0
-1.3 -> 1
0 -> -4.3 [label=<!a &amp; !b>, arrowhead=onormal]
-4.3 [label=<>,shape=point]
-4.3 -> 0
-4.3 -> 2
}
}
EOF
diff ex11.dot expect11.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
......
...@@ -336,15 +336,15 @@ digraph G { ...@@ -336,15 +336,15 @@ digraph G {
color=green color=green
label="" label=""
1 [label="1", peripheries=2] 1 [label="1", peripheries=2]
1 -> 1 [label="1"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=red color=red
label="" label=""
0 [label="0"] 0 [label="0"]
}
0 -> 1 [label="b"] 0 -> 1 [label="b"]
0 -> 0 [label="0"] 0 -> 0 [label="0"]
1 -> 1 [label="1"] }
} }
EOF EOF
diff stdout expected diff stdout expected
......
...@@ -327,21 +327,21 @@ digraph G { ...@@ -327,21 +327,21 @@ digraph G {
subgraph cluster_0 { subgraph cluster_0 {
color=green color=green
1 [label="s1", peripheries=2] 1 [label="s1", peripheries=2]
1 -> 1 [label="a"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=green color=green
0 [label="s0", peripheries=2] 0 [label="s0", peripheries=2]
0 -> 0 [label="b"]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=black color=black
3 [label="s3"] 3 [label="s3"]
3 -> 1 [label="a"]
3 -> 0 [label="b"]
} }
0 -> 0 [label="b"]
1 -> 1 [label="a"]
2 [label="s2"] 2 [label="s2"]
2 -> 0 [label="b"] 2 -> 0 [label="b"]
3 -> 1 [label="a"]
3 -> 0 [label="b"]
} }
EOF EOF
......
...@@ -83,67 +83,67 @@ digraph G { ...@@ -83,67 +83,67 @@ digraph G {
color=grey color=grey
label="" label=""
5 [label="5"] 5 [label="5"]
5 -> 6 [label="1"]
6 [label="6"] 6 [label="6"]
6 -> 5 [label="1"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=grey color=grey
label="" label=""
0 [label="0"] 0 [label="0"]
0 -> 0 [label="a & b\n{0,1,2}"]
0 -> 0 [label="!a & !b\n{2}"]
0 -> 5 [label="a\n{2}"]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=green color=green
label="" label=""
9 [label="9"] 9 [label="9"]
9 -> 9 [label="!a & b\n{0,2}"]
9 -> 10 [label="a & b\n{0,1}"]
10 [label="10"] 10 [label="10"]
10 -> 9 [label="!a & b\n{0,1}"]
10 -> 10 [label="a & b\n{0,2}"]
} }
subgraph cluster_3 { subgraph cluster_3 {
color=green color=green
label="" label=""
8 [label="8"] 8 [label="8"]
8 -> 8 [label="!a & b\n{0,2}"]
8 -> 8 [label="a & b\n{0,1}"]
8 -> 9 [label="1"]
} }
subgraph cluster_4 { subgraph cluster_4 {
color=green color=green
label="" label=""
7 [label="7"] 7 [label="7"]
7 -> 7 [label="!a & b\n{0,1}"]
7 -> 7 [label="a & b\n{0,2}"]
7 -> 8 [label="1"]
} }
subgraph cluster_5 { subgraph cluster_5 {
color=black color=black
label="" label=""
2 [label="2"] 2 [label="2"]
2 -> 0 [label="a"]
2 -> 7 [label="b"]
} }
subgraph cluster_6 { subgraph cluster_6 {
color=red color=red
label="" label=""
4 [label="4"] 4 [label="4"]
4 -> 4 [label="!b\n{1,2}"]
4 -> 2 [label="b"]
} }
subgraph cluster_7 { subgraph cluster_7 {
color=green color=green
label="" label=""
1 [label="1"] 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 -> 4 [label="b"]
1 -> 3 [label="a & !b"] 1 -> 3 [label="a & !b"]
2 -> 0 [label="a"] 3 [label="3"]
2 -> 7 [label="b"]
3 -> 1 [label="a & b\n{0,1}"] 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}"]
} }
EOF EOF
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
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