Commit 1cc45b24 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

dot: display acceptance names

* spot/twaalgos/dot.cc: Display common acceptance names.
* NEWS: Mention the change.
* doc/org/oaut.org: Adjust text.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.
parent f8ef06ac
...@@ -59,6 +59,9 @@ New in spot 2.3.5.dev (not yet released) ...@@ -59,6 +59,9 @@ New in spot 2.3.5.dev (not yet released)
the Python bindings can be found at the Python bindings can be found at
https://spot.lrde.epita.fr/ipynb/decompose.html https://spot.lrde.epita.fr/ipynb/decompose.html
- The print_dot() function will now display names for well known
acceptance conditions under the formula when option 'a' is used.
- A new named property for automata called "original-states" can be - A new named property for automata called "original-states" can be
used to record the origin of a state before transformation. It is used to record the origin of a state before transformation. It is
currently defined by the degeneralization algorithms, and by currently defined by the degeneralization algorithms, and by
......
...@@ -610,21 +610,21 @@ ltl2tgba --dot=vcsna '(Ga -> Gb) W c' ...@@ -610,21 +610,21 @@ ltl2tgba --dot=vcsna '(Ga -> Gb) W c'
#+RESULTS: #+RESULTS:
#+begin_example #+begin_example
digraph G { digraph G {
label="(Gb | F!a) W c\nInf(0)" label="(Gb | F!a) W c\nInf(0)\n[Büchi]"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
node[style=filled, fillcolor="#ffffa0"] edge[arrowhead=vee, arrowsize=.7]
I [label="", style=invis, height=0] I [label="", style=invis, height=0]
I -> 1 I -> 0
subgraph cluster_0 { subgraph cluster_0 {
color=green color=green
label="" label=""
0 [label="0"] 1 [label="1"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=green color=green
label="" label=""
3 [label="3"] 2 [label="2"]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=red color=red
...@@ -634,20 +634,20 @@ digraph G { ...@@ -634,20 +634,20 @@ digraph G {
subgraph cluster_3 { subgraph cluster_3 {
color=green color=green
label="" label=""
1 [label="1"] 0 [label="0"]
2 [label="2"] 3 [label="3"]
} }
0 -> 0 [label="b\n{0}"] 0 -> 0 [label="!a & !c\n{0}"]
1 -> 0 [label="a & b & !c"] 0 -> 1 [label="c"]
1 -> 1 [label="!a & !c\n{0}"] 0 -> 2 [label="a & b & !c"]
1 -> 2 [label="a & !c"] 0 -> 3 [label="a & !c"]
1 -> 3 [label="c"] 1 -> 1 [label="1\n{0}"]
2 -> 1 [label="!a & !c\n{0}"] 2 -> 2 [label="b\n{0}"]
2 -> 2 [label="a & !c"] 3 -> 0 [label="!a & !c\n{0}"]
2 -> 3 [label="!a & c"] 3 -> 1 [label="!a & c"]
2 -> 4 [label="a & c"] 3 -> 3 [label="a & !c"]
3 -> 3 [label="1\n{0}"] 3 -> 4 [label="a & c"]
4 -> 3 [label="!a"] 4 -> 1 [label="!a"]
4 -> 4 [label="a"] 4 -> 4 [label="a"]
} }
#+end_example #+end_example
...@@ -660,20 +660,20 @@ SPOT_DOTEXTRA= ltl2tgba --dot=vcsna '(Ga -> Gb) W c' ...@@ -660,20 +660,20 @@ SPOT_DOTEXTRA= ltl2tgba --dot=vcsna '(Ga -> Gb) W c'
#+RESULTS: oaut-dot2 #+RESULTS: oaut-dot2
#+begin_example #+begin_example
digraph G { digraph G {
label="(Gb | F!a) W c\nInf(0)" label="(Gb | F!a) W c\nInf(0)\n[Büchi]"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, height=0] I [label="", style=invis, height=0]
I -> 1 I -> 0
subgraph cluster_0 { subgraph cluster_0 {
color=green color=green
label="" label=""
0 [label="0"] 1 [label="1"]
} }
subgraph cluster_1 { subgraph cluster_1 {
color=green color=green
label="" label=""
3 [label="3"] 2 [label="2"]
} }
subgraph cluster_2 { subgraph cluster_2 {
color=red color=red
...@@ -683,20 +683,20 @@ digraph G { ...@@ -683,20 +683,20 @@ digraph G {
subgraph cluster_3 { subgraph cluster_3 {
color=green color=green
label="" label=""
1 [label="1"] 0 [label="0"]
2 [label="2"] 3 [label="3"]
} }
0 -> 0 [label="b\n{0}"] 0 -> 0 [label="!a & !c\n{0}"]
1 -> 0 [label="a & b & !c"] 0 -> 1 [label="c"]
1 -> 1 [label="!a & !c\n{0}"] 0 -> 2 [label="a & b & !c"]
1 -> 2 [label="a & !c"] 0 -> 3 [label="a & !c"]
1 -> 3 [label="c"] 1 -> 1 [label="1\n{0}"]
2 -> 1 [label="!a & !c\n{0}"] 2 -> 2 [label="b\n{0}"]
2 -> 2 [label="a & !c"] 3 -> 0 [label="!a & !c\n{0}"]
2 -> 3 [label="!a & c"] 3 -> 1 [label="!a & c"]
2 -> 4 [label="a & c"] 3 -> 3 [label="a & !c"]
3 -> 3 [label="1\n{0}"] 3 -> 4 [label="a & c"]
4 -> 3 [label="!a"] 4 -> 1 [label="!a"]
4 -> 4 [label="a"] 4 -> 4 [label="a"]
} }
#+end_example #+end_example
...@@ -710,7 +710,9 @@ $txt ...@@ -710,7 +710,9 @@ $txt
The acceptance condition is displayed in the same way as in the [[http://adl.github.io/hoaf/][HOA The acceptance condition is displayed in the same way as in the [[http://adl.github.io/hoaf/][HOA
format]]. Here =Inf(0)= means that runs are accepting if and only if format]]. Here =Inf(0)= means that runs are accepting if and only if
they visit some the transitions in the set #0 infinitely often. they visit some the transitions in the set #0 infinitely often. For
well known acceptance conditions (as Büchi in this case), their name
is also displayed in bracket below.
The strongly connected components are displayed using the following colors: The strongly connected components are displayed using the following colors:
- *green* components contain an accepting cycle - *green* components contain an accepting cycle
......
...@@ -88,6 +88,7 @@ namespace spot ...@@ -88,6 +88,7 @@ namespace spot
bool opt_name_ = false; bool opt_name_ = false;
bool opt_show_acc_ = false; bool opt_show_acc_ = false;
bool mark_states_ = false; bool mark_states_ = false;
bool dcircles_ = false;
bool opt_scc_ = false; bool opt_scc_ = false;
bool opt_html_labels_ = false; bool opt_html_labels_ = false;
bool opt_state_labels_ = false; bool opt_state_labels_ = false;
...@@ -416,6 +417,65 @@ namespace spot ...@@ -416,6 +417,65 @@ namespace spot
} }
} }
void print_acceptance_for_human()
{
const char* nl = opt_html_labels_ ? "<br/>" : "\\n";
if (aut_->acc().is_generalized_buchi())
{
if (aut_->acc().is_all())
os_ << nl << "[all]";
else if (aut_->acc().is_buchi())
os_ << nl << "[Büchi]";
else
os_ << nl << "[gen. Büchi " << aut_->num_sets() << ']';
}
else if (aut_->acc().is_generalized_co_buchi())
{
if (aut_->acc().is_none())
os_ << nl << "[none]";
else if (aut_->acc().is_co_buchi())
os_ << nl << "[co-Büchi]";
else
os_ << nl << "[gen. co-Büchi " << aut_->num_sets() << ']';
}
else
{
int r = aut_->acc().is_rabin();
assert(r != 0);
if (r > 0)
{
os_ << nl << "[Rabin " << r << ']';
}
else
{
r = aut_->acc().is_streett();
assert(r != 0);
if (r > 0)
{
os_ << nl << "[Streett " << r << ']';
}
else
{
std::vector<unsigned> pairs;
if (aut_->acc().is_generalized_rabin(pairs))
{
os_ << nl << "[gen. Rabin " << pairs.size() << ']';
}
else
{
bool max = false;
bool odd = false;
if (aut_->acc().is_parity(max, odd))
os_ << nl << "[parity "
<< (max ? "max " : "min ")
<< (odd ? "odd " : "even ")
<< aut_->num_sets() << ']';
}
}
}
}
}
void void
start() start()
{ {
...@@ -439,11 +499,17 @@ namespace spot ...@@ -439,11 +499,17 @@ namespace spot
os_ << "\\n"; os_ << "\\n";
} }
if (opt_show_acc_) if (opt_show_acc_)
aut_->get_acceptance().to_text {
(os_, [this](std::ostream& os, int v) if (!dcircles_)
{ {
this->output_set(os, v); aut_->get_acceptance().to_text
}); (os_, [this](std::ostream& os, int v)
{
this->output_set(os, v);
});
}
print_acceptance_for_human();
}
os_ << "\"\n"; os_ << "\"\n";
} }
else else
...@@ -456,11 +522,17 @@ namespace spot ...@@ -456,11 +522,17 @@ namespace spot
os_ << "<br/>"; os_ << "<br/>";
} }
if (opt_show_acc_) if (opt_show_acc_)
aut_->get_acceptance().to_html {
(os_, [this](std::ostream& os, int v) if (!dcircles_)
{ {
this->output_html_set_aux(os, v); aut_->get_acceptance().to_html
}); (os_, [this](std::ostream& os, int v)
{
this->output_html_set_aux(os, v);
});
}
print_acceptance_for_human();
}
os_ << ">\n"; os_ << ">\n";
} }
os_ << " labelloc=\"t\"\n"; os_ << " labelloc=\"t\"\n";
...@@ -517,9 +589,7 @@ namespace spot ...@@ -517,9 +589,7 @@ namespace spot
void void
process_state(unsigned s) process_state(unsigned s)
{ {
if (mark_states_ && if (mark_states_ && !dcircles_)
((opt_bullet && !opt_bullet_but_buchi)
|| aut_->num_sets() != 1))
{ {
acc_cond::mark_t acc = 0U; acc_cond::mark_t acc = 0U;
for (auto& t: aut_->out(s)) for (auto& t: aut_->out(s))
...@@ -589,7 +659,7 @@ namespace spot ...@@ -589,7 +659,7 @@ namespace spot
// Use state_acc_sets(), not state_is_accepting() because // Use state_acc_sets(), not state_is_accepting() because
// on co-Büchi automata we want to mark the rejecting // on co-Büchi automata we want to mark the rejecting
// states. // states.
if (mark_states_ && aut_->state_acc_sets(s)) if (dcircles_ && aut_->state_acc_sets(s))
os_ << ", peripheries=2"; os_ << ", peripheries=2";
} }
if (highlight_states_) if (highlight_states_)
...@@ -745,6 +815,9 @@ namespace spot ...@@ -745,6 +815,9 @@ namespace spot
name_ = aut_->get_named_prop<std::string>("automaton-name"); name_ = aut_->get_named_prop<std::string>("automaton-name");
mark_states_ = (!opt_force_acc_trans_ mark_states_ = (!opt_force_acc_trans_
&& aut_->prop_state_acc().is_true()); && aut_->prop_state_acc().is_true());
dcircles_ = (mark_states_
&& (!opt_bullet || opt_bullet_but_buchi)
&& (aut_->acc().is_buchi() || aut_->acc().is_co_buchi()));
if (opt_shape_ == ShapeAuto) if (opt_shape_ == ShapeAuto)
{ {
if (sn_ || sprod_ || aut->num_states() > 100 if (sn_ || sprod_ || aut->num_states() > 100
......
...@@ -58,7 +58,7 @@ autfilt --dot=bans alt.hoa >alt.dot ...@@ -58,7 +58,7 @@ autfilt --dot=bans alt.hoa >alt.dot
cat >expect.dot <<EOF cat >expect.dot <<EOF
digraph G { digraph G {
rankdir=LR rankdir=LR
label="Fin(⓿)" label="Fin(⓿)\n[co-Büchi]"
labelloc="t" labelloc="t"
I [label="", style=invis, width=0] I [label="", style=invis, width=0]
I -> -11 [arrowhead=onormal] I -> -11 [arrowhead=onormal]
...@@ -500,937 +500,7 @@ style='arrowhead=onormal' ...@@ -500,937 +500,7 @@ style='arrowhead=onormal'
cat >expect6.dot<<EOF cat >expect6.dot<<EOF
digraph G { digraph G {
rankdir=LR rankdir=LR
label=<Fin(<font color="# label=<Fin(<font color="#1F78B4"></font>)<br/>[co-Büchi]>
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
--BODY--
State: 0
[t] 1 {0}
State: 1
[t] 1
[0] 1 {0}
--END--
EOF
diff expected res
cat >ex1<<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic univ-branch
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
EOF
cat >ex2<<EOF
HOA: v1
States: 3
Start: 0&1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic univ-branch
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
EOF
cat >ex3<<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic univ-branch
--BODY--
State: 0
[0] 1
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
EOF
autfilt -q --equivalent-to=ex1 ex2
autfilt -q --included-in=ex1 ex2
autfilt -q --equivalent-to=ex1 ex3 && exit 1
autfilt -q --intersect=ex1 ex3
cat >ex4<<EOF
HOA: v1
States: 5
Start: 0&2
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc deterministic
properties: univ-branch
--BODY--
State: 0
[0] 0
[!0] 0&2
State: 1
[t] 1&4
State: 2
[!0] 2 {0}
[0] 3
State: 3
[t] 3
State: 4
--END--
HOA: v1
States: 5
Start: 0&2&4
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc deterministic
properties: univ-branch
--BODY--
State: 0
[0] 0
[!0] 0&2
State: 1
[t] 1&4
State: 2
[!0] 2 {0}
[0] 3
State: 3
[t] 3
State: 4
--END--
EOF
cat >expect4<<EOF
HOA: v1
States: 3
Start: 0&1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic univ-branch
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
HOA: v1
States: 4
Start: 0&1&3
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc deterministic
properties: univ-branch
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
State: 3
--END--
EOF
cat >expect4d<<EOF
HOA: v1
States: 3
Start: 0&1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic univ-branch
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant weak
--BODY--
State: 0
--END--
EOF
run 0 autfilt --remove-unreachable-states ex4 > out4
diff expect4 out4
run 0 autfilt --remove-dead-states ex4 > out4
diff expect4d out4
cat >ex5<<EOF
HOA: v1
States: 2
Start: 0&1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
--BODY--
State: 0
State: 1
--END--
HOA: v1
States: 3
Start: 0
AP: 1 "a"
Acceptance: 0 t
--BODY--
State: 0
[0] 1&2
[!0] 1
State: 1
[!0] 1
State: 2
--END--
HOA: v1
States: 4
Start: 0&1
AP: 1 "a"
Acceptance: 0 t
--BODY--
State: 0
[0] 1&2
State: 1
[!0] 1&0&3
State: 2
State: 3
[t] 3
--END--
EOF
run 0 autfilt --remove-dead-states ex5 > out5
cat >expect <<EOF
HOA: v1
States: 1
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: trans-labels explicit-labels state-acc deterministic
properties: stutter-invariant weak
--BODY--
State: 0
--END--
HOA: v1
States: 2
Start: 0