A new complementation construction based on ranking.

* src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh: The
construction.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/complementation.cc: Add options to support this
construction in addition to Safra construction.
* src/tgba/Makefile.am: Adjust.
* src/tgbatest/complementation.test: Adjust to test also this
complementation.

ChangeLog

@@ -1,3 +1,16 @@
+2009-09-29  Guillaume Sadegh  <sadegh@lrde.epita.fr>
+
+	A new complementation construction based on ranking.
+
+	* src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh: The
+	construction.
+	* src/tgbatest/Makefile.am: Adjust.
+	* src/tgbatest/complementation.cc: Add options to support this
+	construction in addition to Safra construction.
+	* src/tgba/Makefile.am: Adjust.
+	* src/tgbatest/complementation.test: Adjust to test also this
+	complementation.
+
 2009-09-29  Guillaume Sadegh  <sadegh@lrde.epita.fr>
 
 	* src/ltltest/randltl.cc, src/ltltest/reduc.test,

src/tgba/Makefile.am

@@ -40,6 +40,7 @@ tgba_HEADERS = \
   tgbabddconcreteproduct.hh \
   tgbabddcoredata.hh \
   tgbabddfactory.hh \
+  tgbacomplement.hh \
   tgbaexplicit.hh \
   tgbafromfile.hh \
   tgbascc.hh \
@@ -63,8 +64,9 @@ libtgba_la_SOURCES = \
   tgbabddconcretefactory.cc \
   tgbabddconcreteproduct.cc \
   tgbabddcoredata.cc \
-  tgbafromfile.cc \
+  tgbacomplement.cc \
   tgbaexplicit.cc \
+  tgbafromfile.cc \
   tgbaproduct.cc \
   tgbareduc.cc \
   tgbasafracomplement.cc \

src/tgba/tgbacomplement.cc

