From 2e356aed1da71139fb00f62be5bc0d40b48ab794 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 4 Jan 2015 12:38:07 +0100
Subject: [PATCH] dotty: fix output of name and detection of state-based
 acceptance

* src/tgbaalgos/dotty.cc: Do not output name by default.  Display
accepting states by default no acceptance set are used.
Avoid copying the automaton when possible.
* src/tgbatest/dstar.test: Exercise --dot=t.
---
 src/tgbaalgos/dotty.cc  | 13 +++++++------
 src/tgbatest/dstar.test | 13 +++++--------
 2 files changed, 12 insertions(+), 14 deletions(-)

diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
index ea01f8302..48f66f9d3 100644
--- a/src/tgbaalgos/dotty.cc
+++ b/src/tgbaalgos/dotty.cc
@@ -41,7 +41,7 @@ namespace spot
       std::ostream& os_;
       bool opt_force_acc_trans_ = false;
       bool opt_horizontal_ = true;
-      bool opt_name_ = true;
+      bool opt_name_ = false;
       bool opt_circles_ = false;
       bool mark_states_ = false;
       bool opt_scc_ = false;
@@ -74,7 +74,7 @@ namespace spot
 		opt_horizontal_ = false;
 		break;
 	      case 't':
-		opt_force_acc_trans_ = false;
+		opt_force_acc_trans_ = true;
 		break;
 	      default:
 		throw std::runtime_error
@@ -132,7 +132,8 @@ namespace spot
       void print(const const_tgba_digraph_ptr& aut)
       {
 	aut_ = aut;
-	mark_states_ = !opt_force_acc_trans_ && aut_->has_state_based_acc();
+	mark_states_ = !opt_force_acc_trans_ &&
+	  (aut_->has_state_based_acc() || aut_->acc().num_sets() == 0);
 	auto si =
 	  std::unique_ptr<scc_info>(opt_scc_ ? new scc_info(aut) : nullptr);
 	start();
@@ -300,9 +301,9 @@ namespace spot
 	return os;
       }
     dotty_output d(os, options);
-    auto aut = make_tgba_digraph(g, tgba::prop_set::all());
-    if (assume_sba)
-      aut->prop_state_based_acc();
+    auto aut = std::dynamic_pointer_cast<const tgba_digraph>(g);
+    if (!aut)
+      aut = make_tgba_digraph(g, tgba::prop_set::all());
     d.print(aut);
     return os;
   }
diff --git a/src/tgbatest/dstar.test b/src/tgbatest/dstar.test
index d9c106396..01eac6de4 100755
--- a/src/tgbatest/dstar.test
+++ b/src/tgbatest/dstar.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -63,13 +63,13 @@ digraph G {
   rankdir=LR
   I [label="", style=invis, width=0]
   I -> 0
-  0 [label="0"]
+  0 [label="0", peripheries=2]
   0 -> 0 [label="a & !b"]
   0 -> 1 [label="!a & !b"]
   0 -> 2 [label="b"]
-  1 [label="1"]
+  1 [label="1", peripheries=2]
   1 -> 1 [label="1"]
-  2 [label="2"]
+  2 [label="2", peripheries=2]
   2 -> 2 [label="1"]
 }
 EOF
@@ -256,7 +256,7 @@ State: 0
 Acc-Sig:
 0
 EOF
-run 0 ../ltl2tgba -XDD aut.dsa | tee stdout
+run 0 ../../bin/dstar2tgba --dot=t aut.dsa | tee stdout
 
 cat >expected<<EOF
 digraph G {
@@ -265,9 +265,6 @@ digraph G {
   I -> 0
   0 [label="0"]
   0 -> 0 [label="1"]
-  0 -> 1 [label="1"]
-  1 [label="1"]
-  1 -> 1 [label="1"]
 }
 EOF