From ae50155297f8fdc95354a48b38787a8598d01ddc Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 23 Jan 2015 17:29:35 +0100
Subject: [PATCH] dotty: output label for unreachable state even if SCCs are
 shown

* src/tgbaalgos/dotty.cc: Fix output of unreachable states.
* src/tgbatest/readsave.test: Add test.
---
 src/tgbaalgos/dotty.cc     |  2 +-
 src/tgbatest/readsave.test | 54 ++++++++++++++++++++++++++++++++++++--
 2 files changed, 53 insertions(+), 3 deletions(-)

diff --git a/src/tgbaalgos/dotty.cc b/src/tgbaalgos/dotty.cc
index ae38516c4..458805c3d 100644
--- a/src/tgbaalgos/dotty.cc
+++ b/src/tgbaalgos/dotty.cc
@@ -154,7 +154,7 @@ namespace spot
 	unsigned ns = aut_->num_states();
 	for (unsigned n = 0; n < ns; ++n)
 	  {
-	    if (!si)
+	    if (!si || !si->reachable_state(n))
 	      process_state(n);
 	    for (auto& t: aut_->out(n))
 	      process_link(t);
diff --git a/src/tgbatest/readsave.test b/src/tgbatest/readsave.test
index 80985eb98..0baa2e398 100755
--- a/src/tgbatest/readsave.test
+++ b/src/tgbatest/readsave.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche
+# et Développement 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
 # et Marie Curie.
@@ -284,3 +284,53 @@ cat >expected <<EOF
 "!b & X(b & GFa)","!b; cycle{a & b}"
 EOF
 diff output expected
+
+
+$autfilt --dot=vcsn >output <<EOF
+HOA: v1
+States: 4
+Start: 2
+Start: 3
+AP: 2 "a" "b"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc
+--BODY--
+State: 0 {0}
+[1] 0
+State: 1 {0}
+[0] 1
+State: 2
+[1] 0
+State: 3
+[0] 1
+--END--
+EOF
+
+cat >expected <<EOF
+digraph G {
+  node [shape="circle"]
+  I [label="", style=invis, height=0]
+  I -> 3
+  subgraph cluster_0 {
+  label=""
+  1 [label="1"]
+  }
+  subgraph cluster_1 {
+  label=""
+  0 [label="0"]
+  }
+  subgraph cluster_2 {
+  label=""
+  3 [label="3"]
+  }
+  0 -> 0 [label="b\n{0}"]
+  1 -> 1 [label="a\n{0}"]
+  2 [label="2"]
+  2 -> 0 [label="b"]
+  3 -> 1 [label="a"]
+  3 -> 0 [label="b"]
+}
+EOF
+
+diff output expected