@@ -0,0 +1,794 @@
+#include <vector>
+#include <cassert>
+#include <sstream>
+#include <boost/shared_ptr.hpp>
+#include "bdd.h"
+#include "state.hh"
+#include "tgbacomplement.hh"
+#include "misc/hash.hh"
+#include "tgbaalgos/bfssteps.hh"
+#include "misc/hashfunc.hh"
+#include "ltlast/formula.hh"
+#include "ltlast/constant.hh"
+
+namespace spot
+{
+  /// \brief An Equivalence Relation for \c boost::shared_ptr<const state>.
+  /// \ingroup tgba_essentials
+  ///
+  /// This is meant to be used as a comparison functor for
+  /// Sgi \c hash_map whose key are of type \c boost::shared_ptr<const state>.
+  ///
+  /// For instance here is how one could declare
+  /// a map of \c boost::shared_ptr<const state>
+  /// \code
+  ///   // Remember how many times each state has been visited.
+  ///   Sgi::hash_map<boost::shared_ptr<const state>, int,
+  ///                 spot::state_shared_ptr_hash,
+  ///                 spot::state_shared_ptr_equal> seen;
+  /// \endcode
+  struct state_shared_ptr_equal:
+    public std::binary_function<boost::shared_ptr<const state>,
+                                boost::shared_ptr<const state>, bool>
+  {
+    bool
+    operator()(boost::shared_ptr<const state> left,
+               boost::shared_ptr<const state> right) const
+    {
+      assert(left);
+      return 0 == left->compare(right.get());
+    }
+  };
+
+
+  /// \brief Hash Function for \c boost::shared_ptr<const state>.
+  /// \ingroup tgba_essentials
+  /// \ingroup hash_funcs
+  ///
+  /// This is meant to be used as a hash functor for
+  /// Sgi's \c hash_map whose key are of type
+  /// \c boost::shared_ptr<const state>.
+  ///
+  /// For instance here is how one could declare
+  /// a map of \c boost::shared_ptr<const state>.
+  /// \code
+  ///   // Remember how many times each state has been visited.
+  ///   Sgi::hash_map<boost::shared_ptr<const state>, int,
+  ///                 spot::state_shared_ptr_hash,
+  ///                 spot::state_shared_ptr_equal> seen;
+  /// \endcode
+  struct state_shared_ptr_hash:
+    public std::unary_function<boost::shared_ptr<const state>, size_t>
+  {
+    size_t
+    operator()(boost::shared_ptr<const state> that) const
+    {
+      assert(that);
+      return that->hash();
+    }
+  };
+
+  namespace
+  {
+    ////////////////////////////////////////
+    // rank
+
+    /// \brief A rank structure, one of the main structure of the algorithm.
+    ///
+    /// A rank has a number (\a rank) that refers to the depth in the DAG of
+    /// the current word. When the rank is odd, a \a condition is associated
+    /// to this rank.
+    struct rank_t
+    {
+      mutable unsigned rank;
+      mutable bdd_ordered condition;
+
+      bool operator<(const rank_t& other) const
+      {
+        return rank < other.rank ||
+          condition.order() < other.condition.order();
+      }
+
+      unsigned get_rank() const
+      {
+        return rank;
+      }
+
+      bdd_ordered get_condition() const
+      {
+        return condition;
+      }
+
+      size_t hash() const
+      {
+        size_t hash = wang32_hash(rank);
+        if (rank & 1)
+          hash ^= wang32_hash(condition.order());
+        return hash;
+      }
+
+      std::string format() const
+      {
+        std::ostringstream ss;
+        ss << "{rank: " << rank;
+        if (rank & 1)
+        {
+          ss << ", bdd: {" << condition.order() << ", " <<
+            bddset << condition.get_bdd() << "} ";
+        }
+        ss << "}";
+        return ss.str();
+      }
+    };
+
+    // typedefs.
+    typedef boost::shared_ptr<const state> shared_state;
+    typedef Sgi::hash_map<shared_state, rank_t,
+                          state_shared_ptr_hash,
+                          state_shared_ptr_equal> state_rank_map;
+    typedef Sgi::hash_set<shared_state,
+                          state_shared_ptr_hash,
+                          state_shared_ptr_equal> state_set;
+
+    ////////////////////////////////////////
+    // count_states
+
+    /// \brief Count the number of states in a tgba.
+    class count_states : public bfs_steps
+    {
+    public:
+      count_states(const tgba* a)
+        : bfs_steps(a)
+      {
+        shared_state s(a->get_init_state());
+        states_.insert(s);
+
+        tgba_run::steps l;
+        search(s.get(), l);
+      }
+
+      virtual const state* filter(const state* s)
+      {
+        shared_state _s(s);
+        if (states_.find(_s) == states_.end())
+        {
+          states_.insert(_s);
+          return s;
+        }
+        return 0;
+      }
+
+      virtual bool match(tgba_run::step&, const state*)
+      {
+        return false;
+      }
+
+      size_t size() const
+      {
+        return states_.size();
+      }
+    private:
+      state_set states_;
+    };
+
+    ////////////////////////////////////////
+    // state_complement
+
+    /// States used by spot::tgba_complement.
+    /// A state has a map of states associated to ranks, and a set
+    /// of filtered states.
+    /// \ingroup tgba_representation
+    class state_complement : public state
+    {
+    public:
+      state_complement();
+      state_complement(const state_complement& other);
+      state_complement(state_rank_map state_map, state_set state_filter);
+      virtual ~state_complement() {}
+
+      virtual int compare(const state* other) const;
+      virtual size_t hash() const;
+      virtual state_complement* clone() const;
+
+      void add(shared_state state, const rank_t& rank);
+      const state_rank_map& get_state_map() const;
+      const state_set& get_filter_set() const;
+      bool accepting() const;
+    private:
+      state_rank_map state_map_;
+      state_set state_filter_;
+    };
+
+    state_complement::state_complement()
+    {
+    }
+
+    state_complement::state_complement(state_rank_map state_map,
+                                       state_set state_filter)
+      : state_map_(state_map), state_filter_(state_filter)
+    {
+    }
+
+    state_complement::state_complement(const state_complement& other)
+    {
+      state_map_ = other.state_map_;
+      state_filter_ = other.state_filter_;
+    }
+
+    int
+    state_complement::compare(const state* o) const
+    {
+      const state_complement* other = dynamic_cast<const state_complement*>(o);
+
+      if (other == 0)
+        return 1;
+
+      if (state_map_.size() < other->state_map_.size())
+        return -1;
+      else if (state_map_.size() > other->state_map_.size())
+        return 1;
+
+      if (state_filter_.size() < other->state_filter_.size())
+        return -1;
+      else if (state_filter_.size() > other->state_filter_.size())
+        return 1;
+
+      {
+        state_rank_map::const_iterator i = state_map_.begin();
+        state_rank_map::const_iterator j = other->state_map_.begin();
+        while (i != state_map_.end() && j != other->state_map_.end())
+        {
+          int result = i->first->compare(j->first.get());
+          if (result != 0)
+            return result;
+          if (i->second < j->second)
+            return -1;
+          if (j->second < i->second)
+            return 1;
+          ++i;
+          ++j;
+        }
+      }
+
+      {
+        state_set::const_iterator i = state_filter_.begin();
+        state_set::const_iterator j = other->state_filter_.begin();
+        while (i != state_filter_.end() && j != other->state_filter_.end())
+        {
+          int result = (*i)->compare(j->get());
+          if (result != 0)
+            return result;
+          ++i;
+          ++j;
+        }
+      }
+
+      return 0;
+    }
+
+    size_t
+    state_complement::hash() const
+    {
+      size_t hash = 0;
+
+      {
+        state_rank_map::const_iterator i = state_map_.begin();
+        while (i != state_map_.end())
+        {
+          hash ^= i->first->hash();
+          hash ^= i->second.hash();
+          ++i;
+        }
+      }
+
+      {
+        state_set::const_iterator i = state_filter_.begin();
+        while (i != state_filter_.end())
+        {
+          hash ^= (*i)->hash();
+          ++i;
+        }
+      }
+
+      return hash;
+    }
+
+    state_complement*
+    state_complement::clone() const
+    {
+      return new state_complement(*this);
+    }
+
+    void
+    state_complement::add(shared_state state,
+                          const rank_t& rank)
+    {
+      state_map_[state] = rank;
+    }
+
+    const state_rank_map&
+    state_complement::get_state_map() const
+    {
+      return state_map_;
+    }
+
+    const state_set&
+    state_complement::get_filter_set() const
+    {
+      return state_filter_;
+    }
+
+    bool
+    state_complement::accepting() const
+    {
+      return state_filter_.empty();
+    }
+
+    /// Successor iterators used by spot::tgba_complement.
+    /// \ingroup tgba_representation
+    ///
+    /// Since the algorithm works on-the-fly, the key components of the
+    /// algorithm are implemented in this class.
+    ///
+    ///
+    class tgba_complement_succ_iterator: public tgba_succ_iterator
+    {
+    public:
+      typedef std::list<bdd> bdd_list_t;
+
+      tgba_complement_succ_iterator(const tgba_sgba_proxy* automaton,
+                                    bdd the_acceptance_cond,
+                                    const acc_list_t& acc_list,
+                                    const state_complement* origin);
+      virtual ~tgba_complement_succ_iterator() {};
+
+      virtual void first();
+      virtual void next();
+      virtual bool done() const;
+      virtual state_complement* current_state() const;
+      virtual bdd current_condition() const;
+      virtual bdd current_acceptance_conditions() const;
+    private:
+      /// \brief Create the highest rank of \a origin_ as origin and
+      /// \a condition as successor condition.
+      void successor_highest_rank(bdd condition);
+      void get_atomics(std::set<int>& list, bdd c);
+      void get_conj_list();
+      bool is_valid_rank() const;
+      bool next_valid_rank();
+
+      const tgba_sgba_proxy* automaton_;
+      bdd the_acceptance_cond_;
+      const acc_list_t& acc_list_;
+      const state_complement* origin_;
+      const state_complement* current_state_;
+      bdd_list_t condition_list_;
+      bdd_list_t::const_iterator current_condition_;
+      state_rank_map highest_current_ranks_;
+      state_rank_map current_ranks_;
+      state_set highest_state_set_;
+    };
+
+    tgba_complement_succ_iterator::
+    tgba_complement_succ_iterator(const tgba_sgba_proxy* automaton,
+                                  bdd the_acceptance_cond,
+                                  const acc_list_t& acc_list,
+                                  const state_complement* origin)
+      : automaton_(automaton), the_acceptance_cond_(the_acceptance_cond),
+        acc_list_(acc_list), origin_(origin)
+    {
+      get_conj_list();
+    }
+
+    /// Insert in \a list atomic properties of the formula \a c.
+    void
+    tgba_complement_succ_iterator::get_atomics(std::set<int>& list, bdd c)
+    {
+      bdd current = bdd_satone(c);
+      while (current != bddtrue && current != bddfalse)
+      {
+        list.insert(bdd_var(current));
+        bdd high = bdd_high(current);
+        if (high == bddfalse)
+          current = bdd_low(current);
+        else
+          current = high;
+      }
+    }
+
+    /// Create the conjunction of all the atomic properties from
+    /// the successors of the current state.
+    void
+    tgba_complement_succ_iterator::get_conj_list()
+    {
+      std::set<int> atomics;
+      condition_list_.clear();
+      state_rank_map sr_map = origin_->get_state_map();
+
+      // Retrieve all the atomics in acceptance conditions.
+      for (state_rank_map::const_iterator i = sr_map.begin();
+           i != sr_map.end();
+           ++i)
+      {
+        tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get());
+        for (iterator->first(); !iterator->done(); iterator->next())
+        {
+          bdd c = iterator->current_condition();
+          get_atomics(atomics, c);
+        }
+        delete iterator;
+      }
+
+      // Compute the conjunction of all those atomic properties.
+      unsigned atomics_size = atomics.size();
+
+      assert(atomics_size < 32);
+      for (unsigned i = 1; i <= static_cast<unsigned>(1 << atomics_size); ++i)
+      {
+        bdd result = bddtrue;
+        unsigned position = 1;
+        for (std::set<int>::const_iterator a_it = atomics.begin();
+             a_it != atomics.end();
+             ++a_it, position <<= 1)
+        {
+          bdd this_atomic;
+          if (position & i)
+            this_atomic = bdd_ithvar(*a_it);
+          else
+            this_atomic = bdd_nithvar(*a_it);
+          result = bdd_apply(result, this_atomic, bddop_and);
+        }
+        condition_list_.push_back(result);
+      }
+    }
+
+    /// Check whether \a current_ranks_ is a valid rank.
+    /// For each odd rank, its condition associated must not
+    /// be present in its tracked state.
+    bool
+    tgba_complement_succ_iterator::is_valid_rank() const
+    {
+      for (state_rank_map::const_iterator i = current_ranks_.begin();
+           i != current_ranks_.end();
+           ++i)
+      {
+        if (i->second.rank & 1)
+        {
+          if ((automaton_->state_acceptance_conditions(i->first.get()) &
+               i->second.condition.get_bdd()) != bddfalse)
+            return false;
+        }
+      }
+      return true;
+    }
+
+    /// \brief Decrease \a current_ranks_ and produces a valid rank.
+    /// \a current_ranks_ is a map of states to a rank.
+    /// A rank for a state is valid if it is inferior than the rank of its
+    /// predecessor.
+    /// When the rank is odd, its has an acceptance condition associated that
+    /// must not be in its associated state.
+    /// \return false if there is not valid rank as successor.
+    bool tgba_complement_succ_iterator::next_valid_rank()
+    {
+      state_rank_map::const_iterator i;
+      do {
+        for (i = current_ranks_.begin();
+             i != current_ranks_.end();
+             ++i)
+        {
+          if (i->second.rank != 0)
+          {
+            if (i->second.rank & 1)
+            {
+              if (i->second.condition.order() == 0)
+                --i->second.rank;
+              else
+                i->second.condition =
+                  acc_list_[i->second.condition.order() - 1];
+            }
+            else
+            {
+              --i->second.rank;
+              i->second.condition = acc_list_[acc_list_.size() - 1];
+            }
+            break;
+          }
+          else
+          {
+            current_ranks_[i->first] = highest_current_ranks_[i->first];
+          }
+        }
+      }
+      while ((i != current_ranks_.end()) && !is_valid_rank());
+
+      return i != current_ranks_.end();
+    }
+
+    /// \brief Create the highest rank of \a origin_ as origin and
+    /// \a condition as successor condition.
+    void
+    tgba_complement_succ_iterator::successor_highest_rank(bdd condition)
+    {
+      // Highest rank for bdd.
+      state_rank_map sr_map = origin_->get_state_map();
+      highest_current_ranks_.clear();
+
+      for (state_rank_map::const_iterator i = sr_map.begin();
+           i != sr_map.end();
+           ++i)
+      {
+        tgba_succ_iterator* iterator = automaton_->succ_iter(i->first.get());
+        for (iterator->first(); !iterator->done(); iterator->next())
+        {
+          bdd c = iterator->current_condition();
+          if ((c & condition) != bddfalse)
+          {
+            shared_state s(iterator->current_state());
+            if (highest_current_ranks_.find(s) != highest_current_ranks_.end())
+            {
+              if (i->second < highest_current_ranks_[s])
+                highest_current_ranks_[s] = i->second;
+            }
+            else
+              highest_current_ranks_[s] = i->second;
+          }
+        }
+        delete iterator;
+      }
+
+      // Highest $O$ set of the algorithm.
+      state_set s_set = origin_->get_filter_set();
+      highest_state_set_.clear();
+
+      for (state_set::const_iterator i = s_set.begin();
+           i != s_set.end();
+           ++i)
+      {
+        tgba_succ_iterator* iterator = automaton_->succ_iter(i->get());
+        for (iterator->first(); !iterator->done(); iterator->next())
+        {
+          bdd c = iterator->current_condition();
+          if ((c & condition) != bddfalse)
+          {
+            shared_state s(iterator->current_state());
+            highest_state_set_.insert(s);
+          }
+        }
+        delete iterator;
+      }
+
+      current_ranks_ = highest_current_ranks_;
+    }
+
+    void
+    tgba_complement_succ_iterator::first()
+    {
+      current_condition_ = condition_list_.begin();
+      if (done())
+        return;
+
+      successor_highest_rank(*current_condition_);
+
+      if (!is_valid_rank())
+        next_valid_rank();
+    }
+
+    void
+    tgba_complement_succ_iterator::next()
+    {
+      if (done())
+        return;
+
+      if (!next_valid_rank())
+      {
+        ++current_condition_;
+        if (!done())
+        {
+          successor_highest_rank(*current_condition_);
+          if (!is_valid_rank())
+            next_valid_rank();
+        }
+      }
+    }
+
+    bool
+    tgba_complement_succ_iterator::done() const
+    {
+      return (current_condition_ == condition_list_.end());
+    }
+
+    state_complement*
+    tgba_complement_succ_iterator::current_state() const
+    {
+      if (done())
+        return 0;
+
+      // If the filter set is empty, all the states of the map
+      // that are associated to an even rank create the new filter set.
+      state_set filter;
+      if (origin_->get_filter_set().empty())
+      {
+        for (state_rank_map::const_iterator i = current_ranks_.begin();
+             i != current_ranks_.end();
+             ++i)
+          if (!(i->second.rank & 1))
+            filter.insert(i->first);
+      }
+      else
+      {
+        // It the filter set is non-empty, we delete from this set states
+        // that are now associated to an odd rank.
+        for (state_set::const_iterator i = highest_state_set_.begin();
+             i != highest_state_set_.end();
+             ++i)
+        {
+          state_rank_map::const_iterator s(current_ranks_.find(*i));
+          assert(s != current_ranks_.end());
+
+          if (!(s->second.get_rank() & 1))
+            filter.insert(*i);
+        }
+      }
+
+      return new state_complement(current_ranks_, filter);
+    }
+
+    bdd
+    tgba_complement_succ_iterator::current_condition() const
+    {
+      if (done())
+        return bddfalse;
+      return *current_condition_;
+    }
+
+    bdd
+    tgba_complement_succ_iterator::current_acceptance_conditions() const
+    {
+      if (done())
+        return bddfalse;
+
+      // This algorithm doesn't generalized acceptance conditions.
+      if (origin_->accepting())
+        return the_acceptance_cond_;
+      else
+        return bddfalse;
+    }
+
+  } // end namespace anonymous.
+
+  /// Retrieve all the atomic acceptance conditions of the automaton.
+  /// They are inserted into \a acc_list_.
+  void
+  tgba_complement::get_acc_list()
+  {
+    bdd c = automaton_->all_acceptance_conditions();
+    bdd current = bdd_satone(c);
+    unsigned i = 0;
+    while (current != bddtrue && current != bddfalse)
+    {
+      acc_list_.push_back(bdd_ordered(bdd_var(current), i));
+      ++i;
+      bdd high = bdd_high(current);
+      if (high == bddfalse)
+        current = bdd_low(current);
+      else
+        current = high;
+    }
+  }
+
+  tgba_complement::tgba_complement(const tgba* a)
+    : automaton_(new tgba_sgba_proxy(a))
+  {
+    get_dict()->register_all_variables_of(automaton_, this);
+    int v = get_dict()
+      ->register_acceptance_variable(ltl::constant::true_instance(), this);
+    the_acceptance_cond_ = bdd_ithvar(v);
+    {
+      count_states count(automaton_);
+      nb_states_ = count.size();
+    }
+    get_acc_list();
+  }
+
+  tgba_complement::~tgba_complement()
+  {
+    get_dict()->unregister_all_my_variables(this);
+    delete automaton_;
+  }
+
+  state*
+  tgba_complement::get_init_state() const
+  {
+    state_complement* init = new state_complement();
+    rank_t r = {2 * nb_states_, bdd_ordered()};
+    init->add(shared_state(automaton_->get_init_state()), r);
+    return init;
+  }
+
+  tgba_succ_iterator*
+  tgba_complement::succ_iter(const state* local_state,
+                             const state*,
+                             const tgba*) const
+  {
+    const state_complement* state =
+      dynamic_cast<const state_complement*>(local_state);
+    assert(state);
+
+    return new tgba_complement_succ_iterator(automaton_,
+                                             the_acceptance_cond_,
+                                             acc_list_, state);
+  }
+
+  bdd_dict*
+  tgba_complement::get_dict() const
+  {
+    return automaton_->get_dict();
+  }
+
+  std::string
+  tgba_complement::format_state(const state* state) const
+  {
+    const state_complement* s = dynamic_cast<const state_complement*>(state);
+    assert(s);
+    std::ostringstream ss;
+    ss << "{ set: {" << std::endl;
+
+    const state_rank_map& state_map = s->get_state_map();
+    const state_set& state_filter = s->get_filter_set();
+
+    for (state_rank_map::const_iterator i = state_map.begin();
+         i != state_map.end();
+         ++i)
+    {
+      ss << "  {" << automaton_->format_state(i->first.get())
+         << ", " << i->second.format() << "}" << std::endl;
+    }
+    ss << "} odd-less: {";
+
+    for (state_set::const_iterator i = state_filter.begin();
+         i != state_filter.end();
+         ++i)
+    {
+      ss << "  " << automaton_->format_state(i->get()) << std::endl;
+    }
+
+    ss << "} }";
+    return ss.str();
+  }
+
+  bdd
+  tgba_complement::all_acceptance_conditions() const
+  {
+    return the_acceptance_cond_;
+  }
+
+  bdd
+  tgba_complement::neg_acceptance_conditions() const
+  {
+    return !the_acceptance_cond_;
+  }
+
+  bdd
+  tgba_complement::compute_support_conditions(const state* state) const
+  {
+    tgba_succ_iterator* i = succ_iter(state);
+    bdd result = bddtrue;
+    for (i->first(); !i->done(); i->next())
+      result |= i->current_condition();
+    delete i;
+    return result;
+  }
+
+  bdd
+  tgba_complement::compute_support_variables(const state* state) const
+  {
+    tgba_succ_iterator* i = succ_iter(state);
+    bdd result = bddtrue;
+    for (i->first(); !i->done(); i->next())
+      result &= bdd_support(i->current_condition());
+    delete i;
+    return result;
+  }
+
+} // end namespace spot.

