dot: add option "k"

Fixes #134.

* spot/twaalgos/dot.cc: Implement it.
* bin/common_aoutput.cc, spot/twaalgos/dot.hh, NEWS: Document it.
* tests/core/readsave.test, tests/python/ltsmin.ipynb: Test it.

NEWS

@@ -19,6 +19,10 @@ New in spot 1.99.7a (not yet released)
     with
        ltl2tgba -D 'Ga | Gb | Gc' -d
 
+  * print_dot() now has option "k" to use state-based labels when
+    possible.  This is similar to the "k" option already supported
+    by print_hoa(), and is useful when printing Kripke structures.
+
   Python:
 
   * The ltsmin interface has been binded in Python.  See

bin/common_aoutput.cc

@@ -80,7 +80,7 @@ static const argp_option options[] =
   {
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Output format:", 3 },
-    { "dot", 'd', "1|a|b|B|c|e|f(FONT)|h|n|N|o|r|R|s|t|v|+INT|<INT",
+    { "dot", 'd', "1|a|b|B|c|e|f(FONT)|h|k|n|N|o|r|R|s|t|v|+INT|<INT",
       OPTION_ARG_OPTIONAL,
       "GraphViz's format.  Add letters for "
       "(1) force numbered states, "
@@ -88,11 +88,13 @@ static const argp_option options[] =
       "(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, "
+      "(k) use state labels when possible, "
+      "(n) with name, (N) without name, "
       "(o) ordered transitions, "
       "(r) rainbow colors for acceptance sets, "
       "(R) color acceptance sets by Inf/Fin, (s) with SCCs, "
       "(t) force transition-based acceptance, "
+      "(v) vertical layout, "
       "(+INT) add INT to all set numbers, "
       "(<INT) display at most INT states", 0 },
     { "hoaf", 'H', "i|l|m|s|t|v", OPTION_ARG_OPTIONAL,

spot/twaalgos/dot.cc

@@ -55,6 +55,7 @@ namespace spot
       bool mark_states_ = false;
       bool opt_scc_ = false;
       bool opt_html_labels_ = false;
+      bool opt_state_labels_ = false;
       const_twa_graph_ptr aut_;
       std::vector<std::string>* sn_ = nullptr;
       std::vector<std::pair<unsigned, unsigned>>* sprod_ = nullptr;
@@ -192,6 +193,9 @@ namespace spot
 	    case 'h':
 	      opt_horizontal_ = true;
 	      break;
+	    case 'k':
+	      opt_state_labels_ = true;
+	      break;
 	    case 'n':
 	      opt_name_ = true;
 	      break;
@@ -319,6 +323,21 @@ namespace spot
 	  os_ << '}';
       }
 
+      std::string
+      state_label(unsigned s) const
+      {
+	bdd label = bddfalse;
+	for (auto& t: aut_->out(s))
+	  {
+	    label = t.cond;
+	    break;
+	  }
+	if (label == bddfalse
+	    && incomplete_ && incomplete_->find(s) != incomplete_->end())
+	  return "...";
+	return bdd_format_formula(aut_->get_dict(), label);
+      }
+
       void
       start()
       {
@@ -440,6 +459,8 @@ namespace spot
 		    os_ << "\\n";
 		    output_set(acc);
 		  }
+		if (opt_state_labels_)
+		  escape_str(os_ << "\\n", state_label(s));
 		os_ << '"';
 	      }
 	    else
@@ -456,6 +477,8 @@ namespace spot
 		    os_ << "<br/>";
 		    output_html_set(acc);
 		  }
+		if (opt_state_labels_)
+		  escape_html(os_ << "<br/>", state_label(s));
 		os_ << '>';
 	      }
 	    os_ << "]\n";
@@ -470,6 +493,8 @@ namespace spot
 	      os_ << (*sprod_)[s].first << ',' << (*sprod_)[s].second;
 	    else
 	      os_ << s;
+	    if (opt_state_labels_)
+	      escape_str(os_ << "\\n", state_label(s));
 	    os_ << '"';
 	    // Use state_acc_sets(), not state_is_accepting() because
 	    // on co-Büchi automata we want to mark the rejecting
