* src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the

functionality of the old tgba_tba_proxy.
* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator,
tgba_tba_proxy): Rewrite to produce TBA with at most N copies of
each state, skipping the `bddtrue' stage now used only in
tgba_sba_proxy.  Doing so removes approximately 6% of states in
the degeneralized tests of spotlbtt.test.
(tgba_sba_proxy): Implement it.
* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust
to take a tgba_sba_proxy.
* src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to
never_claim_reachable().

ChangeLog

@@ -1,5 +1,18 @@
 2004-11-16  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgba/tgbatba.hh (tgba_sba_proxy): New class, with the
+	functionality of the old tgba_tba_proxy.
+	* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator,
+	tgba_tba_proxy): Rewrite to produce TBA with at most N copies of
+	each state, skipping the `bddtrue' stage now used only in
+	tgba_sba_proxy.  Doing so removes approximately 6% of states in
+	the degeneralized tests of spotlbtt.test.
+	(tgba_sba_proxy): Implement it.
+	* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust
+	to take a tgba_sba_proxy.
+	* src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to
+	never_claim_reachable().
+
 	* src/tgba/tgbatba.cc (state_tba_proxy::hash): Use wang32_hash.
 	* src/tgba/tgbaproduct.cc (state_product::hash): Likewise.
 
@@ -8,7 +21,7 @@
 	* src/evtgba/product.cc (evtgba_product_state::hash): ... here.
 	* src/misc/Makefile.am (misc_HEADERS): Add hashfunc.hh.
 
-2004-11-15  Alexandre Duret-Lutz  <adl@gnu.org>
+2004-11-15  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/tgbatest/ltl2tgba.cc (main): For non-generalized emptiness
 	check, degeneralize the automaton only if it has too much

src/tgba/tgbatba.cc

@@ -112,9 +112,10 @@ namespace spot
       typedef tgba_tba_proxy::cycle_list::const_iterator iterator;
     public:
       tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it,
-				   iterator expected, iterator end,
+				   iterator expected,
+				   const list& cycle,
 				   bdd the_acceptance_cond)
-	: it_(it), expected_(expected), end_(end),
+	: it_(it), expected_(expected), cycle_(cycle),
 	  the_acceptance_cond_(the_acceptance_cond)
       {
       }
@@ -131,12 +132,14 @@ namespace spot
       first()
       {
 	it_->first();
+	sync_();
       }
 
       void
       next()
       {
 	it_->next();
+	sync_();
       }
 
       bool
@@ -150,27 +153,7 @@ namespace spot
       state_tba_proxy*
       current_state() const
       {
-	// A transition in the *EXPECTED acceptance set should be directed
+	return new state_tba_proxy(it_->current_state(), next_);
-	// to the next acceptance set.  If the current transition is also
-	// in the next acceptance set, then go the one after, etc.
-	//
-	// See Denis Oddoux's PhD thesis for a nice explanation (in French).
-	//  @PhDThesis{	  oddoux.03.phd,
-	//    author	= {Denis Oddoux},
-	//    title	= {Utilisation des automates alternants pour un
-	//  		  model-checking efficace des logiques temporelles
-	//  		  lin{\'e}aires.},
-	//    school	= {Universit{\'e}e Paris 7},
-	//    year	= {2003},
-	//    address	= {Paris, France},
-	//    month	= {December}
-	//  }
-	//
-	iterator next = expected_;
-	bdd acc = it_->current_acceptance_conditions();
-	while ((acc & *next) == *next && next != end_)
-	  ++next;
-	return new state_tba_proxy(it_->current_state(), next);
       }
 
       bdd
@@ -182,13 +165,66 @@ namespace spot
       bdd
       current_acceptance_conditions() const
       {
-	return the_acceptance_cond_;
+	return accepting_ ? the_acceptance_cond_ : bddfalse;
       }
 
     protected:
