Better selection of the acceptance of the initial state in SBA.

* src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Set
cycle_start_ to start in the accepting layer of the degeneralized
automaton if the initial state has an accepting self-loop.
Otherwise, starts at the level of the first acceptance condition
as previously.
(tgba_sba_proxy::get_init_state): Use cycle_start_.
* src/tgba/tgbatba.hh (tgba_tba_proxy::a_): Make it protected so
that we can use it in tgba_sba_proxy::tgba_sba_proxy.
(tgba_sba_proxy::cycle_start_, tgba_sba_proxy::get_init_state):
Declare.
* src/tgbatest/ltl2tgba.test: More tests.

ChangeLog

@@ -1,3 +1,19 @@
+2010-03-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Better selection of the acceptance of the initial state in SBA.
+
+	* src/tgba/tgbatba.cc (tgba_sba_proxy::tgba_sba_proxy): Set
+	cycle_start_ to start in the accepting layer of the degeneralized
+	automaton if the initial state has an accepting self-loop.
+	Otherwise, starts at the level of the first acceptance condition
+	as previously.
+	(tgba_sba_proxy::get_init_state): Use cycle_start_.
+	* src/tgba/tgbatba.hh (tgba_tba_proxy::a_): Make it protected so
+	that we can use it in tgba_sba_proxy::tgba_sba_proxy.
+	(tgba_sba_proxy::cycle_start_, tgba_sba_proxy::get_init_state):
+	Declare.
+	* src/tgbatest/ltl2tgba.test: More tests.
+
 2010-03-05  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	Generalize the previous patch to accepting states in SBA.

src/tgba/tgbatba.cc

@@ -375,7 +375,49 @@ namespace spot
     : tgba_tba_proxy(a)
   {
     if (a->number_of_acceptance_conditions() > 0)
-      acc_cycle_.push_back(bddtrue);
+      {
+	cycle_start_ = acc_cycle_.insert(acc_cycle_.end(), bddtrue);
+
+	bdd all = a->all_acceptance_conditions();
+
+	state* init = a->get_init_state();
+	tgba_succ_iterator* it = a->succ_iter(init);
+	for (it->first(); !it->done(); it->next())
+	  {
+	    // Look only for transitions that are accepting.
+	    if (all != it->current_acceptance_conditions())
+	      continue;
+	    // Look only for self-loops.
+	    state* dest = it->current_state();
+	    if (dest->compare(init) == 0)
+	      {
+		// The initial state has an accepting self-loop.
+		// In that case it is better to start the accepting
+		// cycle on a "acceptance" state.  This will avoid
+		// duplication of the initial state.
+		// The cycle_start_ points to the right starting
+		// point already, so just return.
+		delete dest;
+		delete it;
+		return;
+	      }
+	    delete dest;
+	  }
+	delete it;
+      }
+
+    // If we arrive here either because the number of acceptance
+    // condition is 0, or because the initial state has no accepting
+    // self-loop, start the acceptance cycle on the first condition
+    // (that is a non-accepting state if the number of conditions is
+    // not 0).
+    cycle_start_ = acc_cycle_.begin();
+  }
+
+  state*
+  tgba_sba_proxy::get_init_state() const
+  {
+    return new state_tba_proxy(a_->get_init_state(), cycle_start_);
   }
 
   bool

src/tgba/tgbatba.hh

@@ -1,3 +1,5 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Développement de
+// l'Epita.
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -79,8 +81,8 @@ namespace spot
     virtual bdd compute_support_variables(const state* state) const;
 
     cycle_list acc_cycle_;
-  private:
     const tgba* a_;
+  private:
     bdd the_acceptance_cond_;
     // Disallow copy.
     tgba_tba_proxy(const tgba_tba_proxy&);
@@ -115,6 +117,10 @@ namespace spot
     /// considered accepting.  This is useful in algorithms working on
     /// degeneralized automata with state acceptance conditions.
     bool state_is_accepting(const state* state) const;
+
+    virtual state* get_init_state() const;
+  protected:
+    cycle_list::iterator cycle_start_;
   };
 
 }

src/tgbatest/ltl2tgba.test

@@ -59,3 +59,19 @@ for opt in '' -D -DS; do
   grep 'transitions: 6$' stdout
   grep 'states: 3$' stdout
 done
+
+# Make sure '!(Ga U b)' has 3 states and 6 transitions,
+# before and after degeneralization.
+for opt in '' -D -DS; do
+  ../ltl2tgba -k -f -R3 $opt '!(Ga U b)' > stdout
+  grep 'transitions: 6$' stdout
+  grep 'states: 3$' stdout
+done
+
+# Make sure 'Ga U b' has 4 states and 6 transitions,
+# before and after degeneralization.
+for opt in '' -D -DS; do
+  ../ltl2tgba -k -f -R3 $opt 'Ga U b' > stdout
+  grep 'transitions: 6$' stdout
+  grep 'states: 4$' stdout
+done