src/tgba/tgbacomplement.hh

@@ -0,0 +1,99 @@
+#ifndef SPOT_TGBA_TGBACOMPLEMENT_HH
+#define SPOT_TGBA_TGBACOMPLEMENT_HH
+
+#include <vector>
+#include "bdd.h"
+#include "tgba.hh"
+#include "tgba/tgbasgba.hh"
+
+namespace spot
+{
+  class bdd_ordered
+  {
+  public:
+    bdd_ordered()
+      : order_(0)
+    {};
+
+    bdd_ordered(int bdd_, unsigned order_)
+      : bdd_(bdd_), order_(order_)
+    {
+    }
+
+    unsigned order() const
+    {
+      return order_;
+    }
+
+    unsigned& order()
+    {
+      return order_;
+    }
+
+    bdd get_bdd() const
+    {
+      return bdd_ithvar(bdd_);
+    }
+  private:
+    int bdd_;
+    unsigned order_;
+  };
+
+  typedef std::vector<bdd_ordered> acc_list_t;
+
+  /// \brief Build a complemented automaton.
+  /// \ingroup tgba
+  ///
+  /// The construction comes from:
+  /// @Article{         kupferman.05.tcs,
+  ///   title           = {{From complementation to certification}},
+  ///   author          = {Kupferman, O. and Vardi, M.Y.},
+  ///   journal         = {Theoretical Computer Science},
+  ///   volume  	= {345},
+  ///   number          = {1},
+  ///   pages		= {83--100},
+  ///   year		= {2005},
+  ///   publisher	= {Elsevier}
+  /// }
+  ///
+  /// The original automaton is used as a States-based Generalized
+  /// Büchi Automaton.
+  ///
+  /// The construction is done on-the-fly, by the
+  /// \c tgba_complement_succ_iterator class.
+  /// \see tgba_complement_succ_iteratora
+  class tgba_complement : public tgba
+  {
+  public:
+    tgba_complement(const tgba* a);
+    virtual ~tgba_complement();
+
+    // tgba interface
+    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_acceptance_conditions() const;
+    virtual bdd neg_acceptance_conditions() const;
+  protected:
+    virtual bdd compute_support_conditions(const state* state) const;
+    virtual bdd compute_support_variables(const state* state) const;
+  private:
+    /// Retrieve all the atomic acceptance conditions of the automaton.
+    /// They are inserted into \a acc_list_.
+    void get_acc_list();
+  private:
+    const tgba_sgba_proxy* automaton_;
+    bdd the_acceptance_cond_;
+    unsigned nb_states_;
+    acc_list_t acc_list_;
+  }; // end class tgba_complement.
+
+} // end namespace spot.
+
+
+#endif  // !SPOT_TGBA_TGBACOMPLEMENT_HH