+
+      void
+      sync_()
+      {
+	if (done())
+	  return;
+
+	bdd acc = it_->current_acceptance_conditions();
+
+	// bddtrue is a special condition used for tgba_sba_proxy
+	// to denote the (N+1)th copy of the state, after all acceptance
+	// conditions have been traversed.  Such state is always accepting,
+	// so do not check acc for this.
+	// bddtrue is also used by tgba_tba_proxy if the automata do not
+	// use acceptance conditions.  In that cases, all state are accepting.
+	if (*expected_ != bddtrue)
+	  {
+	    // A transition in the *EXPECTED acceptance set should be
+	    // directed to the next acceptance set.  If the current
+	    // transition is also in the next acceptance set, then go
+	    // the one after, etc.
+	    //
+	    // See Denis Oddoux's PhD thesis for a nice explanation (in French).
+	    // @PhDThesis{	  oddoux.03.phd,
+	    //   author	= {Denis Oddoux},
+	    //   title	= {Utilisation des automates alternants pour un
+	    // 		  model-checking efficace des logiques temporelles
+	    // 		  lin{\'e}aires.},
+	    //   school	= {Universit{\'e}e Paris 7},
+	    //   year	= {2003},
+	    //   address= {Paris, France},
+	    //   month	= {December}
+	    // }
+
+	    next_ = expected_;
+	    while (next_ != cycle_.end() && (acc & *next_) == *next_)
+	      ++next_;
+	    if (next_ != cycle_.end())
+	      {
+		accepting_ = false;
+		return;
+	      }
+	  }
+	// The transition is accepting.
+	accepting_ = true;
+	// Skip as much acceptance conditions as we can on our cycle.
+	next_ = cycle_.begin();
+	while (next_ != expected_ && (acc & *next_) == *next_)
+	  ++next_;
+      }
+
       tgba_succ_iterator* it_;
       const iterator expected_;
-      const iterator end_;
+      iterator next_;
+      bool accepting_;
+      const list& cycle_;
       const bdd the_acceptance_cond_;
       friend class tgba_tba_proxy;
     };
@@ -198,23 +234,26 @@ namespace spot
   tgba_tba_proxy::tgba_tba_proxy(const tgba* a)
     : a_(a)
   {
-    bdd all = a_->all_acceptance_conditions();
-
     // We will use one acceptance condition for this automata.
     // Let's call it Acc[True].
     int v = get_dict()
       ->register_acceptance_variable(ltl::constant::true_instance(), this);
     the_acceptance_cond_ = bdd_ithvar(v);
 
-    // Now build the "cycle" of acceptance conditions.
+    if (a->number_of_acceptance_conditions() == 0)
-
-    acc_cycle_.push_front(bddtrue);
-
-    while (all != bddfalse)
       {
-	bdd next = bdd_satone(all);
+	acc_cycle_.push_front(bddtrue);
-	all -= next;
+      }
-	acc_cycle_.push_front(next);
+    else
+      {
+	// Build a cycle of expected acceptance conditions.
+	bdd all = a_->all_acceptance_conditions();
+	while (all != bddfalse)
+	  {
+	    bdd next = bdd_satone(all);
+	    all -= next;
+	    acc_cycle_.push_front(next);
+	  }
       }
   }
 
@@ -241,13 +280,8 @@ namespace spot
     tgba_succ_iterator* it = a_->succ_iter(s->real_state(),
 					   global_state, global_automaton);
 
-    cycle_list::const_iterator j = s->acceptance_iterator();
+    return new tgba_tba_proxy_succ_iterator(it, s->acceptance_iterator(),
-    cycle_list::const_iterator i = j++;
+					    acc_cycle_, the_acceptance_cond_);
-    if (j == acc_cycle_.end())
-      return new tgba_tba_proxy_succ_iterator(it, acc_cycle_.begin(),
-					      acc_cycle_.end(),
-					      the_acceptance_cond_);
-    return new tgba_tba_proxy_succ_iterator(it, i, acc_cycle_.end(), bddfalse);
   }
 
   bdd_dict*
@@ -290,15 +324,6 @@ namespace spot
     return !the_acceptance_cond_;
   }
 
-  bool
-  tgba_tba_proxy::state_is_accepting(const state* state) const
-  {
-    const state_tba_proxy* s =
-      dynamic_cast<const state_tba_proxy*>(state);
-    assert(s);
-    return bddtrue == s->acceptance_cond();
-  }
-
   bdd
   tgba_tba_proxy::compute_support_conditions(const state* state) const
   {
@@ -326,4 +351,23 @@ namespace spot
     return a_->transition_annotation(i->it_);
   }
 
