From a89b9d36787695bf74e64fb11b601ad42de720da Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 21 Jan 2015 23:28:35 +0100
Subject: [PATCH] hoa: do not add a fake initial state when possible

* src/hoaparse/hoaparse.yy: If we have multiple initial states, but
one of them has no incoming edge, use this state instead of the fake
initial state we normally add.
* src/tgbatest/hoaparse.test: Add test case.
---
 src/hoaparse/hoaparse.yy   | 28 ++++++++++++----
 src/tgbatest/hoaparse.test | 65 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 87 insertions(+), 6 deletions(-)

diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy
index 503416623..d35d5be6b 100644
--- a/src/hoaparse/hoaparse.yy
+++ b/src/hoaparse/hoaparse.yy
@@ -1357,13 +1357,29 @@ static void fix_initial_state(result_& r)
     }
   else
     {
-      // Multiple initial states.  Add a fake one.
+      // Multiple initial states.  We might need to add a fake one,
+      // unless one of the actual initial state has no incoming edge.
       auto& aut = r.h->aut;
-      unsigned i = aut->new_state();
-      aut->set_init_state(i);
-      for (auto p : start)
-	for (auto& t: aut->out(p))
-	  aut->new_transition(i, t.dst, t.cond);
+      std::vector<unsigned> has_incoming(aut->num_states(), 0);
+      for (auto& t: aut->transitions())
+	has_incoming[t.dst] = true;
+
+      bool found = false;
+      unsigned init = 0;
+      for (auto p: start)
+	if (!has_incoming[p])
+	  {
+	    init = p;
+	    found = true;
+	  }
+      if (!found)
+	// We do need a fake initial state
+	init = aut->new_state();
+      aut->set_init_state(init);
+      for (auto p: start)
+	if (p != init)
+	  for (auto& t: aut->out(p))
+	    aut->new_transition(init, t.dst, t.cond);
     }
 }
 
diff --git a/src/tgbatest/hoaparse.test b/src/tgbatest/hoaparse.test
index 7810dbead..6f63e11f7 100755
--- a/src/tgbatest/hoaparse.test
+++ b/src/tgbatest/hoaparse.test
@@ -1218,3 +1218,68 @@ State: 5 {0}
 [t] 5
 --END--
 EOF
+
+# Another example from ltl3ba
+# Here we make sure that we do not always need to create a fake
+# initial state when multiple initial states are used.
+cat >input <<EOF
+HOA: v1
+tool: "ltl3ba" "1.1.0 - working copy"
+name: "TGBA for GFa && GF(b&&c) && GF(d||e) || x"
+States: 3
+Start: 0
+Start: 2
+acc-name: generalized-Buchi 3
+Acceptance: 3 Inf(0) & Inf(1) & Inf(2)
+AP: 6 "a" "b" "c" "d" "e" "x"
+properties: trans-labels explicit-labels trans-acc no-univ-branch
+--BODY--
+State: 0 "(x)"
+ [(5)] 1 {0 1 2}
+State: 1 "t"
+ [t] 1 {0 1 2}
+State: 2 "G((F(a) && F((b) && (c))) && F((d) || (e)))"
+ [t] 2
+ [(0)] 2 {0}
+ [(1 & 2)] 2 {1}
+ [(0 & 1 & 2)] 2 {0 1}
+ [(!3 & 4) | (3)] 2 {2}
+ [(0 & !3 & 4) | (0 & 3)] 2 {0 2}
+ [(1 & 2 & !3 & 4) | (1 & 2 & 3)] 2 {1 2}
+ [(0 & 1 & 2 & !3 & 4) | (0 & 1 & 2 & 3)] 2 {0 1 2}
+--END--
+EOF
+
+expectok input <<EOF
+HOA: v1
+name: "TGBA for GFa && GF(b&&c) && GF(d||e) || x"
+States: 3
+Start: 0
+AP: 6 "a" "b" "c" "d" "e" "x"
+acc-name: generalized-Buchi 3
+Acceptance: 3 Inf(0)&Inf(1)&Inf(2)
+properties: trans-labels explicit-labels trans-acc complete
+--BODY--
+State: 0
+[5] 1 {0 1 2}
+[t] 2
+[0] 2
+[1&2] 2
+[0&1&2] 2
+[3 | 4] 2
+[0&3 | 0&4] 2
+[1&2&3 | 1&2&4] 2
+[0&1&2&3 | 0&1&2&4] 2
+State: 1
+[t] 1 {0 1 2}
+State: 2
+[t] 2
+[0] 2 {0}
+[1&2] 2 {1}
+[0&1&2] 2 {0 1}
+[3 | 4] 2 {2}
+[0&3 | 0&4] 2 {0 2}
+[1&2&3 | 1&2&4] 2 {1 2}
+[0&1&2&3 | 0&1&2&4] 2 {0 1 2}
+--END--
+EOF