diff --git a/NEWS b/NEWS
index 80e1e9578..cf21d5273 100644
--- a/NEWS
+++ b/NEWS
@@ -59,6 +59,9 @@ New in spot 2.3.5.dev (not yet released)
the Python bindings can be found at
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
used to record the origin of a state before transformation. It is
currently defined by the degeneralization algorithms, and by
diff --git a/doc/org/oaut.org b/doc/org/oaut.org
index 95fe045e0..539f596e4 100644
--- a/doc/org/oaut.org
+++ b/doc/org/oaut.org
@@ -610,21 +610,21 @@ ltl2tgba --dot=vcsna '(Ga -> Gb) W c'
#+RESULTS:
#+begin_example
digraph G {
- label="(Gb | F!a) W c\nInf(0)"
+ label="(Gb | F!a) W c\nInf(0)\n[Büchi]"
labelloc="t"
node [shape="circle"]
- node[style=filled, fillcolor="#ffffa0"]
+ edge[arrowhead=vee, arrowsize=.7]
I [label="", style=invis, height=0]
- I -> 1
+ I -> 0
subgraph cluster_0 {
color=green
label=""
- 0 [label="0"]
+ 1 [label="1"]
}
subgraph cluster_1 {
color=green
label=""
- 3 [label="3"]
+ 2 [label="2"]
}
subgraph cluster_2 {
color=red
@@ -634,20 +634,20 @@ digraph G {
subgraph cluster_3 {
color=green
label=""
- 1 [label="1"]
- 2 [label="2"]
+ 0 [label="0"]
+ 3 [label="3"]
}
- 0 -> 0 [label="b\n{0}"]
- 1 -> 0 [label="a & b & !c"]
- 1 -> 1 [label="!a & !c\n{0}"]
- 1 -> 2 [label="a & !c"]
- 1 -> 3 [label="c"]
- 2 -> 1 [label="!a & !c\n{0}"]
- 2 -> 2 [label="a & !c"]
- 2 -> 3 [label="!a & c"]
- 2 -> 4 [label="a & c"]
- 3 -> 3 [label="1\n{0}"]
- 4 -> 3 [label="!a"]
+ 0 -> 0 [label="!a & !c\n{0}"]
+ 0 -> 1 [label="c"]
+ 0 -> 2 [label="a & b & !c"]
+ 0 -> 3 [label="a & !c"]
+ 1 -> 1 [label="1\n{0}"]
+ 2 -> 2 [label="b\n{0}"]
+ 3 -> 0 [label="!a & !c\n{0}"]
+ 3 -> 1 [label="!a & c"]
+ 3 -> 3 [label="a & !c"]
+ 3 -> 4 [label="a & c"]
+ 4 -> 1 [label="!a"]
4 -> 4 [label="a"]
}
#+end_example
@@ -660,20 +660,20 @@ SPOT_DOTEXTRA= ltl2tgba --dot=vcsna '(Ga -> Gb) W c'
#+RESULTS: oaut-dot2
#+begin_example
digraph G {
- label="(Gb | F!a) W c\nInf(0)"
+ label="(Gb | F!a) W c\nInf(0)\n[Büchi]"
labelloc="t"
node [shape="circle"]
I [label="", style=invis, height=0]
- I -> 1
+ I -> 0
subgraph cluster_0 {
color=green
label=""
- 0 [label="0"]
+ 1 [label="1"]
}
subgraph cluster_1 {
color=green
label=""
- 3 [label="3"]
+ 2 [label="2"]
}
subgraph cluster_2 {
color=red
@@ -683,20 +683,20 @@ digraph G {
subgraph cluster_3 {
color=green
label=""
- 1 [label="1"]
- 2 [label="2"]
+ 0 [label="0"]
+ 3 [label="3"]
}
- 0 -> 0 [label="b\n{0}"]
- 1 -> 0 [label="a & b & !c"]
- 1 -> 1 [label="!a & !c\n{0}"]
- 1 -> 2 [label="a & !c"]
- 1 -> 3 [label="c"]
- 2 -> 1 [label="!a & !c\n{0}"]
- 2 -> 2 [label="a & !c"]
- 2 -> 3 [label="!a & c"]
- 2 -> 4 [label="a & c"]
- 3 -> 3 [label="1\n{0}"]
- 4 -> 3 [label="!a"]
+ 0 -> 0 [label="!a & !c\n{0}"]
+ 0 -> 1 [label="c"]
+ 0 -> 2 [label="a & b & !c"]
+ 0 -> 3 [label="a & !c"]
+ 1 -> 1 [label="1\n{0}"]
+ 2 -> 2 [label="b\n{0}"]
+ 3 -> 0 [label="!a & !c\n{0}"]
+ 3 -> 1 [label="!a & c"]
+ 3 -> 3 [label="a & !c"]
+ 3 -> 4 [label="a & c"]
+ 4 -> 1 [label="!a"]
4 -> 4 [label="a"]
}
#+end_example
@@ -710,7 +710,9 @@ $txt
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
-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:
- *green* components contain an accepting cycle
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index fd0c1e4f4..32e581e11 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -88,6 +88,7 @@ namespace spot
bool opt_name_ = false;
bool opt_show_acc_ = false;
bool mark_states_ = false;
+ bool dcircles_ = false;
bool opt_scc_ = false;
bool opt_html_labels_ = false;
bool opt_state_labels_ = false;
@@ -416,6 +417,65 @@ namespace spot
}
}
+ void print_acceptance_for_human()
+ {
+ const char* nl = opt_html_labels_ ? "
" : "\\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 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
start()
{
@@ -439,11 +499,17 @@ namespace spot
os_ << "\\n";
}
if (opt_show_acc_)
- aut_->get_acceptance().to_text
- (os_, [this](std::ostream& os, int v)
- {
- this->output_set(os, v);
- });
+ {
+ if (!dcircles_)
+ {
+ aut_->get_acceptance().to_text
+ (os_, [this](std::ostream& os, int v)
+ {
+ this->output_set(os, v);
+ });
+ }
+ print_acceptance_for_human();
+ }
os_ << "\"\n";
}
else
@@ -456,11 +522,17 @@ namespace spot
os_ << "
";
}
if (opt_show_acc_)
- aut_->get_acceptance().to_html
- (os_, [this](std::ostream& os, int v)
- {
- this->output_html_set_aux(os, v);
- });
+ {
+ if (!dcircles_)
+ {
+ 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_ << " labelloc=\"t\"\n";
@@ -517,9 +589,7 @@ namespace spot
void
process_state(unsigned s)
{
- if (mark_states_ &&
- ((opt_bullet && !opt_bullet_but_buchi)
- || aut_->num_sets() != 1))
+ if (mark_states_ && !dcircles_)
{
acc_cond::mark_t acc = 0U;
for (auto& t: aut_->out(s))
@@ -589,7 +659,7 @@ namespace spot
// Use state_acc_sets(), not state_is_accepting() because
// on co-Büchi automata we want to mark the rejecting
// states.
- if (mark_states_ && aut_->state_acc_sets(s))
+ if (dcircles_ && aut_->state_acc_sets(s))
os_ << ", peripheries=2";
}
if (highlight_states_)
@@ -745,6 +815,9 @@ namespace spot
name_ = aut_->get_named_prop("automaton-name");
mark_states_ = (!opt_force_acc_trans_
&& 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 (sn_ || sprod_ || aut->num_states() > 100
diff --git a/tests/core/alternating.test b/tests/core/alternating.test
index 50c8814aa..ab2a97a8b 100755
--- a/tests/core/alternating.test
+++ b/tests/core/alternating.test
@@ -58,7 +58,7 @@ autfilt --dot=bans alt.hoa >alt.dot
cat >expect.dot < -11 [arrowhead=onormal]
@@ -500,937 +500,7 @@ style='arrowhead=onormal'
cat >expect6.dot<ex2<ex3<ex4<expect4<expect4d< out4
-diff expect4 out4
-run 0 autfilt --remove-dead-states ex4 > out4
-diff expect4d out4
-
-
-cat >ex5< out5
-cat >expect <ex6< ex6.dot
-
-style='arrowhead=onormal'
-cat >expect6.dot<ex2<ex3<ex4<expect4<expect4d< out4
-diff expect4 out4
-run 0 autfilt --remove-dead-states ex4 > out4
-diff expect4d out4
-
-
-cat >ex5< out5
-cat >expect <ex6< ex6.dot
-
-style='arrowhead=onormal'
-cat >expect6.dot<ex2<ex3<ex4<expect4<expect4d< out4
-diff expect4 out4
-run 0 autfilt --remove-dead-states ex4 > out4
-diff expect4d out4
-
-
-cat >ex5< out5
-cat >expect <ex6< ex6.dot
-
-style='arrowhead=onormal'
-cat >expect6.dot<⓿)>
+ label=⓿)
[co-Büchi]>
labelloc="t"
node [shape="circle"]
fontname="Lato"
@@ -1447,7 +517,7 @@ digraph G {
-1.1 [label=<>,shape=point]
-1.1 -> 0 [style=bold, color="#FF4DA0"]
-1.1 -> 1 [style=bold, color="#FF4DA0"]
- 0 -> -1.2 [label=, style=bold, color="#FF7F00", $style]
+ 0 -> -1.2 [label=, style=bold, color="#FF7F00", arrowhead=onormal]
-1.2 [label=<>,shape=point]
-1.2 -> 0 [style=bold, color="#FF7F00"]
-1.2 -> 1 [style=bold, color="#FF7F00"]
@@ -1455,7 +525,6 @@ digraph G {
1 -> 1 [label=]
}
EOF
-
diff ex6.dot expect6.dot
cat >ex7< ex9.dot
cat >expect9.dot <⓿)>
+ label=⓿)
[co-Büchi]>
labelloc="t"
node [shape="circle"]
fontname="Lato"
@@ -1716,7 +785,7 @@ run 0 autfilt --dot='baryf(Lato)' ex10 > ex10.dot
cat >expect10.dot <⓿)>
+ label=⓿)
[co-Büchi]>
labelloc="t"
node [shape="circle"]
fontname="Lato"
@@ -1772,7 +841,7 @@ run 2 autfilt --dot='sbarf(Lato)' ex11 > ex11.dot
cat >expect11.dot <⓿)>
+ label=⓿)
[co-Büchi]>
labelloc="t"
fontname="Lato"
node [fontname="Lato"]
diff --git a/tests/core/readsave.test b/tests/core/readsave.test
index 90005c2f2..6b6548f51 100755
--- a/tests/core/readsave.test
+++ b/tests/core/readsave.test
@@ -357,7 +357,7 @@ cat output
cat >expected <expected <expected <
+ label=[gen. Büchi 2]>
labelloc="t"
fontname="Lato"
node [fontname="Lato"]
@@ -470,7 +470,7 @@ EOF
cat >expected < 0
@@ -524,7 +524,7 @@ diff out expected
cat >expected2 <output6d2
cat >expect6d2 <⓿)>
+ label=⓿)
[Büchi]>
labelloc="t"
I [label="", style=invis, width=0]
I -> 1
diff --git a/tests/python/_altscc.ipynb b/tests/python/_altscc.ipynb
index 30aaa5aa6..6c67c1445 100644
--- a/tests/python/_altscc.ipynb
+++ b/tests/python/_altscc.ipynb
@@ -15,7 +15,7 @@
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
- "version": "3.5.3"
+ "version": "3.5.4"
},
"name": ""
},
@@ -78,14 +78,15 @@
"\n",
"\n",
- "