src/tgbatest/Makefile.am

@@ -31,7 +31,7 @@ check_SCRIPTS = defs
 # Keep this sorted alphabetically.
 check_PROGRAMS = \
   bddprod \
-  safracomplement \
+  complement \
   explicit \
   expldot \
   explprod \

src/tgbatest/complementation.cc

@@ -16,18 +16,22 @@
 #include "tgba/tgbatba.hh"
 
 #include "tgba/tgbasafracomplement.hh"
+#include "tgba/tgbacomplement.hh"
 
 void usage(const char* prog)
 {
   std::cout << "usage: " << prog << " [options]" << std::endl;
   std::cout << "with options" << std::endl
+            << "-S                      Use safra complementation"
+            << std::endl
             << "-s     buchi_automaton  display the safra automaton"
             << std::endl
             << "-a     buchi_automaton  display the complemented automaton"
             << std::endl
             << "-astat buchi_automaton  statistics for !a" << std::endl
             << "-fstat formula          statistics for !A_f" << std::endl
-            << "-f     formula          test !A_f and !A_!f" << std::endl;
+            << "-f     formula          test !A_f and !A_!f" << std::endl
+            << "-p     formula          print the automaton for f" << std::endl;
 }
 
 int main(int argc, char* argv[])
@@ -40,6 +44,8 @@ int main(int argc, char* argv[])
   bool stats = false;
   bool formula = false;
   bool automaton = false;
