* src/tgba/tgba.hh (tgba::~tgba): Make it public.

* src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: New files.
* src/tgba/Makefile.am (tgba_HEADERS): Add tgbatba.hh.
(libtgba_la_SOURCES): Add tgbatba.cc.
* src/tgbatest/ltl2tgba.cc: Add option -D.

ChangeLog

@@ -1,5 +1,11 @@
 2003-07-25  Alexandre Duret-Lutz  <aduret@src.lip6.fr>
 
+	* src/tgba/tgba.hh (tgba::~tgba): Make it public.
+	* src/tgba/tgbatba.cc, src/tgba/tgbatba.hh: New files.
+	* src/tgba/Makefile.am (tgba_HEADERS): Add tgbatba.hh.
+	(libtgba_la_SOURCES): Add tgbatba.cc.
+	* src/tgbatest/ltl2tgba.cc: Add option -D.
+
 	* src/tgbaalgos/lbtt.cc (bdd_less_than): Move ...
 	* src/misc/bddlt.hh: ... in this new file.
 	* src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh.

src/tgba/Makefile.am

@@ -18,7 +18,8 @@ tgba_HEADERS = \
   tgbabddcoredata.hh \
   tgbabddfactory.hh \
   tgbaexplicit.hh \
-  tgbaproduct.hh
+  tgbaproduct.hh \
+  tgbatba.hh
 
 noinst_LTLIBRARIES = libtgba.la
 libtgba_la_SOURCES = \
@@ -32,4 +33,5 @@ libtgba_la_SOURCES = \
   tgbabddconcreteproduct.cc \
   tgbabddcoredata.cc \
   tgbaexplicit.cc \
-  tgbaproduct.cc
+  tgbaproduct.cc \
+  tgbatba.cc

src/tgba/tgba.hh

