From 80ce0e21294fcd9bc542049e77a01f1093278304 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 2 Dec 2014 20:14:57 +0100
Subject: [PATCH] satminimization: do not assume the initial state is 0

* src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc: Here.
---
 src/tgbaalgos/dtbasat.cc  |  9 ++++++---
 src/tgbaalgos/dtgbasat.cc | 11 ++++++-----
 2 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc
index 4339bf396..f4a1ccaf2 100644
--- a/src/tgbaalgos/dtbasat.cc
+++ b/src/tgbaalgos/dtbasat.cc
@@ -395,9 +395,12 @@ namespace spot
 	}
 
       dout << "(2) the initial state is reachable\n";
-      dout << state_pair(0, 0) << '\n';
-      out << d.prodid[state_pair(0, 0)] << " 0\n";
-      ++nclauses;
+      {
+	unsigned init = ref->get_init_state_number();
+	dout << state_pair(0, init) << '\n';
+	out << d.prodid[state_pair(0, init)] << " 0\n";
+	++nclauses;
+      }
 
       for (std::map<state_pair, int>::const_iterator pit = d.prodid.begin();
 	   pit != d.prodid.end(); ++pit)
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index 0b9b6dbeb..805569feb 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -527,9 +527,12 @@ namespace spot
 	}
 
       dout << "(9) the initial state is reachable\n";
-      dout << path(0, 0) << '\n';
-      out << d.pathid[path(0, 0)] << " 0\n";
-      ++nclauses;
+      {
+	unsigned init = ref->get_init_state_number();
+	dout << path(0, init) << '\n';
+	out << d.pathid[path(0, init)] << " 0\n";
+	++nclauses;
+      }
 
       for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
 	for (unsigned q1p = 0; q1p < ref_size; ++q1p)
@@ -732,11 +735,9 @@ namespace spot
 						transition_acc
 						  ta(q2, l,
 						     d.cacc.mark(m), q3);
-						int tai = d.transaccid[ta];
 						const char* not_ = "¬";
 						if (d.cacc.has(biga_, m))
 						  not_ = "";
-						out << tai << ' ';
 						out <<  " ∧ " << not_
 						    << ta << "FC";
 					      }