+  bool safra = false;
+  bool print_formula = false;
 
   if (argc < 3)
   {
@@ -67,12 +73,16 @@ int main(int argc, char* argv[])
 
       switch (argv[i][1])
       {
+        case 'S':
+          safra = true; break;
         case 's':
-          print_safra = true; break;
+          safra = true; print_safra = true; break;
         case 'a':
           print_automaton = true; break;
         case 'f':
           check = true; break;
+        case 'p':
+          print_formula = true; break;
         default:
           std::cerr << "unrecognized option `-" << argv[i][1]
                     << "'" << std::endl;
@@ -98,14 +108,46 @@ int main(int argc, char* argv[])
     if (spot::format_tgba_parse_errors(std::cerr, file, pel))
       return 2;
 
-    spot::tgba_safra_complement* complement =
+    spot::tgba* complement = 0;
-      new spot::tgba_safra_complement(a);
+
+    if (safra)
+      complement = new spot::tgba_safra_complement(a);
+    else
+      complement = new spot::tgba_complement(a);
 
     if (print_automaton)
       spot::dotty_reachable(std::cout, complement);
 
     if (print_safra)
-      spot::display_safra(complement);
+    {
+      spot::tgba_safra_complement* safra_complement =
+        dynamic_cast<spot::tgba_safra_complement*>(complement);
+      spot::display_safra(safra_complement);
+    }
+    delete complement;
+    delete a;
+  }
+  else if (print_formula)
+  {
+    spot::tgba* a;
+    spot::ltl::formula* f1 = 0;
+
+    spot::ltl::parse_error_list p1;
+    f1 = spot::ltl::parse(file, p1);
+
+    if (spot::ltl::format_parse_errors(std::cerr, file, p1))
+      return 2;
+
+    a = spot::ltl_to_tgba_fm(f1, dict);
+
+    spot::tgba* complement = 0;
+    if (safra)
+      complement = new spot::tgba_safra_complement(a);
+    else
+      complement = new spot::tgba_complement(a);
+
+    spot::dotty_reachable(std::cout, complement);
+    spot::ltl::destroy(f1);
     delete complement;
     delete a;
   }
@@ -133,7 +175,7 @@ int main(int argc, char* argv[])
         return 2;
     }
 
