Commit a7051b32 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

dot: fix #393

* spot/twaalgos/dot.cc: Add support for option 'E', and default to
rectangle nodes for large labels.
* bin/common_aoutput.cc, NEWS: Document it.
* tests/core/alternating.test, tests/core/dstar.test,
tests/core/readsave.test, tests/core/sccdot.test,
tests/core/tgbagraph.test, tests/python/_product_weak.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/parity.ipynb, tests/python/pdegen.py,
tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb: Adjust all
test cases.
parent 3ea63e9a
Pipeline #18488 failed with stage
in 190 minutes and 28 seconds
......@@ -36,6 +36,12 @@ New in spot 2.8.7.dev (not yet released)
- ltlsynt --algo=lar uses the new version of to_parity() mentionned
below. The old version is available via --algo=lar.old
- The dot printer is now automatically using rectangles with rounded
corners for automata states if one state label have five or more
characters. This saves space with very long labels. Use --dot=c,
--dot=e, or --dot=E to force the use of Circles, Ellipses, or
rEctangles.
Library:
- Historically, Spot only supports LTL with infinite semantics
......@@ -110,6 +116,13 @@ New in spot 2.8.7.dev (not yet released)
dealing with n-ary operators and isolating subsets of operands
that can be relabeled as a single term.
- print_dot() default was changed to use circles for automata with
fewer than 10 unamed states, ellipses for automata with up to 1000
unamed states (or named states with up to 4 characters), and
rounded rectangles otherwise. Rectangles are also used for
automata with acceptance bullets on states. The new "E" option
can be used to force rectangles in all situations.
Backward-incompatible changes:
- iar() and iar_maybe() have been moved from
......
// -*- coding: utf-8 -*-
// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
// Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -97,7 +97,7 @@ static const argp_option options[] =
/**************************************************/
{ nullptr, 0, nullptr, 0, "Output format:", 3 },
{ "dot", 'd',
"1|a|A|b|B|c|C(COLOR)|e|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#",
"1|a|A|b|B|c|C(COLOR)|e|E|f(FONT)|h|k|K|n|N|o|r|R|s|t|u|v|y|+INT|<INT|#",
OPTION_ARG_OPTIONAL,
"GraphViz's format. Add letters for "
"(1) force numbered states, "
......@@ -109,6 +109,7 @@ static const argp_option options[] =
"(C) color nodes with COLOR, "
"(d) show origins when known, "
"(e) force elliptic nodes, "
"(E) force rEctangular nodes, "
"(f(FONT)) use FONT, "
"(g) hide edge labels, "
"(h) horizontal layout, "
......
......@@ -86,7 +86,9 @@ namespace spot
acc_cond::mark_t inf_sets_ = {};
acc_cond::mark_t fin_sets_ = {};
unsigned opt_shift_sets_ = 0;
enum { ShapeAuto = 0, ShapeCircle, ShapeEllipse } opt_shape_ = ShapeAuto;
enum { ShapeAuto = 0, ShapeCircle, ShapeEllipse,
ShapeRectangle } opt_shape_ = ShapeAuto;
const char* extrastyle = "";
bool opt_force_acc_trans_ = false;
bool opt_vertical_ = false;
bool opt_name_ = false;
......@@ -254,6 +256,9 @@ namespace spot
case 'e':
opt_shape_ = ShapeEllipse;
break;
case 'E':
opt_shape_ = ShapeRectangle;
break;
case 'f':
if (*options != '(')
throw std::runtime_error
......@@ -495,7 +500,8 @@ namespace spot
return;
std::string dest = string_dst(dst, color_num);
if (univ == 0)
os_ << " " << dest << " [label=<>,shape=point]\n";
os_ << " " << dest
<< " [label=<>,shape=point,width=0.05,height=0.05]\n";
if (print_edges)
{
for (unsigned d: aut_->univ_dests(dst))
......@@ -603,14 +609,18 @@ namespace spot
os_ << " node [shape=\"circle\"]\n";
break;
case ShapeEllipse:
// Do not print anything. Ellipse is
// the default shape used by GraphViz.
// Ellipse is the default shape used by GraphViz, but
// with set width and height so it's a circle when possible.
os_ << " node [shape=\"ellipse\",width=\"0.5\",height=\"0.5\"]\n";
break;
case ShapeRectangle:
os_ << " node [shape=\"box\",style=\"rounded\",width=\"0.5\"]\n";
break;
case ShapeAuto:
SPOT_UNREACHABLE();
}
if (!opt_node_color_.empty())
os_ << " node [style=\"filled\", fillcolor=\""
os_ << " node [style=\"filled" << extrastyle << "\", fillcolor=\""
<< opt_node_color_ << "\"]\n";
if (!opt_font_.empty())
os_ << " fontname=\"" << opt_font_
......@@ -713,7 +723,7 @@ namespace spot
auto iter = highlight_states_->find(s);
if (iter != highlight_states_->end())
{
os_ << ", style=\"bold";
os_ << ", style=\"bold" << extrastyle;
if (!opt_node_color_.empty())
os_ << ",filled";
os_ << "\", color=\"" << palette[iter->second % palette_mod]
......@@ -884,7 +894,8 @@ namespace spot
if (opt_name_)
name_ = graph_name_;
mark_states_ = (!opt_force_acc_trans_
&& aut_->prop_state_acc().is_true());
&& aut_->prop_state_acc().is_true()
&& aut_->num_sets() > 0);
dcircles_ = (mark_states_
&& (!opt_bullet || opt_bullet_but_buchi)
&& (aut_->acc().is_buchi() || aut_->acc().is_co_buchi()));
......@@ -892,22 +903,37 @@ namespace spot
{
if ((inline_state_names_ && (sn_ || sprod_ || opt_state_labels_))
|| (opt_state_labels_ && opt_latex_)
|| aut->num_states() > 100
|| aut->num_states() > 1000
|| (mark_states_ && !dcircles_)
|| orig_)
{
opt_shape_ = ShapeRectangle;
// If all state names are very short, prefer ellipses.
if (!opt_state_labels_ && !orig_
&& !(mark_states_ && !dcircles_)
&& ((sn_ && std::all_of(sn_->begin(), sn_->end(),
[](const std::string& s)
{ return s.size() <= 4; }))
|| (sprod_ && std::all_of(sprod_->begin(),
sprod_->end(),
[](auto p)
{
return (p.first < 100
&& p.second < 100);
}))))
opt_shape_ = ShapeEllipse;
}
else if (aut->num_states() > 10)
{
opt_shape_ = ShapeEllipse;
// If all state names are short, prefer circles.
if (!opt_state_labels_ && !orig_ &&
sn_ && std::all_of(sn_->begin(), sn_->end(),
[](const std::string& s)
{ return s.size() <= 2; }))
opt_shape_ = ShapeCircle;
}
else
{
opt_shape_ = ShapeCircle;
}
}
if (opt_shape_ == ShapeRectangle)
extrastyle = ",rounded";
auto si =
std::unique_ptr<scc_info>(opt_scc_ ? new scc_info(aut) : nullptr);
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2016-2018 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2016-2018, 2020 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
......@@ -62,6 +62,7 @@ digraph "" {
rankdir=LR
label="Fin(⓿)\n[co-Büchi]"
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> -11 [arrowhead=onormal]
subgraph cluster_0 {
......@@ -88,7 +89,7 @@ digraph "" {
color=green
label=""
3 [label="GF(b)"]
-8 [label=<>,shape=point]
-8 [label=<>,shape=point,width=0.05,height=0.05]
}
subgraph cluster_5 {
color=red
......@@ -100,15 +101,15 @@ digraph "" {
label=""
0 [label="((((a) U (b)) && GF(b)) && FG(a))"]
}
-11 [label=<>,shape=point]
-11 [label=<>,shape=point,width=0.05,height=0.05]
-11 -> 0
-11 -> 2
0 -> -1 [label="b", arrowhead=onormal]
-1 [label=<>,shape=point]
-1 [label=<>,shape=point,width=0.05,height=0.05]
-1 -> 1
-1 -> 3
0 -> -4 [label="a & !b", style=bold, color="#E31A1C", arrowhead=onormal]
-4 [label=<>,shape=point]
-4 [label=<>,shape=point,width=0.05,height=0.05]
-4 -> 1 [style=bold, color="#E31A1C"]
-4 -> 3 [style=bold, color="#E31A1C"]
-4 -> 5 [style=bold, color="#E31A1C"]
......@@ -506,23 +507,23 @@ digraph "" {
rankdir=LR
label=<Fin(<font color="#1F78B4"></font>)<br/>[co-Büchi]>
labelloc="t"
node [shape="circle"]
node [shape="box",style="rounded",width="0.5"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
I [label="", style=invis, width=0]
I -> -1 [arrowhead=onormal]
-1 [label=<>,shape=point]
-1 [label=<>,shape=point,width=0.05,height=0.05]
-1 -> 0
-1 -> 1
0 [label=<0>]
0 -> 0 [label=<!a &amp; !c>]
0 -> -1.1 [label=<a &amp; b &amp; !c>, style=bold, color="#FF4DA0", $style]
-1.1 [label=<>,shape=point]
-1.1 [label=<>,shape=point,width=0.05,height=0.05]
-1.1 -> 0 [style=bold, color="#FF4DA0"]
-1.1 -> 1 [style=bold, color="#FF4DA0"]
0 -> -1.2 [label=<a &amp; !c>, style=bold, color="#FF7F00", arrowhead=onormal]
-1.2 [label=<>,shape=point]
-1.2 [label=<>,shape=point,width=0.05,height=0.05]
-1.2 -> 0 [style=bold, color="#FF7F00"]
-1.2 -> 1 [style=bold, color="#FF7F00"]
1 [label=<1>]
......@@ -569,6 +570,7 @@ digraph "SLAA for c R (c | G(a & b) | (F!b & F!a))" {
rankdir=LR
label=<Fin($color1) &amp; Fin($color)<br/>[Streett-like 2]>
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
......@@ -598,10 +600,10 @@ digraph "SLAA for c R (c | G(a & b) | (F!b & F!a))" {
color=green
label=""
0 [label=<c R (c | G(a &amp; b) | (F!b &amp; F!a))>]
-1 [label=<>,shape=point]
-4 [label=<>,shape=point]
-7 [label=<>,shape=point]
-10 [label=<>,shape=point]
-1 [label=<>,shape=point,width=0.05,height=0.05]
-4 [label=<>,shape=point,width=0.05,height=0.05]
-7 [label=<>,shape=point,width=0.05,height=0.05]
-10 [label=<>,shape=point,width=0.05,height=0.05]
}
0 -> 4 [label=<c>]
0 -> 0 [label=<!a &amp; !b &amp; !c>]
......@@ -665,6 +667,7 @@ digraph "SLAA for c R (c | G(a & b) | (F!b & F!a))" {
rankdir=LR
label=<Fin($color1) &amp; Fin($color)<br/>[Streett-like 2]>
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
......@@ -689,11 +692,11 @@ digraph "SLAA for c R (c | G(a & b) | (F!b & F!a))" {
color=green
label=""
0 [label=<c R (c | G(a &amp; b) | (F!b &amp; F!a))>]
-1 [label=<>,shape=point]
-4 [label=<>,shape=point]
-7 [label=<>,shape=point]
-1 [label=<>,shape=point,width=0.05,height=0.05]
-4 [label=<>,shape=point,width=0.05,height=0.05]
-7 [label=<>,shape=point,width=0.05,height=0.05]
1 [label=<G(a &amp; b)>]
-10 [label=<>,shape=point]
-10 [label=<>,shape=point,width=0.05,height=0.05]
}
0 -> 4 [label=<c>]
0 -> 0 [label=<!a &amp; !b &amp; !c>]
......@@ -745,7 +748,7 @@ digraph "" {
rankdir=LR
label=<Fin(<font color="#1F78B4"></font>)<br/>[co-Büchi]>
labelloc="t"
node [shape="circle"]
node [shape="box",style="rounded",width="0.5"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
......@@ -753,14 +756,14 @@ digraph "" {
I -> 0
0 [label=<0>]
0 -> -1.1 [label=<b &amp; c>, style=bold, color="#FF4DA0", arrowhead=onormal]
-1.1 [label=<>,shape=point]
-1.1 [label=<>,shape=point,width=0.05,height=0.05]
-1.1 -> 1 [style=bold, color="#FF4DA0"]
-1.1 -> 2 [style=bold, color="#FF4DA0"]
1 [label=<1>]
1 -> -1.1 [label=<a &amp; b>, style=bold, color="#FF4DA0", arrowhead=onormal]
2 [label=<2>]
2 -> -1.2 [label=<!a &amp; !b &amp; !c>, style=bold, color="#FF7F00", $style]
-1.2 [label=<>,shape=point]
-1.2 [label=<>,shape=point,width=0.05,height=0.05]
-1.2 -> 1 [style=bold, color="#FF7F00"]
-1.2 -> 2 [style=bold, color="#FF7F00"]
}
......@@ -792,7 +795,7 @@ digraph "" {
rankdir=LR
label=<Fin(<font color="#1F78B4"></font>)<br/>[co-Büchi]>
labelloc="t"
node [shape="circle"]
node [shape="box",style="rounded",width="0.5"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
......@@ -800,17 +803,17 @@ digraph "" {
I -> 0
0 [label=<0>]
0 -> -1.1 [label=<b &amp; c>, style=bold, color="#FF4DA0", arrowhead=onormal]
-1.1 [label=<>,shape=point]
-1.1 [label=<>,shape=point,width=0.05,height=0.05]
-1.1 -> 1 [style=bold, color="#FF4DA0"]
-1.1 -> 2 [style=bold, color="#FF4DA0"]
1 [label=<1>]
1 -> -1.3 [label=<a &amp; b>, style=bold, color="#6A3D9A", arrowhead=onormal]
-1.3 [label=<>,shape=point]
-1.3 [label=<>,shape=point,width=0.05,height=0.05]
-1.3 -> 1 [style=bold, color="#6A3D9A"]
-1.3 -> 2 [style=bold, color="#6A3D9A"]
2 [label=<2>]
2 -> -1.2 [label=<!a &amp; !b &amp; !c>, style=bold, color="#FF7F00", $style]
-1.2 [label=<>,shape=point]
-1.2 [label=<>,shape=point,width=0.05,height=0.05]
-1.2 -> 1 [style=bold, color="#FF7F00"]
-1.2 -> 2 [style=bold, color="#FF7F00"]
}
......@@ -848,6 +851,7 @@ digraph "SLAA for G((b & Fa) | (!b & G!a))" {
rankdir=LR
label=<Fin(<font color="#1F78B4"></font>)<br/>[co-Büchi]>
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
......@@ -872,8 +876,8 @@ digraph "SLAA for G((b & Fa) | (!b & G!a))" {
color=green
label=""
0 [label=<G((b &amp; Fa) | (!b &amp; G!a))>]
-1 [label=<>,shape=point]
-4 [label=<>,shape=point]
-1 [label=<>,shape=point,width=0.05,height=0.05]
-4 [label=<>,shape=point,width=0.05,height=0.05]
}
0 -> 0 [label=<a &amp; b>]
0 -> -1 [label=<!a &amp; b>, arrowhead=onormal]
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2013-2016, 2018 Laboratoire de Recherche et
# Copyright (C) 2013-2016, 2018, 2020 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
......@@ -63,7 +63,7 @@ digraph "" {
rankdir=LR
label="Fin(0) & Inf(1)\n[Rabin 1]"
labelloc="t"
node [shape="circle"]
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
......
......@@ -420,6 +420,7 @@ digraph "G(Fa & Fb)" {
rankdir=LR
label=<Inf($zero)&amp;Inf($one)<br/>[gen. Büchi 2]>
labelloc="t"
node [shape="ellipse",width="0.5",height="0.5"]
fontname="Lato"
node [fontname="Lato"]
edge [fontname="Lato"]
......@@ -491,6 +492,7 @@ digraph "" {
rankdir=LR
label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))\n[gen. Rabin 3]"
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
......@@ -545,7 +547,7 @@ digraph "" {
rankdir=LR
label="(Fin(⓿)|Fin(❸)) | (Fin(❶) & Inf(❷))\n[gen. Rabin 3]"
labelloc="t"
node [shape="circle"]
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
0 [label="0"]
1 [label="1\n⓿❸", tooltip="test me"]
......@@ -568,7 +570,7 @@ diff out expected2
cat >expected3 <<EOF
digraph "" {
rankdir=LR
node [shape="circle"]
node [shape="ellipse",width="0.5",height="0.5"]
I [label="", style=invis, width=0]
0 [label="6", peripheries=2]
u0 [label="...", shape=none, width=0, height=0, tooltip="hidden successors"]
......@@ -891,6 +893,7 @@ run 0 autfilt -dAk input6 >output6d
cat >expect6d <<EOF
digraph "" {
rankdir=LR
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> 1
0 [label="0\nb"]
......@@ -914,6 +917,7 @@ digraph "" {
rankdir=LR
label=<Inf(<font color="#1F78B4"></font>)<br/>[Büchi]>
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> 1
0 [label=<0<br/>b>]
......@@ -1031,14 +1035,15 @@ autfilt -dA input9 > output9
cat >expected9 <<EOF
digraph "a U (b U c)" {
rankdir=LR
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> 2
0 [label="0", peripheries=2, style="bold", color="#1F78B4"]
0 [label="0", peripheries=2, style="bold,rounded", color="#1F78B4"]
0 -> 0 [label="1", style=bold, color="#1F78B4"]
1 [label="1"]
1 -> 0 [label="c", style=bold, color="#FF4DA0"]
1 -> 1 [label="b & !c", style=bold, color="#FF7F00"]
2 [label="new\nline", style="bold", color="#6A3D9A"]
2 [label="new\nline", style="bold,rounded", color="#6A3D9A"]
2 -> 0 [label="c", style=bold, color="#6A3D9A"]
2 -> 1 [label="!a & b & !c"]
2 -> 2 [label="a & !c"]
......@@ -1046,12 +1051,13 @@ digraph "a U (b U c)" {
EOF
diff output9 expected9
autfilt -dbar input9 > output9a
style=', style="bold", color="#1F78B4"'
style=', style="bold,rounded", color="#1F78B4"'
cat >expected9a <<EOF
digraph "a U (b U c)" {
rankdir=LR
label=<Inf(<font color="#1F78B4"></font>)<br/>[Büchi]>
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> 2
0 [label=<0<br/><font color="#1F78B4"></font>>$style]
......@@ -1059,7 +1065,7 @@ digraph "a U (b U c)" {
1 [label=<1>]
1 -> 0 [label=<c>, style=bold, color="#FF4DA0"]
1 -> 1 [label=<b &amp; !c>, style=bold, color="#FF7F00"]
2 [label=<new<br/>line>, style="bold", color="#6A3D9A"]
2 [label=<new<br/>line>, style="bold,rounded", color="#6A3D9A"]
2 -> 0 [label=<c>, style=bold, color="#6A3D9A"]
2 -> 1 [label=<!a &amp; b &amp; !c>]
2 -> 2 [label=<a &amp; !c>]
......@@ -1097,6 +1103,7 @@ ltl2tgba 'a U b' | autfilt --remove-ap=b=0 --name=%M --dot=dA >out
cat >expected <<EOF
digraph "a U b" {
rankdir=LR
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0 (1)"]
......
......@@ -76,7 +76,7 @@ digraph "" {
rankdir=LR
label="(Inf(0)&Inf(1)) & Fin(2)\n[Streett-like 3]"
labelloc="t"
node [shape="circle"]
node [shape="ellipse",width="0.5",height="0.5"]
I [label="", style=invis, width=0]
I -> 1
subgraph cluster_0 {
......
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
# Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
......@@ -122,6 +122,7 @@ digraph "" {
rankdir=LR
label="t\n[Fin-less 2]"
labelloc="t"
node [shape="ellipse",width="0.5",height="0.5"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0"]
......@@ -237,7 +238,7 @@ digraph "" {
rankdir=LR
label="t\n[all]"
labelloc="t"
node [shape="circle"]
node [shape="ellipse",width="0.5",height="0.5"]
I [label="", style=invis, width=0]
I -> 2
0 [label="s1", style="bold", color="#E31A1C"]
......@@ -251,7 +252,7 @@ digraph "" {
rankdir=LR
label="t\n[all]"
labelloc="t"
node [shape="circle"]
node [shape="ellipse",width="0.5",height="0.5"]
I [label="", style=invis, width=0]
I -> 0
0 [label="s3", style="bold", color="#505050"]
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -334,6 +334,7 @@ assert dot == """digraph "" {
rankdir=LR
label="Inf(2) | (Inf(1) & Fin(0))\\n[Rabin-like 2]"
labelloc="t"
node [shape="box",style="rounded",width="0.5"]
I [label="", style=invis, width=0]
I -> 0
0 [label="0 (0)"]
......
This diff is collapsed.
This diff is collapsed.
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