Make sure we only output one initial state in LBTT's output.

* src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument
to designate initial states.
(lbtt_reachable): Adjust calls to fill_todo.  Handle the
fake initial state accepting conditions specially.
* src/tgbaalgos/lbtt.hh: Update comments.

ChangeLog

@@ -1,5 +1,12 @@
 2003-07-09  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	Make sure we only output one initial state in LBTT's output.
+	* src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument
+	to designate initial states.
+	(lbtt_reachable): Adjust calls to fill_todo.  Handle the
+	fake initial state accepting conditions specially.
+	* src/tgbaalgos/lbtt.hh: Update comments.
+
 	* src/tgbaalgos/lbtt.cc (lbtt_reachable): Do not end transitions
 	guards with -1 in output.
 

src/tgbaalgos/lbtt.cc

@@ -119,13 +119,20 @@ namespace spot
   typedef std::pair<unsigned, unsigned> minmax_pair;
   typedef std::map<state*, minmax_pair, state_ptr_less_than> seen_map;
 
-  // Take a STATE from the source automata, and fill TODO with
+  // Take a STATE from the source automaton, and fill TODO with
   // the list of associated states to output.  Return the correponding
   // range in MMP.  Update SEEN, ACP_SEEN, and STATE_NUMBER.
+  //
+  // INIT must be set to true when registering the initial state.
+  // This allows us to create an additional state if required.  (LBTT
+  // supports only one initial state, so whenever the initial state
+  // of the source automaton has to be split, we need to create
+  // a supplementary state, to act as initial state for LBTT.)
   void
   fill_todo(todo_set& todo, seen_map& seen, acp_seen_map& acp_seen,
 	    state* state, const tgba& g,
-	    minmax_pair& mmp, unsigned& state_number)
+	    minmax_pair& mmp, unsigned& state_number,
+	    bool init)
   {
     typedef std::set<bdd, bdd_less_than> bdd_set;
 
@@ -145,6 +152,18 @@ namespace spot
       {
 	acc_seen.insert(si->current_accepting_conditions());
       }
+
+    // Order the creation of the supplementary initial state of needed.
+    // Use bddtrue as accepting condition because it cannot conflict
+    // with other (state, accepting cond) pairs in the maps.
+    if (init && acc_seen.size() > 1)
+      {
+	state_acc_pair p(state, bddtrue);
+	todo.insert(p);
+	acp_seen[p] = state_number++;
+      }
+
+    // Order the creation of normal states.
     mmp.first = state_number;
     for (bdd_set::iterator i = acc_seen.begin(); i != acc_seen.end(); ++i)
       {
@@ -170,7 +189,7 @@ namespace spot
     minmax_pair mmp;
 
     fill_todo(todo, seen, acp_seen,
-	      g.get_init_state(), g, mmp, state_number);
+	      g.get_init_state(), g, mmp, state_number, true);
     accepting_cond_splitter acs(g.all_accepting_conditions());
 
     while(! todo.empty())
@@ -179,10 +198,14 @@ namespace spot
 	todo.erase(todo.begin());
 	unsigned number = acp_seen[sap];
 
-	body << number << " "
+	// number == 0 is the initial state.  bddtrue as an accepting
-	     // Mark the initial state.
+	// conditions indicates a "fake" initial state introduced
-	     << ((number >= mmp.first && number < mmp.second) ? 1 : 0) << " ";
+	// because the original initial state was split into many
-
+	// states (with different accepting conditions).
+	// As this "fake" state has no input transitions, there is
+	// no point in computing any accepting conditions.
+	body << number << (number ? " 0 " : " 1 ");
+	if (sap.second != bddtrue)
 	  acs.split(body, sap.second);
 	body << "-1" << std::endl;
 
@@ -192,12 +215,14 @@ namespace spot
 	    // We have put the accepting conditions on the state,
 	    // so draw only outgoing transition with these accepting
 	    // conditions.
-	    if (si->current_accepting_conditions() != sap.second)
+
+	    if (sap.second != bddtrue
+		&& si->current_accepting_conditions() != sap.second)
 	      continue;
 
 	    minmax_pair destrange;
 	    fill_todo(todo, seen, acp_seen,
-		      si->current_state(), g, destrange, state_number);
+		      si->current_state(), g, destrange, state_number, false);
 
 	    // Link to all instances of the successor.
 	    std::string s = bdd_to_lbtt(si->current_condition(), d);

src/tgbaalgos/lbtt.hh

@@ -12,16 +12,19 @@ namespace spot
   /// labeled by propositional formulae, and generalized
   /// Büchi accepting conditions on \emph states.  This
   /// is unlike our spot::tgba automata which put
-  /// botg generalized accepting conditions and propositional
+  /// both generalized accepting conditions and propositional
   /// formulae) on \emph transitions.
   ///
-  /// This algorithm will therefore produce an automata
+  /// This algorithm will therefore produce an automata where
-  /// where accepting conditions have been moved from
+  /// accepting conditions have been moved from each transition to
-  /// each transition to previous state.  In the worst
+  /// previous state.  In the worst case, doing so will multiply the
-  /// case, doing so will multiply the number of states
+  /// number of states and transitions of the automata by
-  /// and transitions of the automata by <code>2^|Acc|</code>.
+  /// <code>2^|Acc|</code>.  where <code>|Acc|</code> is the number of
-  /// where <code>|Acc|</code> is the number of accepting
+  /// accepting conditions used by the automata.  (It can be a bit
-  /// conditions used by the automata.  You have been warned.
+  /// more because LBTT allows only for one initial state:
+  /// lbtt_reachable() may also have to create an additional state in
+  /// case the source initial state had to be split.)  You have been
+  /// warned.
   ///
   /// \param g The automata to print.
   /// \param os Where to print.