-    spot::tgba_safra_complement* complement =
+    spot::tgba_safra_complement* safra_complement =
       new spot::tgba_safra_complement(a);
 
     spot::tgba_statistics a_size =  spot::stats_reachable(a);
@@ -152,8 +194,18 @@ int main(int argc, char* argv[])
               << std::endl;
     delete buchi;
 
-    spot::tgba_statistics b_size =  spot::stats_reachable(complement);
+    spot::tgba_statistics b_size =  spot::stats_reachable(safra_complement);
-    std::cout << "Complement: "
+    std::cout << "Safra Complement: "
+              << b_size.states << ", "
+              << b_size.transitions << ", "
+              << safra_complement->number_of_acceptance_conditions()
+              << std::endl;
+
+    spot::tgba_complement* complement =
+      new spot::tgba_complement(a);
+
+    b_size =  spot::stats_reachable(complement);
+    std::cout << "GBA Complement: "
               << b_size.states << ", "
               << b_size.transitions << ", "
               << complement->number_of_acceptance_conditions()
@@ -191,8 +243,19 @@ int main(int argc, char* argv[])
     spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not,
                                                         spot::ltl::clone(f1));
     spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict);
-    spot::tgba_safra_complement* nAf = new spot::tgba_safra_complement(Af);
+
-    spot::tgba_safra_complement* nAnf = new spot::tgba_safra_complement(Anf);
+    spot::tgba* nAf;
+    spot::tgba* nAnf;
+    if (safra)
+    {
+      nAf = new spot::tgba_safra_complement(Af);
+      nAnf = new spot::tgba_safra_complement(Anf);
+    }
+    else
+    {
+      nAf = new spot::tgba_complement(Af);
+      nAnf = new spot::tgba_complement(Anf);
+    }
     spot::tgba* prod = new spot::tgba_product(nAf, nAnf);
     spot::emptiness_check* ec = spot::couvreur99(prod);
     spot::emptiness_check_result* res = ec->check();

src/tgbatest/complementation.test

@@ -26,6 +26,7 @@ set -e
 
 while read f; do
     run 0 ../complement -f "$f"
+    run 0 ../complement -S -f "$f"
 done <<EOF
 GFa
 FGa