From 5b3034b605c709ec5eca4d7095b97860cdff3e76 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Feb 2015 11:24:29 +0100 Subject: [PATCH] dot: add an option to display the acceptance * src/tgbaalgos/dotty.cc: Display the acceptance if "a" is used. * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc, src/tgbaalgos/dotty.hh: Document it. * src/tgbatest/readsave.test: Test it. --- src/bin/common_aoutput.cc | 8 ++++---- src/bin/dstar2tgba.cc | 8 ++++---- src/tgbaalgos/dotty.cc | 25 ++++++++++++++++++++---- src/tgbaalgos/dotty.hh | 3 ++- src/tgbatest/readsave.test | 40 +++++++++++++++++++++++++++++++++++--- 5 files changed, 68 insertions(+), 16 deletions(-) diff --git a/src/bin/common_aoutput.cc b/src/bin/common_aoutput.cc index 91b0b15d0..dc83891ce 100644 --- a/src/bin/common_aoutput.cc +++ b/src/bin/common_aoutput.cc @@ -50,10 +50,10 @@ static const argp_option options[] = /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, { "dot", OPT_DOT, "c|h|n|N|s|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, (s) with SCCs, " - "(t) always transition-based acceptance.", 0 }, + "GraphViz's format (default). Add letters for " + "(a) acceptance display, (c) circular nodes, (h) horizontal layout, " + "(v) vertical layout, (n) with name, (N) without name, (s) with SCCs, " + "(t) force 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, " diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index 2550727b8..8ee0eba09 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -72,10 +72,10 @@ static const argp_option options[] = /**************************************************/ { 0, 0, 0, 0, "Output format:", 3 }, { "dot", OPT_DOT, "c|h|n|N|s|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, (s) with SCCs, " - "(t) always transition-based acceptance.", 0 }, + "GraphViz's format (default). Add letters for (a) acceptance display, " + "(c) circular nodes, (h) horizontal layout, (v) vertical layout, " + "(n) with name, (N) without name, (s) with SCCs, " + "(t) force 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, " diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc index 927dc7b72..12788bc9d 100644 --- a/src/tgbaalgos/dotty.cc +++ b/src/tgbaalgos/dotty.cc @@ -42,10 +42,12 @@ namespace spot bool opt_horizontal_ = true; bool opt_name_ = false; bool opt_circles_ = false; + bool opt_show_acc_ = false; bool mark_states_ = false; bool opt_scc_ = false; const_tgba_digraph_ptr aut_; std::vector* sn_; + std::string* name_ = nullptr; public: dotty_output(std::ostream& os, const char* options) @@ -55,6 +57,9 @@ namespace spot while (char c = *options++) switch (c) { + case 'a': + opt_show_acc_ = true; + break; case 'c': opt_circles_ = true; break; @@ -88,9 +93,19 @@ namespace spot 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 (name_ || opt_show_acc_) + { + os_ << " label=\""; + if (name_) + { + escape_str(os_, *name_); + if (opt_show_acc_) + os_ << "\\n"; + } + if (opt_show_acc_) + os_ << aut_->get_acceptance(); + os_ << "\"\n labelloc=\"t\"\n"; + } if (opt_circles_) os_ << " node [shape=\"circle\"]\n"; os_ << " I [label=\"\", style=invis, "; @@ -137,6 +152,8 @@ namespace spot { aut_ = aut; sn_ = aut->get_named_prop>("state-names"); + if (opt_name_) + name_ = aut_->get_named_prop("automaton-name"); mark_states_ = !opt_force_acc_trans_ && aut_->is_sba(); auto si = std::unique_ptr(opt_scc_ ? new scc_info(aut) : nullptr); @@ -147,7 +164,7 @@ namespace spot for (unsigned i = 0; i < sccs; ++i) { os_ << " subgraph cluster_" << i << " {\n"; - if (opt_name_) + if (name_ || opt_show_acc_) // Reset the label, otherwise the graph label would // be inherited by the cluster. os_ << " label=\"\"\n"; diff --git a/src/tgbaalgos/dotty.hh b/src/tgbaalgos/dotty.hh index 20330fe91..2f7c85fe3 100644 --- a/src/tgbaalgos/dotty.hh +++ b/src/tgbaalgos/dotty.hh @@ -39,7 +39,8 @@ namespace spot /// 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. + /// automaton, 'n' shows the name, 'c' uses circle-shaped states, + /// 'a' shows the acceptance. SPOT_API std::ostream& dotty_reachable(std::ostream& os, const const_tgba_ptr& g, diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test index ff5766f02..98609e465 100755 --- a/src/tgbatest/readsave.test +++ b/src/tgbatest/readsave.test @@ -314,15 +314,12 @@ digraph G { I [label="", style=invis, height=0] I -> 3 subgraph cluster_0 { - label="" 1 [label="s1", peripheries=2] } subgraph cluster_1 { - label="" 0 [label="s0", peripheries=2] } subgraph cluster_2 { - label="" 3 [label="s3"] } 0 -> 0 [label="b"] @@ -337,3 +334,40 @@ EOF diff output expected test 1 = `$autfilt -H input --complete | $autfilt --is-complete --count` + + +$ltl2tgba --dot=a 'GFa & GFb' >output +cat output +cat >expected < 0 + 0 [label="0"] + 0 -> 0 [label="a & b\n{0,1}"] + 0 -> 0 [label="!a & !b"] + 0 -> 0 [label="!a & b\n{1}"] + 0 -> 0 [label="a & !b\n{0}"] +} +EOF +diff output expected + +$ltl2tgba --dot=an 'GFa & GFb' >output +cat output +cat >expected < 0 + 0 [label="0"] + 0 -> 0 [label="a & b\n{0,1}"] + 0 -> 0 [label="!a & !b"] + 0 -> 0 [label="!a & b\n{1}"] + 0 -> 0 [label="a & !b\n{0}"] +} +EOF +diff output expected