diff --git a/NEWS b/NEWS index b783f18ea..299c43dd7 100644 --- a/NEWS +++ b/NEWS @@ -71,6 +71,11 @@ New in spot 1.99a (not yet released) - Boost is not used anymore. + - 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, and named automata). + - The tgba_succ_iterator interface has changed. Methods next(), and first() should now return a bool indicating whether the current iteration is valid. diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 3ffa2e55d..54577a03e 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -104,7 +104,10 @@ static const argp_option options[] = /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, { "count", 'c', 0, 0, "print only a count of matched automata", 0 }, - { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "dot", OPT_DOT, "c|h|n|N|t|v", OPTION_ARG_OPTIONAL, + "GraphViz's format (default). Add letters to chose (c) circular nodes, " + "(h) horizontal layout, (v) vertical layout, (n) with name, " + "(N) without name, (t) always transition-based acceptance.", 0 }, { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " "(s) state-based acceptance, (t) transition-based acceptance, " @@ -206,6 +209,7 @@ static const struct argp_child children[] = static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa, Quiet, Count } format = Dot; +const char* opt_dot = nullptr; typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; typedef std::set> unique_aut_t; static long int match_count = 0; @@ -314,6 +318,7 @@ parse_opt(int key, char* arg, struct argp_state*) } case OPT_DOT: format = Dot; + opt_dot = arg; break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); @@ -640,7 +645,8 @@ namespace case Dot: spot::dotty_reachable(std::cout, aut, (type == spot::postprocessor::BA) - || (type == spot::postprocessor::Monitor)); + || (type == spot::postprocessor::Monitor), + opt_dot); break; case Lbtt: spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index c84ab8bc0..adadc167e 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -70,7 +70,10 @@ static const argp_option options[] = "of the given property)", 0 }, /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, - { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "dot", OPT_DOT, "c|h|n|N|t|v", OPTION_ARG_OPTIONAL, + "GraphViz's format (default). Add letters to chose (c) circular nodes, " + "(h) horizontal layout, (v) vertical layout, (n) with name, " + "(N) without name, (t) always transition-based acceptance.", 0 }, { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " "(s) state-based acceptance, (t) transition-based acceptance, " @@ -126,6 +129,7 @@ const struct argp_child children[] = }; enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; +const char* opt_dot = nullptr; bool utf8 = false; const char* stats = ""; const char* hoa_opt = 0; @@ -167,6 +171,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_DOT: format = Dot; + opt_dot = arg; break; case OPT_LBTT: if (arg) @@ -315,7 +320,8 @@ namespace case Dot: spot::dotty_reachable(std::cout, aut, (type == spot::postprocessor::BA) - || (type == spot::postprocessor::Monitor)); + || (type == spot::postprocessor::Monitor), + opt_dot); break; case Lbtt: spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); diff --git a/src/bin/ltl2tgba.cc b/src/bin/ltl2tgba.cc index 9989187d6..d968835a2 100644 --- a/src/bin/ltl2tgba.cc +++ b/src/bin/ltl2tgba.cc @@ -72,7 +72,10 @@ static const argp_option options[] = { 0, 0, 0, 0, "Output format:", 3 }, { "csv-escape", OPT_CSV, 0, 0, "quote formula output by %f in --format " "for use in CSV file", 0 }, - { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "dot", OPT_DOT, "c|h|n|N|t|v", OPTION_ARG_OPTIONAL, + "GraphViz's format (default). Add letters to chose (c) circular nodes, " + "(h) horizontal layout, (v) vertical layout, (n) with name, " + "(N) without name, (t) always transition-based acceptance.", 0 }, { "hoa", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " "(s) state-based acceptance, (t) transition-based acceptance, " @@ -124,7 +127,7 @@ const struct argp_child children[] = }; enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; -bool utf8 = false; +const char* opt_dot = nullptr; const char* stats = ""; const char* hoa_opt = 0; spot::option_map extra_options; @@ -166,6 +169,7 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_DOT: format = Dot; + opt_dot = arg; break; case OPT_LBTT: if (arg) @@ -245,7 +249,8 @@ namespace case Dot: spot::dotty_reachable(std::cout, aut, (type == spot::postprocessor::BA) - || (type == spot::postprocessor::Monitor)); + || (type == spot::postprocessor::Monitor), + opt_dot); break; case Lbtt: spot::lbtt_reachable(std::cout, aut, type == spot::postprocessor::BA); diff --git a/src/bin/randaut.cc b/src/bin/randaut.cc index 1a9b9eadd..a56a41009 100644 --- a/src/bin/randaut.cc +++ b/src/bin/randaut.cc @@ -93,7 +93,10 @@ static const argp_option options[] = RANGE_DOC, /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, - { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, + { "dot", OPT_DOT, "c|h|n|N|t|v", OPTION_ARG_OPTIONAL, + "GraphViz's format (default). Add letters to chose (c) circular nodes, " + "(h) horizontal layout, (v) vertical layout, (n) with name, " + "(N) without name, (t) always transition-based acceptance.", 0 }, { "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, "Output the automaton in HOA format. Add letters to select " "(s) state-based acceptance, (t) transition-based acceptance, " @@ -117,6 +120,7 @@ static const struct argp_child children[] = typedef spot::tgba_digraph::graph_t::trans_storage_t tr_t; typedef std::set> unique_aut_t; static enum output_format { Dot, Lbtt, Lbtt_t, Spin, Hoa } format = Dot; +const char* opt_dot = nullptr; static const char* hoa_opt = 0; static spot::ltl::atomic_prop_set aprops; static bool ap_count_given = false; @@ -210,6 +214,7 @@ parse_opt(int key, char* arg, struct argp_state* as) break; case OPT_DOT: format = Dot; + opt_dot = arg; break; case OPT_LBTT: if (arg) @@ -318,7 +323,7 @@ main(int argc, char** argv) switch (format) { case Dot: - spot::dotty_reachable(std::cout, aut, is_ba); + spot::dotty_reachable(std::cout, aut, is_ba, opt_dot); break; case Lbtt: spot::lbtt_reachable(std::cout, aut, is_ba); diff --git a/src/graphtest/tgbagraph.test b/src/graphtest/tgbagraph.test index 753b97214..9377deb40 100755 --- a/src/graphtest/tgbagraph.test +++ b/src/graphtest/tgbagraph.test @@ -34,7 +34,8 @@ run 0 ../tgbagraph | tee stdout cat >expected < 1 1 [label="0"] 1 -> 1 [label="0"] @@ -48,7 +49,8 @@ digraph G { 3 -> 3 [label="1\n{0,1}"] } digraph G { - 0 [label="", style=invis, height=0] + rankdir=LR + 0 [label="", style=invis, width=0] 0 -> 1 1 [label="0"] 1 -> 1 [label="0"] @@ -60,7 +62,8 @@ digraph G { 3 -> 1 [label="p1 | p2\n{0,1}"] } digraph G { - 0 [label="", style=invis, height=0] + rankdir=LR + 0 [label="", style=invis, width=0] 0 -> 1 1 [label="0"] 1 -> 1 [label="0"] @@ -71,7 +74,8 @@ digraph G { 3 [label="2"] } digraph G { - 0 [label="", style=invis, height=0] + rankdir=LR + 0 [label="", style=invis, width=0] 0 -> 1 1 [label="0"] 1 -> 1 [label="0"] @@ -85,7 +89,8 @@ digraph G { 3 -> 1 [label="1\n{0,1}"] } digraph G { - 0 [label="", style=invis, height=0] + rankdir=LR + 0 [label="", style=invis, width=0] 0 -> 1 1 [label="0"] 1 -> 2 [label="p1"] @@ -97,7 +102,8 @@ digraph G { 3 -> 2 [label="!p1 | p2"] } digraph G { - 0 [label="", style=invis, height=0] + rankdir=LR + 0 [label="", style=invis, width=0] 0 -> 1 1 [label="0"] 1 -> 2 [label="p1"] @@ -111,4 +117,3 @@ digraph G { EOF diff stdout expected - diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index c960cde72..77dd713ac 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -21,6 +21,7 @@ // along with this program. If not, see . #include +#include #include "tgba/tgbagraph.hh" #include "dotty.hh" #include "dottydec.hh" @@ -38,19 +39,53 @@ namespace spot { public: dotty_bfs(std::ostream& os, const_tgba_ptr a, bool mark_accepting_states, - dotty_decorator* dd) + const char* options, dotty_decorator* dd) : tgba_reachable_iterator_breadth_first(a), os_(os), mark_accepting_states_(mark_accepting_states), dd_(dd), sba_(std::dynamic_pointer_cast(a)) { + if (options) + while (char c = *options++) + switch (c) + { + case 'c': + opt_circles = true; + break; + case 'h': + opt_horizontal = true; + break; + case 'n': + opt_name = true; + break; + case 'N': + opt_name = false; + break; + case 'v': + opt_horizontal = false; + break; + case 't': + mark_accepting_states_ = false; + break; + default: + throw std::runtime_error + (std::string("unknown option for dotty(): ") + c); + } } void start() { - os_ << ("digraph G {\n" - " 0 [label=\"\", style=invis, height=0]\n" - " 0 -> 1\n"); + os_ << "digraph G {\n"; + if (opt_horizontal) + os_ << " rankdir=LR\n"; + if (opt_name) + if (auto n = aut_->get_named_prop("automaton-name")) + escape_str(os_ << " label=\"", *n) << "\"\n labelloc=\"t\"\n"; + if (opt_circles) + os_ << " node [shape=\"circle\"]\n"; + os_ << " 0 [label=\"\", style=invis, "; + os_ << (opt_horizontal ? "width" : "height"); + os_ << "=0]\n 0 -> 1\n"; } void @@ -96,12 +131,12 @@ namespace spot std::string label = bdd_format_formula(aut_->get_dict(), si->current_condition()); - auto a = si->current_acceptance_conditions(); - if (a) - { - label += "\n"; - label += aut_->acc().format(a); - } + if (!mark_accepting_states_) + if (auto a = si->current_acceptance_conditions()) + { + label += "\n"; + label += aut_->acc().format(a); + } std::string s = aut_->transition_annotation(si); if (!s.empty()) @@ -122,16 +157,20 @@ namespace spot bool mark_accepting_states_; dotty_decorator* dd_; const_tgba_digraph_ptr sba_; + bool opt_horizontal = true; + bool opt_name = true; + bool opt_circles = false; }; } std::ostream& dotty_reachable(std::ostream& os, const const_tgba_ptr& g, - bool assume_sba, dotty_decorator* dd) + bool assume_sba, const char* options, + dotty_decorator* dd) { if (!dd) dd = dotty_decorator::instance(); - dotty_bfs d(os, g, assume_sba || g->has_state_based_acc(), dd); + dotty_bfs d(os, g, assume_sba || g->has_state_based_acc(), options, dd); d.run(); return os; } diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index 3cc0daae3..48c38b10a 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -41,12 +41,18 @@ namespace spot /// ways. See \ref tgba_dotty "this page" for a list of available /// decorators. If no decorator is specified, the dotty_decorator /// is used. - /// labels the transitions are encoded in UTF-8. + /// + /// \param options an optional string of letters, each indicating a + /// different option. Presently the following options are + /// supported: 'v' for vertical output, 'h' for horizontal output, + /// 't' force transition-based acceptance, 'N' hide the name of the + /// automaton, 'n' shows the name, 'c' uses circle-shaped states. SPOT_API std::ostream& dotty_reachable(std::ostream& os, const const_tgba_ptr& g, bool assume_sba = false, - dotty_decorator* dd = 0); + const char* options = nullptr, + dotty_decorator* dd = nullptr); } #endif // SPOT_TGBAALGOS_DOTTY_HH diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test index 08ce1e20c..0013ad751 100755 --- a/src/tgbatest/det.test +++ b/src/tgbatest/det.test @@ -118,7 +118,8 @@ run 0 ../../bin/autfilt -q --are-isomorph ex.hoa out.hoa run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba cat >ex.tgba < 1 1 [label="0"] 1 -> 2 [label="1"] @@ -127,9 +128,9 @@ digraph G { 2 -> 3 [label="!a"] 2 -> 4 [label="!b"] 3 [label="3", peripheries=2] - 3 -> 3 [label="!a\n{0}"] + 3 -> 3 [label="!a"] 4 [label="4", peripheries=2] - 4 -> 4 [label="!b\n{0}"] + 4 -> 4 [label="!b"] } EOF diff out.tgba ex.tgba diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test index 9a4b382b6..43d80f1d1 100755 --- a/src/tgbatest/dstar.test +++ b/src/tgbatest/dstar.test @@ -60,7 +60,8 @@ run 0 ../ltl2tgba -XD dra.dstar | tee stdout cat >expected < 1 1 [label="0"] 1 -> 1 [label="a & !b"] @@ -80,13 +81,14 @@ run 0 ../ltl2tgba -XDD dra.dstar | tee stdout cat >expected < 1 1 [label="0"] 1 -> 1 [label="a & !b"] 1 -> 2 [label="b"] 2 [label="1", peripheries=2] - 2 -> 2 [label="1\n{0}"] + 2 -> 2 [label="1"] } EOF @@ -123,7 +125,8 @@ run 0 ../ltl2tgba -XDB dsa.dstar | tee stdout cat >expected < 1 1 [label="0"] 1 -> 2 [label="1"] @@ -211,7 +214,8 @@ run 0 ../ltl2tgba -XDD dra.dstar | tee stdout cat >expected < 1 1 [label="0"] 1 -> 2 [label="!a & !b"] @@ -222,15 +226,15 @@ digraph G { 2 -> 2 [label="!b"] 2 -> 4 [label="b"] 3 [label="2", peripheries=2] - 3 -> 2 [label="!a & !b\n{0}"] - 3 -> 3 [label="a & !b\n{0}"] - 3 -> 4 [label="!a & b\n{0}"] - 3 -> 5 [label="a & b\n{0}"] + 3 -> 2 [label="!a & !b"] + 3 -> 3 [label="a & !b"] + 3 -> 4 [label="!a & b"] + 3 -> 5 [label="a & b"] 4 [label="3", peripheries=2] - 4 -> 4 [label="1\n{0}"] + 4 -> 4 [label="1"] 5 [label="4", peripheries=2] - 5 -> 4 [label="!a\n{0}"] - 5 -> 5 [label="a\n{0}"] + 5 -> 4 [label="!a"] + 5 -> 5 [label="a"] } EOF @@ -256,7 +260,8 @@ run 0 ../ltl2tgba -XDD aut.dsa | tee stdout cat >expected< 1 1 [label="0"] 1 -> 1 [label="1"] diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index d305e4003..195a4aefa 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1808,7 +1808,8 @@ checked_main(int argc, char** argv) { spot::tgba_run_dotty_decorator deco(run); spot::dotty_reachable(std::cout, a, - assume_sba, &deco); + assume_sba, nullptr, + &deco); } else if (graph_run_tgba_opt) { diff --git a/src/tgbatest/monitor.test b/src/tgbatest/monitor.test index 5fdd082fc..712a58b5d 100755 --- a/src/tgbatest/monitor.test +++ b/src/tgbatest/monitor.test @@ -33,7 +33,8 @@ expect() expect ../../bin/ltl2tgba --monitor a < 1 1 [label="1", peripheries=2] 1 -> 2 [label="a"] diff --git a/src/tgbatest/neverclaimread.test b/src/tgbatest/neverclaimread.test index c42dd9aff..966bd9039 100755 --- a/src/tgbatest/neverclaimread.test +++ b/src/tgbatest/neverclaimread.test @@ -133,12 +133,13 @@ run 0 ../ltl2tgba -XN input > stdout cat >expected < 1 1 [label="0", peripheries=2] - 1 -> 2 [label="p1\n{0}"] + 1 -> 2 [label="p1"] 2 [label="1", peripheries=2] - 2 -> 2 [label="1\n{0}"] + 2 -> 2 [label="1"] } EOF @@ -324,13 +325,14 @@ EOF ../../bin/autfilt --dot stdout 2>stderr && exit 1 cat >expected < 1 1 [label="0"] 1 -> 2 [label="b"] 1 -> 1 [label="0"] 2 [label="1", peripheries=2] - 2 -> 2 [label="1\n{0}"] + 2 -> 2 [label="1"] } EOF diff stdout expected diff --git a/src/tgbatest/tgbaread.test b/src/tgbatest/tgbaread.test index 6b43ca312..62bd995d9 100755 --- a/src/tgbatest/tgbaread.test +++ b/src/tgbatest/tgbaread.test @@ -36,7 +36,8 @@ run 0 ../tgbaread input > stdout cat >expected < 1 1 [label="0"] 1 -> 2 [label="a & !b\n{0,1}"] diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 642e80b57..fd09c07f0 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -292,7 +292,7 @@ def render_automaton(automaton, dont_run_dot, issba, deco = None): elif hasattr(automaton, 'get_ta'): # TGTA spot.dotty_reachable(dotsrc, automaton.get_ta()) else: # TGBA - spot.dotty_reachable(dotsrc, automaton, issba, deco) + spot.dotty_reachable(dotsrc, automaton, issba, "N", deco) render_dot_maybe(dotsrc.str(), dont_run_dot) def render_formula(f):