+  ////////////////////////////////////////////////////////////////////////
+  // tgba_sba_proxy
+
+  tgba_sba_proxy::tgba_sba_proxy(const tgba* a)
+    : tgba_tba_proxy(a)
+  {
+    if (a->number_of_acceptance_conditions() > 0)
+      acc_cycle_.push_back(bddtrue);
+  }
+
+  bool
+  tgba_sba_proxy::state_is_accepting(const state* state) const
+  {
+    const state_tba_proxy* s =
+      dynamic_cast<const state_tba_proxy*>(state);
+    assert(s);
+    return bddtrue == s->acceptance_cond();
+  }
+
 }

src/tgba/tgbatba.hh

@@ -29,13 +29,12 @@
 namespace spot
 {
 
-  /// \brief Degeneralize a spot::tgba on the fly.
+  /// \brief Degeneralize a spot::tgba on the fly, producing a TBA.
   ///
   /// This class acts as a proxy in front of a spot::tgba, that should
-  /// be degeneralized on the fly.
+  /// be degeneralized on the fly.  The result is still a spot::tgba,
-  ///
+  /// but it will always have exactly one acceptance condition so
-  /// This automaton is a spot::tgba, but it will always have exactly
+  /// it could be called TBA (without the G).
-  /// one acceptance condition.
   ///
   /// The degeneralization is done by synchronizing the input
   /// automaton with a "counter" automaton such as the one shown in
@@ -43,8 +42,10 @@ namespace spot
   /// Couveur, FME99).
   ///
   /// If the input automaton uses N acceptance conditions, the output
-  /// automaton can have at most max(N,1)+1 times more states and
+  /// automaton can have at most max(N,1) times more states and
   /// transitions.
+  ///
+  /// \see tgba_sba_proxy
   class tgba_tba_proxy : public tgba
   {
   public:
@@ -71,29 +72,48 @@ namespace spot
     virtual bdd all_acceptance_conditions() const;
     virtual bdd neg_acceptance_conditions() const;
 
-    /// \brief Whether the state is accepting.
-    ///
-    /// A particularity of a spot::tgba_tba_proxy automaton is that
-    /// when a state has an outgoing accepting arc, all its outgoing
-    /// arcs are accepting.  The state itself can therefore be
-    /// considered accepting.  This is useful to many algorithms
-    /// working on degeneralized automata with state acceptance
-    /// conditions.
-    bool state_is_accepting(const state* state) const;
-
     typedef std::list<bdd> cycle_list;
   protected:
     virtual bdd compute_support_conditions(const state* state) const;
     virtual bdd compute_support_variables(const state* state) const;
 
+    cycle_list acc_cycle_;
   private:
     const tgba* a_;
-    cycle_list acc_cycle_;
     bdd the_acceptance_cond_;
     // Disallow copy.
     tgba_tba_proxy(const tgba_tba_proxy&);
     tgba_tba_proxy& tgba_tba_proxy::operator=(const tgba_tba_proxy&);
   };
 
+  /// \brief Degeneralize a spot::tgba on the fly, producing an SBA.
+  ///
+  /// This class acts as a proxy in front of a spot::tgba, that should
+  /// be degeneralized on the fly.
+  ///
+  /// This is similar to tgba_tba_proxy, except that automata produced
+  /// with this algorithms can also been see as State-based Büchi
+  /// Automata (SBA).  See tgba_sba_proxy::state_is_accepting().  (An
+  /// SBA is a TBA, and a TBA is a TGBA.)
+  ///
+  /// This extra property has a small cost in size: if the input
+  /// automaton uses N acceptance conditions, the output automaton can
+  /// have at most max(N,1)+1 times more states and transitions.
+  /// (This is only max(N,1) for tgba_tba_proxy.)
+  class tgba_sba_proxy : public tgba_tba_proxy
+  {
+  public:
+    tgba_sba_proxy(const tgba* a);
+
+    /// \brief Whether the state is accepting.
+    ///
+    /// A particularity of a spot::tgba_sba_proxy automaton is that
+    /// when a state has an outgoing accepting arc, all its outgoing
+    /// arcs are accepting.  The state itself can therefore be
+    /// considered accepting.  This is useful in algorithms working on
+    /// degeneralized automata with state acceptance conditions.
+    bool state_is_accepting(const state* state) const;
+  };
+
 }
 #endif // SPOT_TGBA_TGBATBA_HH

src/tgbaalgos/neverclaim.cc

