dotty: switch to horizontal output and add options

* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Add an options
parameter.
* src/bin/randaut.cc, src/bin/autfilt.cc, src/bin/dstar2tgba.cc,
src/bin/ltl2tgba.cc, wrap/python/ajax/spot.in: Use it.
* src/tgbatest/det.test, src/tgbatest/dstar.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/monitor.test,
src/tgbatest/neverclaimread.test, src/tgbatest/tgbaread.test,
src/graphtest/tgbagraph.test: Adjust
because automata are now output horizontally.
* NEWS: Mention the change.

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.

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<std::vector<tr_t>> 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<int>::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);

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);

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);

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<std::vector<tr_t>> 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);

src/graphtest/tgbagraph.test

@@ -34,7 +34,8 @@ run 0 ../tgbagraph | tee stdout
 
 cat >expected <<EOF
 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"]
@@ -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
-

src/tgbaalgos/dotty.cc

@@ -21,6 +21,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include <ostream>
+#include <stdexcept>
 #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<const tgba_digraph>(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"
+	os_ << "digraph G {\n";
-		"  0 [label=\"\", style=invis, height=0]\n"
+	if (opt_horizontal)
-		"  0 -> 1\n");
+	  os_ << "  rankdir=LR\n";
+	if (opt_name)
+	  if (auto n = aut_->get_named_prop<std::string>("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,8 +131,8 @@ namespace spot
 	std::string label =
 	  bdd_format_formula(aut_->get_dict(),
 			     si->current_condition());
-	auto a = si->current_acceptance_conditions();
+	if (!mark_accepting_states_)
-	if (a)
+	  if (auto a = si->current_acceptance_conditions())
 	    {
 	      label += "\n";
 	      label += aut_->acc().format(a);
@@ -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;
   }

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

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 <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 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

src/tgbatest/dstar.test

@@ -60,7 +60,8 @@ run 0 ../ltl2tgba -XD dra.dstar | tee stdout
 
 cat >expected <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 1
   1 [label="0"]
   1 -> 1 [label="a & !b"]
@@ -80,13 +81,14 @@ run 0 ../ltl2tgba -XDD dra.dstar | tee stdout
 
 cat >expected <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 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 <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 1
   1 [label="0"]
   1 -> 2 [label="1"]
@@ -211,7 +214,8 @@ run 0 ../ltl2tgba -XDD dra.dstar | tee stdout
 
 cat >expected <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 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 -> 2 [label="!a & !b"]
-  3 -> 3 [label="a & !b\n{0}"]
+  3 -> 3 [label="a & !b"]
-  3 -> 4 [label="!a & b\n{0}"]
+  3 -> 4 [label="!a & b"]
-  3 -> 5 [label="a & b\n{0}"]
+  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 -> 4 [label="!a"]
-  5 -> 5 [label="a\n{0}"]
+  5 -> 5 [label="a"]
 }
 EOF
 
@@ -256,7 +260,8 @@ run 0 ../ltl2tgba -XDD aut.dsa | tee stdout
 
 cat >expected<<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 1
   1 [label="0"]
   1 -> 1 [label="1"]

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)
 				{

src/tgbatest/monitor.test

@@ -33,7 +33,8 @@ expect()
 
 expect ../../bin/ltl2tgba --monitor a <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 1
   1 [label="1", peripheries=2]
   1 -> 2 [label="a"]

src/tgbatest/neverclaimread.test

@@ -133,12 +133,13 @@ run 0 ../ltl2tgba -XN input > stdout
 
 cat >expected <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 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 <input >stdout 2>stderr && exit 1
 cat >expected <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 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

src/tgbatest/tgbaread.test

@@ -36,7 +36,8 @@ run 0 ../tgbaread input > stdout
 
 cat >expected <<EOF
 digraph G {
-  0 [label="", style=invis, height=0]
+  rankdir=LR
+  0 [label="", style=invis, width=0]
   0 -> 1
   1 [label="0"]
   1 -> 2 [label="a & !b\n{0,1}"]

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):