diff --git a/NEWS b/NEWS index 3b94d43ab..a08fa6d10 100644 --- a/NEWS +++ b/NEWS @@ -120,6 +120,10 @@ New in spot 2.10.6.dev (not yet released) into the universal edge vector, since the later can be reallocated during that process. + - Printing an alternating automaton with print_dot() using 'u' to + hide true state could produce some incorrect GraphViz output if + the automaton as a true state as part of a universal group. + New in spot 2.10.6 (2022-05-18) Bugs fixed: diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index 66804f304..70b707edc 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -578,10 +578,27 @@ namespace spot return tmp_dst.str(); } - template - void print_true_state(U to, V from) const + void print_hidden_true_name(unsigned to, unsigned from) const { - os_ << " T" << to << 'T' << from << " [label=\"\", style=invis, "; + os_ << 'T' << to << 'T' << from; + } + + void print_hidden_true_name(unsigned to, const std::string& from) const + { + bool neg = from[0] == '-'; + if (neg) + os_ << '"'; + os_ << 'T' << to << 'T' << from; + if (neg) + os_ << '"'; + } + + template + void print_true_state(unsigned to, F from) const + { + os_ << " "; + print_hidden_true_name(to, from); + os_ << " [label=\"\", style=invis, "; os_ << (opt_vertical_ ? "height=0]\n" : "width=0]\n"); } @@ -606,7 +623,7 @@ namespace spot print_true_state(d, dest); os_ << " " << dest << " -> "; if (dst_is_hidden_true_state) - os_ << 'T' << d << 'T' << dest; + print_hidden_true_name(d, dest); else os_ << d; if ((style && *style) || opt_id_) diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 17f012675..df4e47624 100755 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016-2018, 2020-2021 Laboratoire de Recherche et +# Copyright (C) 2016-2018, 2020-2022 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -1009,3 +1009,41 @@ test '2_0_1_1_1_1_3_3' = "`autfilt --stats=$stats in`" autfilt --stats='%[x]U' in 2>stderr && exit2 grep '%\[x\]U' stderr + +cat >in <out.dot +# T0T-1 is not a valid name for GraphViz, it has to be quoted. +cat >exp.dot < 1 + 1 [label="1"] + 1 -> -1 [label="1\n{0}", arrowhead=onormal] + -1 [label=<>,shape=point,width=0.05,height=0.05] + "T0T-1" [label="", style=invis, width=0] + -1 -> "T0T-1" + -1 -> 1 + T0T1 [label="", style=invis, width=0] + 1 -> T0T1 [label="a"] +} +EOF +diff out.dot exp.dot