dot: improve output to work around GraphViz bug

The related GraphViz issue is
https://gitlab.com/graphviz/graphviz/-/issues/2179

* spot/twaalgos/dot.cc: Avoid initial newline in title.
* NEWS: Mention the bug.
* tests/core/det.test, tests/core/dstar.test,
tests/core/neverclaimread.test, tests/python/automata-io.ipynb: Adjust
test cases.
This commit is contained in:
Alexandre Duret-Lutz 2022-01-11 22:19:20 +01:00
parent cfb782ce75
commit da681e6b4d
6 changed files with 23 additions and 11 deletions

3
NEWS
View file

@ -11,6 +11,9 @@ New in spot 2.10.2.dev (not yet released)
32 states due to an optimization of the determinization being 32 states due to an optimization of the determinization being
unintentionally disabled. unintentionally disabled.
- Work around GraphViz bug #2179 by avoiding unnecessary empty
lines in the acceptance conditions shown in dot.
New in spot 2.10.2 (2021-12-03) New in spot 2.10.2 (2021-12-03)
Bugs fixed: Bugs fixed:

View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2014-2021 Laboratoire de Recherche // Copyright (C) 2011, 2012, 2014-2022 Laboratoire de Recherche
// et Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -626,7 +626,16 @@ namespace spot
std::string accstr = aut_->acc().name("d"); std::string accstr = aut_->acc().name("d");
if (accstr.empty()) if (accstr.empty())
return; return;
os_ << nl_ << '[' << accstr << ']'; // If a name or an acceptance formula was printed,
// we need to add a newline before the human version of the acceptance.
//
// We used to always add that line, but on unnamed Büchi
// automata with double circles, this would (1) create an
// empty line, and (2) run into the following GraphViz bug:
// https://gitlab.com/graphviz/graphviz/-/issues/2179
if (name_ || !dcircles_)
os_ << nl_;
os_ << '[' << accstr << ']';
} }
void void

View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013-2021 Laboratoire de Recherche et Développement de # Copyright (C) 2013-2022 Laboratoire de Recherche et Développement de
# l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -113,7 +113,7 @@ run 0 ../ikwiad -x -DC 'GFa & XGFb' > out.tgba
cat >ex.tgba <<EOF cat >ex.tgba <<EOF
digraph "GFa & XGFb" { digraph "GFa & XGFb" {
rankdir=LR rankdir=LR
label="\n[Büchi]" label="[Büchi]"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, width=0] I [label="", style=invis, width=0]

View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013-2016, 2018, 2020 Laboratoire de Recherche et # Copyright (C) 2013-2016, 2018, 2020, 2022 Laboratoire de Recherche
# Développement de l'Epita (LRDE). # et Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
# #
@ -85,7 +85,7 @@ run 0 ../ikwiad -d -XDB -R3 dra.dstar | tee stdout
cat >expected <<EOF cat >expected <<EOF
digraph "" { digraph "" {
rankdir=LR rankdir=LR
label="\n[Büchi]" label="[Büchi]"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, width=0] I [label="", style=invis, width=0]
@ -132,7 +132,7 @@ run 0 ../ikwiad -d -XDB dsa.dstar | tee stdout
cat >expected <<EOF cat >expected <<EOF
digraph "" { digraph "" {
rankdir=LR rankdir=LR
label="\n[Büchi]" label="[Büchi]"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, width=0] I [label="", style=invis, width=0]

View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2010-2015, 2017-2018, 2020 Laboratoire # Copyright (C) 2010-2015, 2017-2018, 2020, 2022 Laboratoire
# de Recherche et Développement de l'Epita (LRDE). # de Recherche et Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -134,7 +134,7 @@ run 0 ../ikwiad -XN input > stdout
cat >expected <<EOF cat >expected <<EOF
digraph "" { digraph "" {
rankdir=LR rankdir=LR
label="\n[Büchi]" label="[Büchi]"
labelloc="t" labelloc="t"
node [shape="circle"] node [shape="circle"]
I [label="", style=invis, width=0] I [label="", style=invis, width=0]

View file

@ -61,7 +61,7 @@
"\n", "\n",
"digraph \"\" {\n", "digraph \"\" {\n",
" rankdir=LR\n", " rankdir=LR\n",
" label=<<br/>[Büchi]>\n", " label=<[Büchi]>\n",
" labelloc=\"t\"\n", " labelloc=\"t\"\n",
" node [shape=\"circle\"]\n", " node [shape=\"circle\"]\n",
" node [style=\"filled\", fillcolor=\"#ffffaa\"]\n", " node [style=\"filled\", fillcolor=\"#ffffaa\"]\n",