From ff83e92db4bdd90ffe738c07300416b0face8e96 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 5 Aug 2014 19:43:30 +0200
Subject: [PATCH] tgba_digraph: Fix handling of initial state.

* src/tgba/tgbagraph.hh: Store the number of the initial state, not a
pointer to it, because if the state vector is reallocated due to some
later calls to new_state(), this pointer will be invalid.
* src/graphtest/tgbagraph.cc, src/graphtest/tgbagraph.test: Test
for this.
---
 src/graphtest/tgbagraph.cc   |  5 +++++
 src/graphtest/tgbagraph.test | 12 ++++++++++++
 src/tgba/tgbagraph.hh        | 38 +++++++++++++++++++-----------------
 3 files changed, 37 insertions(+), 18 deletions(-)

diff --git a/src/graphtest/tgbagraph.cc b/src/graphtest/tgbagraph.cc
index a3dfb0bf4..694b50ab9 100644
--- a/src/graphtest/tgbagraph.cc
+++ b/src/graphtest/tgbagraph.cc
@@ -82,6 +82,11 @@ void f1()
 
   std::cerr << tg.num_transitions() << '\n';
   assert(tg.num_transitions() == 5);
+
+  // Add enough states so that the state vector is reallocated.
+  for (unsigned i = 0; i < 100; ++i)
+    tg.new_state();
+  spot::dotty_reachable(std::cout, &tg);
 }
 
 int main()
diff --git a/src/graphtest/tgbagraph.test b/src/graphtest/tgbagraph.test
index ea8f4ef8d..5276045fb 100755
--- a/src/graphtest/tgbagraph.test
+++ b/src/graphtest/tgbagraph.test
@@ -96,6 +96,18 @@ digraph G {
   3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"]
   3 -> 2 [label="!p1 | p2\n"]
 }
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="0"]
+  1 -> 2 [label="p1\n"]
+  1 -> 3 [label="p2\n{Acc[p2]}"]
+  2 [label="1"]
+  2 -> 3 [label="p1 & p2\n{Acc[p1]}"]
+  3 [label="2"]
+  3 -> 1 [label="1\n{Acc[p2], Acc[p1]}"]
+  3 -> 2 [label="!p1 | p2\n"]
+}
 EOF
 
 diff stdout expected
diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh
index 768330796..e5cce86c4 100644
--- a/src/tgba/tgbagraph.hh
+++ b/src/tgba/tgbagraph.hh
@@ -33,6 +33,11 @@ namespace spot
   struct SPOT_API tgba_graph_state: public spot::state
   {
   public:
+    tgba_graph_state():
+      spot::state()
+    {
+    }
+
     virtual ~tgba_graph_state() noexcept
     {
     }
@@ -158,14 +163,14 @@ namespace spot
     bdd_dict* dict_;
     bdd all_acceptance_conditions_;
     bdd neg_acceptance_conditions_;
-    mutable const tgba_graph_state* init_;
+    mutable unsigned init_number_;
 
   public:
     tgba_digraph(bdd_dict* dict)
       : dict_(dict),
 	all_acceptance_conditions_(bddfalse),
 	neg_acceptance_conditions_(bddtrue),
-	init_(nullptr)
+	init_number_(0)
     {
     }
 
@@ -223,31 +228,28 @@ namespace spot
 
     void set_init_state(graph_t::state s)
     {
-      init_ = &g_.state_data(s);
+      assert(s < num_states());
+      init_number_ = s;
     }
 
     void set_init_state(const state* s)
     {
-      init_ = down_cast<const tgba_graph_state*>(s);
-      assert(init_);
-    }
-
-    virtual tgba_graph_state* get_init_state() const
-    {
-      if (num_states() == 0)
-	const_cast<graph_t&>(g_).new_state();
-      if (!init_)
-	init_ = &g_.state_data(0);
-      return const_cast<tgba_graph_state*>(init_);
+      set_init_state(state_number(s));
     }
 
     virtual graph_t::state get_init_state_number() const
     {
       if (num_states() == 0)
 	const_cast<graph_t&>(g_).new_state();
-      if (!init_)
-	return 0;
-      return state_number(init_);
+      return init_number_;
+    }
+
+    // FIXME: The return type ought to be const.
+    virtual tgba_graph_state* get_init_state() const
+    {
+      if (num_states() == 0)
+	const_cast<graph_t&>(g_).new_state();
+      return const_cast<tgba_graph_state*>(state_from_number(init_number_));
     }
 
     virtual tgba_succ_iterator*
@@ -276,7 +278,7 @@ namespace spot
       return s - &g_.state_storage(0);
     }
 
-    const state*
+    const tgba_graph_state*
     state_from_number(graph_t::state n) const
     {
       return &g_.state_data(n);