@@ -33,9 +33,10 @@ namespace spot
   {
   protected:
     tgba();
-    virtual ~tgba();
 
   public:
+    virtual ~tgba();
+
     /// \brief Get the initial state of the automaton.
     ///
     /// The state has been allocated with \c new.  It is the

src/tgba/tgbatba.cc

@@ -0,0 +1,253 @@
+#include <cassert>
+#include "tgbatba.hh"
+#include "bddprint.hh"
+#include "ltlast/constant.hh"
+
+namespace spot
+{
+
+  /// \brief A state for spot::tgba_tba_proxy.
+  ///
+  /// This state is in fact a pair of state: the state from the tgba
+  /// automaton, and the "counter" (we use the accepting set
+  /// BDD variable instead of an integer counter).
+  class state_tba_proxy : public state
+  {
+  public:
+    state_tba_proxy(state* s, bdd acc)
+      :	s_(s), acc_(acc)
+    {
+    }
+
+    /// Copy constructor
+    state_tba_proxy(const state_tba_proxy& o)
+      : state(),
+	s_(o.real_state()->clone()),
+	acc_(o.accepting_cond())
+    {
+    }
+
+    virtual 
+    ~state_tba_proxy()
+    {
+      delete s_;
+    }
+
+    state*
+    real_state() const
+    {
+      return s_;
+    }
+
+    bdd
+    accepting_cond() const
+    {
+      return acc_;
+    }
+
+    virtual int 
+    compare(const state* other) const
+    {
+      const state_tba_proxy* o = dynamic_cast<const state_tba_proxy*>(other);
+      assert(o);
+      int res = s_->compare(o->real_state());
+      if (res != 0)
+	return res;
+      return acc_.id() - o->accepting_cond().id();
+    }
+    
+    virtual 
+    state_tba_proxy* clone() const
+    {
+      return new state_tba_proxy(*this);
+    }
+
+  private:
+    state* s_;
+    bdd acc_;
+  };
+
+
+  /// \brief Iterate over the successors of tgba_tba_proxy computed on the fly.
+  class tgba_tba_proxy_succ_iterator: public tgba_succ_iterator
+  {
+  public:
+    tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it,
+				 bdd acc, bdd next_acc,
+				 bdd the_accepting_cond)
+      : it_(it), acc_(acc), next_acc_(next_acc), 
+	the_accepting_cond_(the_accepting_cond)
+    {
+    }
+
+    virtual
+    ~tgba_tba_proxy_succ_iterator()
+    {
+    }
+
+    // iteration
+
+    void 
+    first()
+    {
+      it_->first();
+    }
+
+    void 
+    next()
+    {
+      it_->next();
+    }
+
+    bool 
+    done() const
+    {
+      return it_->done();
+    }
+
+    // inspection
+
+    state_tba_proxy* 
+    current_state() const
+    {
+      state* s = it_->current_state();
+      bdd acc;
+      // Transition in the ACC_ accepting set should be directed
+      // to the NEXT_ACC_ accepting set.
+      if (acc_ == bddtrue 
+	  || (acc_ & it_->current_accepting_conditions()) == acc_)
+	acc = next_acc_;
+      else
+	acc = acc_;
+      return new state_tba_proxy(s, acc);
+    }
+
+    bdd 
+    current_condition() const
+    {
+      return it_->current_condition();
+    }
+
+    bdd 
+    current_accepting_conditions() const
+    {
+      return the_accepting_cond_;
+    }
+
+  protected:
+    tgba_succ_iterator* it_;
+    bdd acc_;
+    bdd next_acc_;
+    bdd the_accepting_cond_;
+  };
+
+
+  tgba_tba_proxy::tgba_tba_proxy(const tgba* a)
+    : a_(a)
+  {
+    bdd all = a_->all_accepting_conditions();
+
+    // We will use one accepting condition for this automata.
+    // Let's call it Acc[True].
+    int v = get_dict()
+      ->register_accepting_variable(ltl::constant::true_instance(), this);
+    the_accepting_cond_ = bdd_ithvar(v);
+
+    // Now build the "cycle" of accepting conditions.
+
+    bdd last = bdd_satone(all);
+    all &= !last;
+
+    acc_cycle_[bddtrue] = last;
+
+    while (all != bddfalse)
+      {
+	bdd next = bdd_satone(all);
+	all &= !next;
+	acc_cycle_[last] = next;
+	last = next;
+      }
+
+    acc_cycle_[last] = bddtrue;
+  }
+
+  tgba_tba_proxy::~tgba_tba_proxy()
+  {
+    get_dict()->unregister_all_my_variables(this);
+  }
+
+  state* 
+  tgba_tba_proxy::get_init_state() const
+  {
+    cycle_map::const_iterator i = acc_cycle_.find(bddtrue);
+    assert(i != acc_cycle_.end());
+    return new state_tba_proxy(a_->get_init_state(), i->second);
+  }
+
+  tgba_succ_iterator*
+  tgba_tba_proxy::succ_iter(const state* local_state,
+			    const state* global_state,
+			    const tgba* global_automaton) const
+  {
+    const state_tba_proxy* s = 
+      dynamic_cast<const state_tba_proxy*>(local_state);
+    assert(s);
+
+    tgba_succ_iterator* it = a_->succ_iter(s->real_state(), 
+					   global_state, global_automaton);
+    bdd acc = s->accepting_cond();
+    cycle_map::const_iterator i = acc_cycle_.find(acc);
+    assert(i != acc_cycle_.end());
+    return 
+      new tgba_tba_proxy_succ_iterator(it, acc, i->second,
+				       (acc == bddtrue) 
+				       ? the_accepting_cond_ : bddfalse);
+  }
+  
+  bdd_dict* 
+  tgba_tba_proxy::get_dict() const
+  {
+    return a_->get_dict();
+  }
+  
+  std::string 
+  tgba_tba_proxy::format_state(const state* state) const
+  {
+    const state_tba_proxy* s = 
+      dynamic_cast<const state_tba_proxy*>(state);
+    assert(s);
+    return a_->format_state(s->real_state()) + "(" 
+      + bdd_format_set(get_dict(), s->accepting_cond()) + ")";
+  }
+  
+  bdd 
+  tgba_tba_proxy::all_accepting_conditions() const
+  {
+    return the_accepting_cond_;
+  }
+  
+  bdd 
+  tgba_tba_proxy::neg_accepting_conditions() const
+  {
+    return !the_accepting_cond_;
+  }
+  
+  bdd 
+  tgba_tba_proxy::compute_support_conditions(const state* state) const
+  {
+    const state_tba_proxy* s = 
+      dynamic_cast<const state_tba_proxy*>(state);
+    assert(s);
+    return a_->support_conditions(s->real_state());
+  }
+  
+  bdd 
+  tgba_tba_proxy::compute_support_variables(const state* state) const
+  {
+    const state_tba_proxy* s = 
+      dynamic_cast<const state_tba_proxy*>(state);
+    assert(s);
+    return a_->support_variables(s->real_state());
+  }
+
+}

src/tgba/tgbatba.hh