@@ -486,8 +511,10 @@ namespace spot
       void
       process_link(const twa_graph::edge_storage_t& t, int number)
       {
-	std::string label = bdd_format_formula(aut_->get_dict(), t.cond);
 	os_ << "  " << t.src << " -> " << t.dst;
+	std::string label;
+	if (!opt_state_labels_)
+	  label = bdd_format_formula(aut_->get_dict(), t.cond);
 	if (!opt_html_labels_)
 	  {
 	    os_ << " [label=\"";
@@ -495,6 +522,7 @@ namespace spot
 	    if (!mark_states_)
 	      if (auto a = t.acc)
 		{
+		  if (!opt_state_labels_)
 		    os_ << "\\n";
 		  output_set(a);
 		}
@@ -507,6 +535,7 @@ namespace spot
 	    if (!mark_states_)
 	      if (auto a = t.acc)
 		{
+		  if (!opt_state_labels_)
 		    os_ << "<br/>";
 		  output_html_set(a);
 		}
@@ -533,6 +562,27 @@ namespace spot
 		  sprod_ = nullptr;
 	      }
 	  }
+	if (opt_state_labels_)
+	  {
+	    // Verify that we can use state labels for this automaton.
+	    unsigned n = aut->num_states();
+	    for (unsigned s = 0; s < n; ++s)
+	      {
+		bool first = true;
+		bdd cond = bddfalse;
+		for (auto& t: aut->out(s))
+		  if (first)
+		    {
+		      cond = t.cond;
+		      first = false;
+		    }
+		  else if (t.cond != cond)
+		    {
+		      opt_state_labels_ = false;
+		      break;
+		    }
+	      }
+	  }
 	incomplete_ =
 	  aut->get_named_prop<std::set<unsigned>>("incomplete-states");
 	if (opt_name_)
@@ -541,11 +591,12 @@ namespace spot
 			&& aut_->prop_state_acc().is_true());
 	if (opt_shape_ == ShapeAuto)
 	  {
-	    if (sn_ || sprod_ || aut->num_states() > 100)
+	    if (sn_ || sprod_ || aut->num_states() > 100 || opt_state_labels_)
 	      {
 		opt_shape_ = ShapeEllipse;
 		// If all state names are short, prefer circles.
-		if (sn_ && std::all_of(sn_->begin(), sn_->end(),
+		if (!opt_state_labels_ &&
+		    sn_ && std::all_of(sn_->begin(), sn_->end(),
 				       [](const std::string& s)
 				       { return s.size() <= 2; }))
 		  opt_shape_ = ShapeCircle;

spot/twaalgos/dot.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
+// Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
 // et Developpement 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
@@ -39,7 +39,7 @@ namespace spot
   /// 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,
-  /// 'a' shows the acceptance.
+  /// 'a' shows the acceptance, 'k' uses state-based labels if possible.
   SPOT_API std::ostream&
   print_dot(std::ostream& os,
 		  const const_twa_ptr& g,

tests/core/readsave.test

@@ -344,7 +344,8 @@ test 1 = `autfilt -H input --complete | autfilt --is-complete --count`
 
 
 # The SPOT_DEFAULT_FORMAT envvar should be ignored if --dot is given.
-SPOT_DEFAULT_FORMAT=hoa ltl2tgba --dot=a 'GFa & GFb' >output
+# --dot=k should be ignored when not applicable.
+SPOT_DEFAULT_FORMAT=hoa ltl2tgba --dot=ak 'GFa & GFb' >output
 cat output
 cat >expected <<EOF
 digraph G {
@@ -859,6 +860,49 @@ EOF
 
 diff output6 expect6
 
+run 0 autfilt -dk input6 >output6d
+cat >expect6d <<EOF
+digraph G {
+  rankdir=LR
+  I [label="", style=invis, width=0]
+  I -> 1
+  0 [label="0\nb"]
+  0 -> 2 [label=""]
+  0 -> 1 [label=""]
+  0 -> 1 [label=""]
+  1 [label="1\na"]
+  1 -> 0 [label=""]
+  1 -> 1 [label=""]
+  2 [label="2\na", peripheries=2]
+  2 -> 2 [label=""]
+  2 -> 0 [label=""]
+  2 -> 1 [label=""]
+}
+EOF
+diff output6d expect6d
+
+run 0 autfilt -dbark input6 >output6d2
+cat >expect6d2 <<EOF
+digraph G {
+  rankdir=LR
+  label=<Inf(<font color="#5DA5DA">⓿</font>)>
+  labelloc="t"
+  I [label="", style=invis, width=0]
+  I -> 1
+  0 [label=<0<br/>b>]
+  0 -> 2 [label=<>]
+  0 -> 1 [label=<>]
+  0 -> 1 [label=<>]
+  1 [label=<1<br/>a>]
+  1 -> 0 [label=<>]
+  1 -> 1 [label=<>]
+  2 [label=<2<br/><font color="#5DA5DA">⓿</font><br/>a>]
+  2 -> 2 [label=<>]
+  2 -> 0 [label=<>]
+  2 -> 1 [label=<>]
+}
+EOF
+diff output6d2 expect6d2
 
 cat >input7 <<EOF
 HOA: v1