From a4b63e8e7fe8f2a205564ab54350cbbcd7d86cda Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 28 Apr 2015 18:22:08 +0200 Subject: [PATCH] dot: heuristic to switch between circles and ellipses * src/twaalgos/dotty.cc: Add an option (e) to force elliptic shape, and a heuristic to choose between circle and ellipse by default. * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc: Document 'e'. * src/taalgos/dotty.cc: Ignore 'e'. * wrap/python/spot.py (setup): Do not force circular states. The default should be fine. * src/tests/det.test, src/tests/dstar.test, src/tests/monitor.test, src/tests/neverclaimread.test, src/tests/readsave.test, src/tests/sccdot.test, src/tests/tgbagraph.test: Adjust expected results. * NEWS: Adjust. --- NEWS | 10 ++++++---- src/bin/common_aoutput.cc | 5 +++-- src/bin/dstar2tgba.cc | 7 ++++--- src/taalgos/dotty.cc | 1 + src/tests/det.test | 1 + src/tests/dstar.test | 5 +++++ src/tests/monitor.test | 1 + src/tests/neverclaimread.test | 1 + src/tests/readsave.test | 9 ++++++--- src/tests/sccdot.test | 1 + src/tests/tgbagraph.test | 9 +++++++-- src/twaalgos/dotty.cc | 35 ++++++++++++++++++++++++++++------- wrap/python/spot.py | 2 +- 13 files changed, 65 insertions(+), 22 deletions(-) diff --git a/NEWS b/NEWS index fe459e73e..457c9cc00 100644 --- a/NEWS +++ b/NEWS @@ -187,10 +187,12 @@ New in spot 1.99b (not yet released) sugar for [:*1..], and corresponds to the operator ⊕ introduced by Dax et al. (ATVA'09). - - GraphViz output now uses an horizontal layout by default. The - --dot option of the various command-line tools takes an optional - parameter to fine-tune the GraphViz output (including vertical - layout, round states, named automata, SCC informations, ordered + - GraphViz output now uses an horizontal layout by default, and + also use circular states (unless the automaton has more than 100 + states, or uses named-states). The --dot option of the various + command-line tools takes an optional parameter to fine-tune the + GraphViz output (including vertical layout, forced circular or + elliptic states, named automata, SCC information, ordered transitions, and different ways to colorize the acceptance sets). The environment variables SPOT_DOTDEFAULT and SPOT_DOTEXTRA can also be used to respectively provide a default diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 6a0c3869b..7ae9172cc 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -51,13 +51,14 @@ static const argp_option options[] = { /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, - { "dot", OPT_DOT, "1|a|b|B|c|f(FONT)|h|n|N|o|r|R|s|t|v", + { "dot", OPT_DOT, "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v", OPTION_ARG_OPTIONAL, "GraphViz's format (default). Add letters for " "(1) force numbered states, " "(a) acceptance display, (b) acceptance sets as bullets, " "(B) bullets except for Büchi/co-Büchi automata, " - "(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, " + "(c) force circular nodes, (e) force elliptic nodes, " + "(f(FONT)) use FONT, (h) horizontal layout, " "(v) vertical layout, (n) with name, (N) without name, " "(o) ordered transitions, " "(r) rainbow colors for acceptance sets, " diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 0563f5321..e1ed9f657 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -73,13 +73,14 @@ static const argp_option options[] = "of the given property)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, - { "dot", OPT_DOT, "1|a|b|B|c|f(FONT)|h|n|N|o|r|R|s|t|v", + { "dot", OPT_DOT, "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v", OPTION_ARG_OPTIONAL, "GraphViz's format (default). Add letters for " "(1) force numbered states, " "(a) acceptance display, (b) acceptance sets as bullets, " - "(B) bullets except for Büchi automata, " - "(c) circular nodes, (f(FONT)) use FONT, (h) horizontal layout, " + "(B) bullets except for Büchi/co-Büchi automata, " + "(c) force circular nodes, (e) force elliptic nodes, " + "(f(FONT)) use FONT, (h) horizontal layout, " "(v) vertical layout, (n) with name, (N) without name, " "(o) ordered transitions, " "(r) rainbow colors for acceptance sets, " diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index d50acc345..aeee34f14 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -88,6 +88,7 @@ namespace spot case 'a': case 'b': case 'B': + case 'e': case 'n': case 'N': case 'o': diff --git a/src/tests/det.test b/src/tests/det.test index 336e549f0..8b5bff541 100755 --- a/src/tests/det.test +++ b/src/tests/det.test @@ -118,6 +118,7 @@ run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba cat >ex.tgba < 0 0 [label="0"] diff --git a/src/tests/dstar.test b/src/tests/dstar.test index 2695fcc68..1fdc3f9b3 100755 --- a/src/tests/dstar.test +++ b/src/tests/dstar.test @@ -61,6 +61,7 @@ run 0 ../ltl2tgba -XD dra.dstar | tee stdout cat >expected < 0 0 [label="0"] @@ -82,6 +83,7 @@ run 0 ../ltl2tgba -XDD dra.dstar | tee stdout cat >expected < 0 0 [label="0"] @@ -126,6 +128,7 @@ run 0 ../ltl2tgba -XDB dsa.dstar | tee stdout cat >expected < 0 0 [label="0"] @@ -215,6 +218,7 @@ run 0 ../ltl2tgba -XDD dra.dstar | tee stdout cat >expected < 0 0 [label="0"] @@ -264,6 +268,7 @@ digraph G { rankdir=LR label="aut.dsa" labelloc="t" + node [shape="circle"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] diff --git a/src/tests/monitor.test b/src/tests/monitor.test index 3e75aef31..b832b469b 100755 --- a/src/tests/monitor.test +++ b/src/tests/monitor.test @@ -34,6 +34,7 @@ expect() expect ../../bin/ltl2tgba --monitor a < 1 0 [label="0"] diff --git a/src/tests/neverclaimread.test b/src/tests/neverclaimread.test index 376961805..885a2b468 100755 --- a/src/tests/neverclaimread.test +++ b/src/tests/neverclaimread.test @@ -134,6 +134,7 @@ run 0 ../ltl2tgba -XN input > stdout cat >expected < 0 0 [label="0", peripheries=2] diff --git a/src/tests/readsave.test b/src/tests/readsave.test index 1fe6acfe2..831cf77bd 100755 --- a/src/tests/readsave.test +++ b/src/tests/readsave.test @@ -349,6 +349,7 @@ digraph G { rankdir=LR label="Inf(0)&Inf(1)" labelloc="t" + node [shape="circle"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] @@ -367,6 +368,7 @@ digraph G { rankdir=LR label="G(Fa & Fb)\nInf(⓿)&Inf(❶)" labelloc="t" + node [shape="circle"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] @@ -379,7 +381,7 @@ EOF diff output expected -SPOT_DOTDEFAULT=bra $ltl2tgba --dot='c.f(Lato)' 'GFa & GFb' >output +SPOT_DOTDEFAULT=bra $ltl2tgba --dot='e.f(Lato)' 'GFa & GFb' >output cat output zero='⓿' @@ -389,7 +391,6 @@ digraph G { rankdir=LR label= labelloc="t" - node [shape="circle"] fontname="Lato" node [fontname="Lato"] edge [fontname="Lato"] @@ -515,6 +516,7 @@ digraph G { rankdir=LR label="Fin(⓿) | (Fin(❶) & Inf(❷)) | Fin(❸)" labelloc="t" + node [shape="circle"] I [label="", style=invis, width=0] 0 [label="0"] 1 [label="1\n⓿❸"] @@ -529,7 +531,8 @@ digraph G { } EOF -# This should remove the state names +# This should remove the state names, and automatically use circled +# states. $autfilt --dot=bao1 in | grep -v '>' >out diff out expected2 diff --git a/src/tests/sccdot.test b/src/tests/sccdot.test index 1a291e386..fd203ba17 100755 --- a/src/tests/sccdot.test +++ b/src/tests/sccdot.test @@ -76,6 +76,7 @@ digraph G { rankdir=LR label="Fin(2) & (Inf(0)&Inf(1))" labelloc="t" + node [shape="circle"] I [label="", style=invis, width=0] I -> 1 subgraph cluster_0 { diff --git a/src/tests/tgbagraph.test b/src/tests/tgbagraph.test index 14d60a1fb..ac5d60025 100755 --- a/src/tests/tgbagraph.test +++ b/src/tests/tgbagraph.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -35,6 +35,7 @@ run 0 ../tgbagraph | tee stdout cat >expected < 0 0 [label="0"] @@ -50,6 +51,7 @@ digraph G { } digraph G { rankdir=LR + node [shape="circle"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] @@ -63,6 +65,7 @@ digraph G { } digraph G { rankdir=LR + node [shape="circle"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] @@ -75,6 +78,7 @@ digraph G { } digraph G { rankdir=LR + node [shape="circle"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] @@ -90,6 +94,7 @@ digraph G { } digraph G { rankdir=LR + node [shape="circle"] I [label="", style=invis, width=0] I -> 0 0 [label="0"] diff --git a/src/twaalgos/dotty.cc b/src/twaalgos/dotty.cc index 06cd9850d..b016650fb 100644 --- a/src/twaalgos/dotty.cc +++ b/src/twaalgos/dotty.cc @@ -47,7 +47,8 @@ namespace spot bool opt_force_acc_trans_ = false; bool opt_horizontal_ = true; bool opt_name_ = false; - bool opt_circles_ = false; + enum { ShapeAuto = 0, ShapeCircle, ShapeEllipse } + opt_shape_ = ShapeAuto; bool opt_show_acc_ = false; bool mark_states_ = false; bool opt_scc_ = false; @@ -123,10 +124,10 @@ namespace spot opt_bullet_but_buchi = true; break; case 'c': - opt_circles_ = true; + opt_shape_ = ShapeCircle; break; - case 'h': - opt_horizontal_ = true; + case 'e': + opt_shape_ = ShapeEllipse; break; case 'f': if (*options != '(') @@ -141,6 +142,9 @@ namespace spot options = end + 1; } break; + case 'h': + opt_horizontal_ = true; + break; case 'n': opt_name_ = true; break; @@ -275,7 +279,6 @@ namespace spot aut_->get_acceptance().used_inf_fin_sets(); if (opt_bullet && aut_->acc().num_sets() <= MAX_BULLET) opt_all_bullets = true; - os_ << "digraph G {\n"; if (opt_horizontal_) os_ << " rankdir=LR\n"; @@ -317,8 +320,18 @@ namespace spot } os_ << " labelloc=\"t\"\n"; } - if (opt_circles_) - os_ << " node [shape=\"circle\"]\n"; + switch (opt_shape_) + { + case ShapeCircle: + os_ << " node [shape=\"circle\"]\n"; + break; + case ShapeEllipse: + // Do not print anything. Ellipse is + // the default shape used by GraphViz. + break; + case ShapeAuto: + SPOT_UNREACHABLE(); + } if (!opt_font_.empty()) os_ << " fontname=\"" << opt_font_ << "\"\n node [fontname=\"" << opt_font_ @@ -452,8 +465,16 @@ namespace spot if (opt_name_) name_ = aut_->get_named_prop("automaton-name"); mark_states_ = !opt_force_acc_trans_ && aut_->has_state_based_acc(); + if (opt_shape_ == ShapeAuto) + { + if (sn_ || aut->num_states() > 100) + opt_shape_ = ShapeEllipse; + else + opt_shape_ = ShapeCircle; + } auto si = std::unique_ptr(opt_scc_ ? new scc_info(aut) : nullptr); + start(); if (si) { diff --git a/wrap/python/spot.py b/wrap/python/spot.py index 6c3d7c8b6..fd6e367d8 100644 --- a/wrap/python/spot.py +++ b/wrap/python/spot.py @@ -48,7 +48,7 @@ def setup(**kwargs): kwargs.get('fillcolor', '#ffffaa')) bullets = 'B' if kwargs.get('bullets', True) else '' - d = 'rcf({})'.format(kwargs.get('font', 'Lato')) + bullets + d = 'rf({})'.format(kwargs.get('font', 'Lato')) + bullets os.environ['SPOT_DOTDEFAULT'] = d # Global BDD dict so that we do not have to create one in user code.