diff --git a/NEWS b/NEWS index 8b0b94c82..ac790f486 100644 --- a/NEWS +++ b/NEWS @@ -35,6 +35,10 @@ New in spot 2.7.2.dev (not yet released) by spot::generic_emptiness_check() when processing SCCs recursively, and makes it easier to write similar code in Python. + - print_dot has a new option 'g', to hide edge labels. This is + helpful to display automata as "graphs", e.g., when illustrating + algorithms that do not care about labels. + Bugs fixed: - When processing CSV files with MSDOS-style \r\n line endings, diff --git a/bin/common_aoutput.cc b/bin/common_aoutput.cc index dd6dd8a70..9e8976da9 100644 --- a/bin/common_aoutput.cc +++ b/bin/common_aoutput.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -101,6 +101,7 @@ static const argp_option options[] = "(d) show origins when known, " "(e) force elliptic nodes, " "(f(FONT)) use FONT, " + "(g) hide edge labels, " "(h) horizontal layout, " "(k) use state labels when possible, " "(K) use transition labels (default), " diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc index badbaa1d1..7d3c1b1e3 100644 --- a/spot/twaalgos/dot.cc +++ b/spot/twaalgos/dot.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2012, 2014-2018 Laboratoire de Recherche +// Copyright (C) 2011, 2012, 2014-2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -108,6 +108,7 @@ namespace spot bool opt_orig_show_ = false; bool max_states_given_ = false; // related to max_states_ bool opt_latex_ = false; + bool opt_showlabel_ = true; const char* nl_ = "\\n"; const char* label_pre_ = "label=\""; char label_post_ = '"'; @@ -266,6 +267,9 @@ namespace spot options = end + 1; } break; + case 'g': // "graphs" are unlabeled automata + opt_showlabel_ = false; + break; case 'h': opt_vertical_ = false; break; @@ -756,12 +760,12 @@ namespace spot os_ << '.' << iter->second % palette_mod; } os_ << " [" << label_pre_; - if (!opt_state_labels_) + if (!opt_state_labels_ && opt_showlabel_) format_label(os_, t.cond); if (!mark_states_) if (auto a = t.acc) { - if (!opt_state_labels_) + if (!opt_state_labels_ && opt_showlabel_) os_ << nl_; output_mark(a); } diff --git a/tests/core/readsave.test b/tests/core/readsave.test index 55c985170..c90778d2d 100755 --- a/tests/core/readsave.test +++ b/tests/core/readsave.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009, 2010, 2012, 2014-2018 Laboratoire de +# Copyright (C) 2009, 2010, 2012, 2014-2019 Laboratoire de # Recherche et Développement de l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -390,6 +390,25 @@ digraph "G(Fa & Fb)" { EOF diff output expected +ltl2tgba -dbang 'GFa & GFb' >output +cat output +cat >expected < 0 + 0 [label="0"] + 0 -> 0 [label=""] + 0 -> 0 [label="❶"] + 0 -> 0 [label="⓿"] + 0 -> 0 [label="⓿❶"] +} +EOF +diff output expected + SPOT_DOTDEFAULT=bra ltl2tgba --dot='Ae.f(Lato)' 'GFa & GFb' >output cat output