@@ -0,0 +1,62 @@
+#ifndef SPOT_TGBA_TGBATBA_HH
+# define SPOT_TGBA_TGBATBA_HH
+
+#include "tgba.hh"
+#include "misc/bddlt.hh"
+
+namespace spot
+{
+
+  /// \brief Degeneralize a spot::tgba on the fly.
+  ///
+  /// This class acts as a proxy in front of a spot::tgba, that should
+  /// be degeneralized on the fly.
+  ///
+  /// This automaton is a spot::tgba, but it will always have exactly
+  /// one accepting condition.
+  ///
+  /// The degeneralization is done by synchronizing the input
+  /// automaton with a "counter" automaton such as the one shown in
+  /// "On-the-fly Verification of Linear Temporal Logic" (Jean-Michel
+  /// Couveur, FME99).
+  ///
+  /// If the input automaton uses N accepting conditions, the output
+  /// automaton can have at most max(N,1)+1 times more states and
+  /// transitions.
+  class tgba_tba_proxy : public tgba
+  {
+  public:
+    tgba_tba_proxy(const tgba* a);
+
+    virtual ~tgba_tba_proxy();
+
+    virtual state* get_init_state() const;
+
+    virtual tgba_succ_iterator*
+    succ_iter(const state* local_state,
+	      const state* global_state = 0,
+	      const tgba* global_automaton = 0) const;
+
+    virtual bdd_dict* get_dict() const;
+
+    virtual std::string format_state(const state* state) const;
+
+    virtual bdd all_accepting_conditions() const;
+    virtual bdd neg_accepting_conditions() const;
+
+  protected:
+    virtual bdd compute_support_conditions(const state* state) const;
+    virtual bdd compute_support_variables(const state* state) const;
+
+  private:
+    const tgba* a_;
+    typedef std::map<bdd, bdd, bdd_less_than> cycle_map;
+    cycle_map acc_cycle_;
+    bdd the_accepting_cond_;
+    // Disallow copy.
+    tgba_tba_proxy(const tgba_tba_proxy&);
+    tgba_tba_proxy& tgba_tba_proxy::operator=(const tgba_tba_proxy&);
+  };
+
+}
+#endif // SPOT_TGBA_TGBATBA_HH

src/tgbatest/ltl2tgba.cc

@@ -7,6 +7,7 @@
 #include "tgba/bddprint.hh"
 #include "tgbaalgos/dotty.hh"
 #include "tgbaalgos/lbtt.hh"
+#include "tgba/tgbatba.hh"
 
 void
 syntax(char* prog)
@@ -18,6 +19,7 @@ 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
 	    << "  -r   display the relation BDD, not the reachability graph"
 	    << std::endl
 	    << "  -R   same as -r, but as a set" << std::endl
@@ -33,6 +35,7 @@ main(int argc, char** argv)
   int exit_code = 0;
 
   bool debug_opt = false;
+  bool degeneralize_opt = false;
   int output = 0;
   int formula_index = 0;
 
@@ -55,6 +58,10 @@ main(int argc, char** argv)
 	{
 	  debug_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-D"))
+	{
+	  degeneralize_opt = true;
+	}
       else if (!strcmp(argv[formula_index], "-r"))
 	{
 	  output = 1;
@@ -88,28 +95,34 @@ main(int argc, char** argv)
   spot::bdd_dict* dict = new spot::bdd_dict();
   if (f)
     {
-      spot::tgba_bdd_concrete* a = spot::ltl_to_tgba(f, dict);
+      spot::tgba_bdd_concrete* concrete = spot::ltl_to_tgba(f, dict);
+      spot::tgba* a = concrete;
       spot::ltl::destroy(f);
+
+      spot::tgba* degeneralized = 0;
+      if (degeneralize_opt)
+	a = degeneralized = new spot::tgba_tba_proxy(a);
+
       switch (output)
 	{
 	case 0:
 	  spot::dotty_reachable(std::cout, a);
 	  break;
 	case 1:
-	  spot::bdd_print_dot(std::cout, a->get_dict(),
-			      a->get_core_data().relation);
+	  spot::bdd_print_dot(std::cout, concrete->get_dict(),
+			      concrete->get_core_data().relation);
 	  break;
 	case 2:
-	  spot::bdd_print_dot(std::cout, a->get_dict(),
-			      a->get_core_data().accepting_conditions);
+	  spot::bdd_print_dot(std::cout, concrete->get_dict(),
+			      concrete->get_core_data().accepting_conditions);
 	  break;
 	case 3:
-	  spot::bdd_print_set(std::cout, a->get_dict(),
-			      a->get_core_data().relation);
+	  spot::bdd_print_set(std::cout, concrete->get_dict(),
+			      concrete->get_core_data().relation);
 	  break;
 	case 4:
-	  spot::bdd_print_set(std::cout, a->get_dict(),
-			      a->get_core_data().accepting_conditions);
+	  spot::bdd_print_set(std::cout, concrete->get_dict(),
+			      concrete->get_core_data().accepting_conditions);
 	  break;
 	case 5:
 	  a->get_dict()->dump(std::cout);
@@ -120,7 +133,11 @@ main(int argc, char** argv)
 	default:
 	  assert(!"unknown output option");
 	}
-      delete a;
+
+      if (degeneralize_opt)
+	delete degeneralized;
+
+      delete concrete;
     }
   else
     {