@@ -37,7 +37,7 @@ namespace spot
     class never_claim_bfs : public tgba_reachable_iterator_breadth_first
     {
     public:
-      never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os,
+      never_claim_bfs(const tgba_sba_proxy* a, std::ostream& os,
 		      const ltl::formula* f)
 	: tgba_reachable_iterator_breadth_first(a),
 	  os_(os), f_(f), accept_all_(-1), fi_needed_(false)
@@ -76,7 +76,7 @@ namespace spot
       state_is_accepting(const state *s)
       {
 	return
-	  dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s);
+	  dynamic_cast<const tgba_sba_proxy*>(automata_)->state_is_accepting(s);
       }
 
       std::string
@@ -184,7 +184,7 @@ namespace spot
   } // anonymous
 
   std::ostream&
-  never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g,
+  never_claim_reachable(std::ostream& os, const tgba_sba_proxy* g,
 			const ltl::formula* f)
   {
     never_claim_bfs n(g, os, f);

src/tgbaalgos/neverclaim.hh

@@ -35,7 +35,7 @@ namespace spot
   /// \param f The (optional) formula associated to the automaton.  If given
   ///          it will be output as a comment.
   std::ostream& never_claim_reachable(std::ostream& os,
-				      const tgba_tba_proxy* g,
+				      const tgba_sba_proxy* g,
 				      const ltl::formula* f = 0);
 }
 

src/tgbatest/ltl2tgba.cc

@@ -58,7 +58,8 @@ syntax(char* prog)
 	    << std::endl
 	    << "  -A    same as -a, but as a set" << std::endl
 	    << "  -d    turn on traces during parsing" << std::endl
-	    << "  -D    degeneralize the automaton" << std::endl
+	    << "  -D    degeneralize the automaton as a TBA" << std::endl
+	    << "  -DS   degeneralize the automaton as an SBA" << std::endl
 	    << "  -e[ALGO]  emptiness-check, expect and compute an "
 	    << "accepting run" << std::endl
 	    << "  -E[ALGO]  emptiness-check, expect no accepting run"
@@ -134,7 +135,7 @@ main(int argc, char** argv)
   int exit_code = 0;
 
   bool debug_opt = false;
-  bool degeneralize_opt = false;
+  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
   bool degeneralize_maybe = false;
   bool fm_opt = false;
   bool fm_exprop_opt = false;
@@ -182,7 +183,11 @@ main(int argc, char** argv)
 	}
       else if (!strcmp(argv[formula_index], "-D"))
 	{
-	  degeneralize_opt = true;
+	  degeneralize_opt = DegenTBA;
+	}
+      else if (!strcmp(argv[formula_index], "-DS"))
+	{
+	  degeneralize_opt = DegenSBA;
 	}
       else if (!strncmp(argv[formula_index], "-e", 2))
         {
@@ -231,7 +236,7 @@ main(int argc, char** argv)
 	}
       else if (!strcmp(argv[formula_index], "-N"))
 	{
-	  degeneralize_opt = true;
+	  degeneralize_opt = DegenSBA;
 	  output = 8;
 	}
       else if (!strcmp(argv[formula_index], "-p"))
@@ -494,10 +499,14 @@ main(int argc, char** argv)
 
       spot::tgba_tba_proxy* degeneralized = 0;
 
-      if (degeneralize_maybe && a->number_of_acceptance_conditions() > 1)
+      if (degeneralize_maybe
-	degeneralize_opt = true;
+	  && degeneralize_opt == NoDegen
-      if (degeneralize_opt)
+	  && a->number_of_acceptance_conditions() > 1)
+	degeneralize_opt = DegenTBA;
+      if (degeneralize_opt == DegenTBA)
 	a = degeneralized = new spot::tgba_tba_proxy(a);
+      else if (degeneralize_opt == DegenSBA)
+	a = degeneralized = new spot::tgba_sba_proxy(a);
 
       spot::tgba_reduc* aut_red = 0;
       if (reduc_aut != spot::Reduce_None)
@@ -602,8 +611,13 @@ main(int argc, char** argv)
 	  spot::lbtt_reachable(std::cout, a);
 	  break;
 	case 8:
-	  spot::never_claim_reachable(std::cout, degeneralized, f);
+	  {
-	  break;
+	    assert(degeneralize_opt == DegenSBA);
+	    const spot::tgba_sba_proxy* s =
+	      static_cast<const spot::tgba_sba_proxy*>(degeneralized);
+	    spot::never_claim_reachable(std::cout, s, f);
+	    break;
+	  }
 	default:
 	  assert(!"unknown output option");
 	}