Preliminary implementation of Testing Automata.

* configure.ac: Generate src/ta/Makefile and src/taalgos/Makefile.
* src/Makefile.am (SUBDIRS): Add them.
* src/tgbatest/ltl2tgba.cc (main): Add option -TA.
* src/ta/Makefile.am, src/ta/ta.hh, src/ta/taexplicit.cc,
src/ta/taexplicit.hh, src/taalgos/Makefile.am,
src/taalgos/dotty.cc, src/taalgos/dotty.hh,
src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
src/taalgos/sba2ta.cc, src/taalgos/sba2ta.hh: New files.

configure.ac

@@ -154,6 +154,8 @@ AC_CONFIG_FILES([
   src/tgbaalgos/gtec/Makefile
   src/tgbaalgos/Makefile
   src/tgba/Makefile
+  src/taalgos/Makefile
+  src/ta/Makefile
   src/tgbaparse/Makefile
   src/tgbatest/defs
   src/tgbatest/Makefile

src/Makefile.am

@@ -1,7 +1,8 @@
-## Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
+## -*- coding: utf-8 -*-
+## Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
 ## de l'Epita (LRDE).
 ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
-## département Systèmes Répartis Coopératifs (SRC), Université Pierre
+## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
 ##
 ## This file is part of Spot, a model checking library.
@@ -25,11 +26,12 @@ AUTOMAKE_OPTIONS = subdir-objects
 
 # List directories in the order they must be built.  Keep tests at the
 # end, after building '.' (since the current directory contains
-# libspot.la needed by the tests).
+# libspot.la needed by the tests)
 SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba		\
-          tgbaalgos tgbaparse evtgba evtgbaalgos evtgbaparse kripke	\
+          tgbaalgos tgbaparse ta taalgos evtgba evtgbaalgos		\
-          saba sabaalgos neverparse kripkeparse . ltltest eltltest      \
+          evtgbaparse kripke saba sabaalgos neverparse kripkeparse	\
-	  tgbatest evtgbatest sabatest sanity kripketest
+          . ltltest eltltest tgbatest evtgbatest sabatest sanity	\
+          kripketest
 
 lib_LTLIBRARIES = libspot.la
 libspot_la_SOURCES =
@@ -43,6 +45,8 @@ libspot_la_LIBADD =  \
   eltlparse/libeltlparse.la \
   tgba/libtgba.la \
   tgbaalgos/libtgbaalgos.la \
+  ta/libta.la \
+  taalgos/libtaalgos.la \
   tgbaparse/libtgbaparse.la \
   neverparse/libneverparse.la \
   evtgba/libevtgba.la \

src/ta/Makefile.am

@@ -0,0 +1,32 @@
+## Copyright (C) 2010 Laboratoire de Recherche et Développement
+## de l'Epita (LRDE).
+##
+## This file is part of Spot, a model checking library.
+##
+## Spot is free software; you can redistribute it and/or modify it
+## under the terms of the GNU General Public License as published by
+## the Free Software Foundation; either version 2 of the License, or
+## (at your option) any later version.
+##
+## Spot is distributed in the hope that it will be useful, but WITHOUT
+## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+## or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+## License for more details.
+##
+## You should have received a copy of the GNU General Public License
+## along with Spot; see the file COPYING.  If not, write to the Free
+## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+## 02111-1307, USA.
+
+AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+tadir = $(pkgincludedir)/ta
+
+ta_HEADERS = \
+  ta.hh \
+  taexplicit.hh
+
+noinst_LTLIBRARIES = libta.la
+libta_la_SOURCES = \
+  taexplicit.cc

src/ta/ta.hh

@@ -0,0 +1,158 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TA_TA_HH
+# define SPOT_TA_TA_HH
+
+#include <set>
+
+#include <cassert>
+#include "misc/bddlt.hh"
+#include "tgba/state.hh"
+#include "tgba/succiter.hh"
+#include "tgba/bdddict.hh"
+
+namespace spot
+{
+  // Forward declarations.  See below.
+  class ta_succ_iterator;
+
+  /// ta representation of a Testing Automata
+  class ta
+  {
+
+  public:
+    virtual
+    ~ta()
+    {
+    }
+
+    typedef std::set<state*, state_ptr_less_than> states_set_t;
+
+    virtual const states_set_t*
+    get_initial_states_set() const  = 0;
+
+    virtual ta_succ_iterator*
+    succ_iter(const spot::state* s) const  = 0;
+
+    virtual bdd_dict*
+    get_dict() const  = 0;
+
+    virtual std::string
+    format_state(const spot::state* s) const  = 0;
+
+    virtual bool
+    is_accepting_state(const spot::state* s) const  = 0;
+
+    virtual bool
+    is_livelock_accepting_state(const spot::state* s) const  = 0;
+
+    virtual bool
+    is_initial_state(const spot::state* s) const  = 0;
+
+    virtual bdd
+    get_state_condition(const spot::state* s) const  = 0;
+
+  };
+
+  /// Successor iterators used by spot::ta.
+  class ta_succ_iterator : public tgba_succ_iterator
+  {
+  public:
+    virtual
+    ~ta_succ_iterator()
+    {
+    }
+
+    virtual void
+    first() = 0;
+    virtual void
+    next() = 0;
+    virtual bool
+    done() const = 0;
+
+    virtual state*
+    current_state() const = 0;
+    virtual bdd
+    current_condition() const = 0;
+
+
+    bdd
+    current_acceptance_conditions() const
+    {
+      assert(!done());
+      return bddfalse;
+    }
+  };
+
+  // A stack of Strongly-Connected Components
+  class sscc_stack
+  {
+  public:
+    struct connected_component
+    {
+    public:
+      connected_component(int index = -1);
+
+      /// Index of the SCC.
+      int index;
+
+      bool is_accepting;
+
+      bool is_initial;
+
+      std::list<state*> rem;
+    };
+
+    /// Stack a new SCC with index \a index.
+    void
+    push(int index);
+
+    /// Access the top SCC.
+    connected_component&
+    top();
+
+    /// Access the top SCC.
+    const connected_component&
+    top() const;
+
+    /// Pop the top SCC.
+    void
+    pop();
+
+    /// How many SCC are in stack.
+    size_t
+    size() const;
+
+    /// The \c rem member of the top SCC.
+    std::list<state*>&
+    rem();
+
+    /// Is the stack empty?
+    bool
+    empty() const;
+
+    typedef std::list<connected_component> stack_type;
+    stack_type s;
+  };
+
+}
+
+#endif // SPOT_TA_TA_HH

src/ta/taexplicit.cc

@@ -0,0 +1,379 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "ltlast/atomic_prop.hh"
+#include "ltlast/constant.hh"
+#include "taexplicit.hh"
+#include "tgba/formula2bdd.hh"
+#include "misc/bddop.hh"
+#include <cassert>
+#include "ltlvisit/tostring.hh"
+
+#include "tgba/bddprint.hh"
+
+
+namespace spot
+{
+
+  ////////////////////////////////////////
+  // ta_explicit_succ_iterator
+
+  ta_explicit_succ_iterator::ta_explicit_succ_iterator(const state_ta_explicit* s)
+  {
+    transitions_ = s->get_transitions();
+  }
+
+  void
+  ta_explicit_succ_iterator::first()
+  {
+    i_ = transitions_->begin();
+  }
+
+  void
+  ta_explicit_succ_iterator::next()
+  {
+    ++i_;
+  }
+
+  bool
+  ta_explicit_succ_iterator::done() const
+  {
+    return i_ == transitions_->end();
+  }
+
+  state*
+  ta_explicit_succ_iterator::current_state() const
+  {
+    assert(!done());
+    state_ta_explicit* s = (*i_)->dest;
+    return s;
+  }
+
+  bdd
+  ta_explicit_succ_iterator::current_condition() const
+  {
+    assert(!done());
+    return (*i_)->condition;
+  }
+
+
+
+
+  ////////////////////////////////////////
+  // state_ta_explicit
+
+  state_ta_explicit::transitions*
+  state_ta_explicit::get_transitions() const
+  {
+    return transitions_;
+  }
+
+
+  void
+  state_ta_explicit::add_transition(state_ta_explicit::transition* t){
+    if(transitions_ == 0)
+      transitions_= new transitions;
+
+    transitions_->push_back(t);
+
+  }
+
+
+  const state*
+  state_ta_explicit::get_tgba_state() const
+  {
+    return tgba_state_;
+  }
+
+  const bdd
+  state_ta_explicit::get_tgba_condition() const
+  {
+    return tgba_condition_;
+  }
+
+  bool
+  state_ta_explicit::is_accepting_state() const
+  {
+    return is_accepting_state_;
+  }
+
+  bool
+  state_ta_explicit::is_initial_state() const
+  {
+    return is_initial_state_;
+  }
+
+  void
+  state_ta_explicit::set_accepting_state(bool is_accepting_state)
+  {
+    is_accepting_state_ = is_accepting_state;
+  }
+
+  bool
+  state_ta_explicit::is_livelock_accepting_state() const
+  {
+    return is_livelock_accepting_state_;
+  }
+
+  void
+  state_ta_explicit::set_livelock_accepting_state(bool is_livelock_accepting_state)
+  {
+    is_livelock_accepting_state_ = is_livelock_accepting_state;
+  }
+
+  void
+  state_ta_explicit::set_initial_state(bool is_initial_state)
+  {
+    is_initial_state_ = is_initial_state;
+  }
+
+  int
+  state_ta_explicit::compare(const spot::state* other) const
+  {
+    const state_ta_explicit* o = dynamic_cast<const state_ta_explicit*> (other);
+    assert(o);
+
+    int compare_value = tgba_state_->compare(o->tgba_state_);
+
+    if (compare_value != 0)
+      return compare_value;
+
+    return tgba_condition_.id() - o->tgba_condition_.id();
+  }
+
+  size_t
+  state_ta_explicit::hash() const
+  {
+    return wang32_hash(tgba_state_->hash()) ^ wang32_hash(tgba_condition_.id());
+  }
+
+  state_ta_explicit*
+  state_ta_explicit::clone() const
+  {
+    return new state_ta_explicit(*this);
+  }
+
+  sscc_stack::connected_component::connected_component(int i)
+  {
+    index = i;
+    is_accepting = false;
+    is_initial = false;
+  }
+
+  sscc_stack::connected_component&
+  sscc_stack::top()
+  {
+    return s.front();
+  }
+
+  const sscc_stack::connected_component&
+  sscc_stack::top() const
+  {
+    return s.front();
+  }
+
+  void
+  sscc_stack::pop()
+  {
+    // assert(rem().empty());
+    s.pop_front();
+  }
+
+  void
+  sscc_stack::push(int index)
+  {
+    s.push_front(connected_component(index));
+  }
+
+  std::list<state*>&
+  sscc_stack::rem()
+  {
+    return top().rem;
+  }
+
+  size_t
+  sscc_stack::size() const
+  {
+    return s.size();
+  }
+
+  bool
+  sscc_stack::empty() const
+  {
+    return s.empty();
+  }
+
+  ////////////////////////////////////////
+  // ta_explicit
+
+
+  ta_explicit::ta_explicit(const tgba* tgba_) :
+    tgba_(tgba_)
+  {
+  }
+
+  ta_explicit::~ta_explicit()
+  {
+    ta::states_set_t::iterator it;
+    for (it = states_set_.begin(); it != states_set_.end(); it++)
+      {
+        const state_ta_explicit* s = dynamic_cast<const state_ta_explicit*> (*it);
+        state_ta_explicit::transitions* trans = s->get_transitions();
+        state_ta_explicit::transitions::iterator it_trans;
+        // We don't destroy the transitions in the state's destructor because
+        // they are not cloned.
+        for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++)
+          {
+            delete *it_trans;
+          }
+        delete trans;
+        delete s->get_tgba_state();
+        delete s;
+      }
+
+  }
+
+  state_ta_explicit*
+  ta_explicit::add_state(state_ta_explicit* s)
+  {
+    std::pair<ta::states_set_t::iterator, bool> add_state_to_ta =
+        states_set_.insert(s);
+
+    if (is_initial_state(*add_state_to_ta.first))
+      initial_states_set_.insert(*add_state_to_ta.first);
+
+    return dynamic_cast<state_ta_explicit*> (*add_state_to_ta.first);
+
+  }
+
+  state_ta_explicit*
+  ta_explicit::add_initial_state(state_ta_explicit* s)
+  {
+    s->set_initial_state(true);
+
+    return add_state(s);
+
+  }
+
+  void
+  ta_explicit::create_transition(state_ta_explicit* source, bdd condition, state_ta_explicit* dest)
+  {
+    state_ta_explicit::transition* t = new state_ta_explicit::transition;
+    t->dest = dest;
+    t->condition = condition;
+    source->add_transition(t);
+
+  }
+
+  const ta::states_set_t*
+  ta_explicit::get_initial_states_set() const
+  {
+    return &initial_states_set_;
+
+  }
+
+  bdd
+  ta_explicit::get_state_condition(const spot::state* initial_state) const
+  {
+    const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (initial_state);
+    return sta->get_tgba_condition();
+  }
+
+  bool
+  ta_explicit::is_accepting_state(const spot::state* s) const
+  {
+    const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (s);
+    return sta->is_accepting_state();
+  }
+
+  bool
+  ta_explicit::is_initial_state(const spot::state* s) const
+  {
+    const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (s);
+    return sta->is_initial_state();
+  }
+
+  bool
+  ta_explicit::is_livelock_accepting_state(const spot::state* s) const
+  {
+    const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (s);
+    return sta->is_livelock_accepting_state();
+  }
+
+  ta_succ_iterator*
+  ta_explicit::succ_iter(const spot::state* state) const
+  {
+    const state_ta_explicit* s = dynamic_cast<const state_ta_explicit*> (state);
+    assert(s);
+    return new ta_explicit_succ_iterator(s);
+  }
+
+  bdd_dict*
+  ta_explicit::get_dict() const
+  {
+    return tgba_->get_dict();
+  }
+
+  const tgba*
+  ta_explicit::get_tgba() const
+  {
+    return tgba_;
+  }
+
+  std::string
+  ta_explicit::format_state(const spot::state* s) const
+  {
+    const state_ta_explicit* sta = dynamic_cast<const state_ta_explicit*> (s);
+    assert(sta);
+    return tgba_->format_state(sta->get_tgba_state()) + "\n"
+        + bdd_format_formula(get_dict(), sta->get_tgba_condition());
+
+  }
+
+  void
+  ta_explicit::delete_stuttering_transitions()
+  {
+    ta::states_set_t::iterator it;
+    for (it = states_set_.begin(); it != states_set_.end(); it++)
+      {
+
+        const state_ta_explicit* source = dynamic_cast<const state_ta_explicit*> (*it);
+
+        state_ta_explicit::transitions* trans = source->get_transitions();
+        state_ta_explicit::transitions::iterator it_trans;
+
+        for (it_trans = trans->begin(); it_trans != trans->end();)
+          {
+            if (source->get_tgba_condition()
+                == ((*it_trans)->dest)->get_tgba_condition())
+              {
+                delete *it_trans;
+                it_trans = trans->erase(it_trans);
+              }
+            else
+              {
+                it_trans++;
+              }
+          }
+      }
+
+  }
+
+}

src/ta/taexplicit.hh

@@ -0,0 +1,197 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita_explicit (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANta_explicitBILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more deta_explicitils.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TA_TAEXPLICIT_HH
+# define SPOT_TA_TAEXPLICIT_HH
+
+#include "misc/hash.hh"
+#include <list>
+#include "tgba/tgba.hh"
+#include <set>
+#include "ltlast/formula.hh"
+#include <cassert>
+#include "misc/bddlt.hh"
+#include "ta.hh"
+
+namespace spot
+{
+  // Forward declarations.  See below.
+  class state_ta_explicit;
+  class ta_explicit_succ_iterator;
+  class ta_explicit;
+
+
+
+  /// ta_explicit explicit representa_explicittion of a Testing Automata_explicit
+  class ta_explicit : public ta
+  {
+  public:
+    ta_explicit(const tgba* tgba_);
+
+    const tgba*
+    get_tgba() const;
+
+    state_ta_explicit*
+    add_state(state_ta_explicit* s);
+
+    state_ta_explicit*
+    add_initial_state(state_ta_explicit* s);
+
+    void
+    create_transition(state_ta_explicit* source, bdd condition, state_ta_explicit* dest);
+
+    void
+    delete_stuttering_transitions();
+    // ta interface
+    virtual
+    ~ta_explicit();
+    virtual const states_set_t*
+    get_initial_states_set() const;
+
+    virtual ta_succ_iterator*
+    succ_iter(const spot::state* s) const;
+
+    virtual bdd_dict*
+    get_dict() const;
+
+    virtual std::string
+    format_state(const spot::state* s) const;
+
+    virtual bool
+    is_accepting_state(const spot::state* s) const;
+
+    virtual bool
+    is_livelock_accepting_state(const spot::state* s) const;
+
+    virtual bool
+    is_initial_state(const spot::state* s) const;
+
+    virtual bdd
+    get_state_condition(const spot::state* s) const;
+
+  private:
+    // Disallow copy.
+    ta_explicit(const ta_explicit& other);
+    ta_explicit&
+    operator=(const ta_explicit& other);
+
+    ta::states_set_t states_set_;
+    ta::states_set_t initial_states_set_;
+    const tgba* tgba_;
+
+  };
+
+  /// states used by spot::ta_explicit.
+  /// \ingroup ta_
+  class state_ta_explicit : public spot::state
+  {
+  public:
+
+    struct transition
+    {
+      bdd condition;
+      state_ta_explicit* dest;
+    };
+
+    typedef std::list<transition*> transitions;
+
+    state_ta_explicit(const state* tgba_state, const bdd tgba_condition,
+        bool is_initial_state = false, bool is_accepting_state = false,
+        bool is_livelock_accepting_state = false, transitions* trans = 0) :
+      tgba_state_(tgba_state), tgba_condition_(tgba_condition),
+          is_initial_state_(is_initial_state), is_accepting_state_(
+              is_accepting_state), is_livelock_accepting_state_(
+              is_livelock_accepting_state), transitions_(trans)
+    {
+    }
+
+    virtual int
+    compare(const spot::state* other) const;
+    virtual size_t
+    hash() const;
+    virtual state_ta_explicit*
+    clone() const;
+
+    virtual
+    ~state_ta_explicit()
+    {
+    }
+
+    transitions*
+    get_transitions() const;
+
+    void
+    add_transition(transition* t);
+
+    const state*
+    get_tgba_state() const;
+    const bdd
+    get_tgba_condition() const;
+    bool
+    is_accepting_state() const;
+    void
+    set_accepting_state(bool is_accepting_state);
+    bool
+    is_livelock_accepting_state() const;
+    void
+    set_livelock_accepting_state(bool is_livelock_accepting_state);
+    bool
+    is_initial_state() const;
+    void
+    set_initial_state(bool is_initial_state);
+
+  private:
+    const state* tgba_state_;
+    const bdd tgba_condition_;
+    bool is_initial_state_;
+    bool is_accepting_state_;
+    bool is_livelock_accepting_state_;
+    transitions* transitions_;
+
+  };
+
+  /// Successor iterators used by spot::ta_explicit.
+  class ta_explicit_succ_iterator : public ta_succ_iterator
+  {
+  public:
+    ta_explicit_succ_iterator(const state_ta_explicit* s);
+
+    virtual void
+    first();
+    virtual void
+    next();
+    virtual bool
+    done() const;
+
+    virtual state*
+    current_state() const;
+    virtual bdd
+    current_condition() const;
+
+
+
+  private:
+    state_ta_explicit::transitions* transitions_;
+    state_ta_explicit::transitions::const_iterator i_;
+  };
+
+}
+
+#endif // SPOT_TA_TAEXPLICIT_HH

src/taalgos/Makefile.am

@@ -0,0 +1,37 @@
+## Copyright (C) 2010 Laboratoire de Recherche et Développement
+## de l'Epita (LRDE).
+##
+## This file is part of Spot, a model checking library.et Marie Curie.
+##
+## Spot is free software; you can redistribute it and/or modify it
+## under the terms of the GNU General Public License as published by
+## the Free Software Foundation; either version 2 of the License, or
+## (at your option) any later version.
+##
+## Spot is distributed in the hope that it will be useful, but WITHOUT
+## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+## or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+## License for more details.
+##
+## You should have received a copy of the GNU General Public License
+## along with Spot; see the file COPYING.  If not, write to the Free
+## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+## 02111-1307, USA.
+
+
+AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS)
+AM_CXXFLAGS = $(WARNING_CXXFLAGS)
+
+taalgosdir = $(pkgincludedir)/taalgos
+
+taalgos_HEADERS = \
+	sba2ta.hh \
+	dotty.hh \
+	reachiter.hh
+
+noinst_LTLIBRARIES = libtaalgos.la
+libtaalgos_la_SOURCES = \
+	sba2ta.cc \
+	dotty.cc \
+	reachiter.cc
+

src/taalgos/dotty.cc

@@ -0,0 +1,127 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <ostream>
+#include "dotty.hh"
+#include "tgba/bddprint.hh"
+#include "reachiter.hh"
+#include "misc/escape.hh"
+#include "misc/bareword.hh"
+
+namespace spot
+{
+  namespace
+  {
+    class dotty_bfs : public ta_reachable_iterator_breadth_first
+    {
+    public:
+      dotty_bfs(std::ostream& os, const ta* a) :
+        ta_reachable_iterator_breadth_first(a), os_(os)
+      {
+      }
+
+      void
+      start()
+      {
+        os_ << "digraph G {" << std::endl;
+
+        int n = 0;
+        const ta::states_set_t* init_states_set =
+            t_automata_->get_initial_states_set();
+        ta::states_set_t::const_iterator it;
+
+        for (it = (init_states_set->begin()); it != init_states_set->end(); it++)
+          {
+            //    cout << (*it).first << " => " << (*it).second << endl;
+
+            bdd init_condition = t_automata_->get_state_condition(*it);
+            std::string label = bdd_format_formula(t_automata_->get_dict(),
+                init_condition);
+            ++n;
+            os_ << -n << "  [label=\"\", style=invis, height=0]" << std::endl;
+            os_ << "  " << -n << " -> " << n << " " << "[label=\"" + label
+                + "\"]" << std::endl;
+
+          }
+      }
+
+      void
+      end()
+      {
+        os_ << "}" << std::endl;
+      }
+
+      void
+      process_state(const state* s, int n)
+      {
+
+        std::string shape = "ellipse";
+        std::string style = "solid";
+        if (t_automata_->is_accepting_state(s))
+          {
+            shape = "doublecircle";
+            style = "bold";
+          }
+
+        if (t_automata_->is_livelock_accepting_state(s))
+          {
+            shape = "octagon";
+            style = "bold";
+          }
+        if (t_automata_->is_livelock_accepting_state(s)
+            && t_automata_->is_accepting_state(s))
+          {
+            shape = "doubleoctagon";
+            style = "bold";
+          }
+
+        os_ << "  " << n << " [label=" << quote_unless_bare_word(
+            t_automata_->format_state(s)) << "]" << "[shape=\"" + shape + "\"]"
+            << "[style=\"" + style + "\"]" << std::endl;
+
+      }
+
+      void
+      process_link(int in, int out, const tgba_succ_iterator* si)
+      {
+
+        os_ << "  " << in << " -> " << out << " [label=\"";
+        escape_str(os_, bdd_format_accset(t_automata_->get_dict(),
+            si->current_condition()))
+
+        << "\"]" << std::endl;
+
+      }
+
+    private:
+      std::ostream& os_;
+    };
+
+  }
+
+  std::ostream&
+  dotty_reachable(std::ostream& os, const ta* a)
+  {
+    dotty_bfs d(os, a);
+    d.run();
+    return os;
+  }
+
+}

src/taalgos/dotty.hh

@@ -0,0 +1,35 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TAALGOS_DOTTY_HH
+# define SPOT_TAALGOS_DOTTY_HH
+
+#include "ta/ta.hh"
+#include <iosfwd>
+
+namespace spot
+{
+  class ta;
+
+  std::ostream&
+  dotty_reachable(std::ostream& os, const ta* a);
+}
+
+#endif // SPOT_TAALGOS_DOTTY_HH

src/taalgos/reachiter.cc

@@ -0,0 +1,176 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita (LRDE).
+//
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <cassert>
+#include "reachiter.hh"
+
+#include <iostream>
+using namespace std;
+
+namespace spot
+{
+  // ta_reachable_iterator
+  //////////////////////////////////////////////////////////////////////
+
+  ta_reachable_iterator::ta_reachable_iterator(const ta* a) :
+    t_automata_(a)
+  {
+  }
+  ta_reachable_iterator::~ta_reachable_iterator()
+  {
+    seen_map::const_iterator s = seen.begin();
+    while (s != seen.end())
+      {
+        // Advance the iterator before deleting the "key" pointer.
+        const state* ptr = s->first;
+        ++s;
+        delete ptr;
+      }
+  }
+
+  void
+  ta_reachable_iterator::run()
+  {
+    int n = 0;
+    start();
+    const ta::states_set_t* init_states_set =
+        t_automata_->get_initial_states_set();
+    ta::states_set_t::const_iterator it;
+
+    for (it = init_states_set->begin(); it != init_states_set->end(); it++)
+      {
+        state* init_state = (*it)->clone();
+        if (want_state(init_state))
+          add_state(init_state);
+        seen[init_state] = ++n;
+
+      }
+
+    const state* t;
+    while ((t = next_state()))
+      {
+        assert(seen.find(t) != seen.end());
+        int tn = seen[t];
+        tgba_succ_iterator* si = t_automata_->succ_iter(t);
+        process_state(t, tn);
+        for (si->first(); !si->done(); si->next())
+          {
+            const state* current = si->current_state()->clone();
+            seen_map::const_iterator s = seen.find(current);
+            bool ws = want_state(current);
+            if (s == seen.end())
+              {
+                seen[current] = ++n;
+                if (ws)
+                  {
+                    add_state(current);
+                    process_link(tn, n, si);
+                  }
+              }
+            else
+              {
+                if (ws)
+                  process_link(tn, s->second, si);
+                delete current;
+              }
+          }
+        delete si;
+      }
+    end();
+  }
+
+  bool
+  ta_reachable_iterator::want_state(const state*) const
+  {
+    return true;
+  }
+
+  void
+  ta_reachable_iterator::start()
+  {
+  }
+
+  void
+  ta_reachable_iterator::end()
+  {
+  }
+
+  void
+  ta_reachable_iterator::process_state(const state*, int)
+  {
+  }
+
+  void
+  ta_reachable_iterator::process_link(int, int, const tgba_succ_iterator*)
+  {
+  }
+
+  // ta_reachable_iterator_depth_first
+  //////////////////////////////////////////////////////////////////////
+
+  ta_reachable_iterator_depth_first::ta_reachable_iterator_depth_first(
+      const ta* a) :
+    ta_reachable_iterator(a)
+  {
+  }
+
+  void
+  ta_reachable_iterator_depth_first::add_state(const state* s)
+  {
+    todo.push(s);
+  }
+
+  const state*
+  ta_reachable_iterator_depth_first::next_state()
+  {
+    if (todo.empty())
+      return 0;
+    const state* s = todo.top();
+    todo.pop();
+    return s;
+  }
+
+  // ta_reachable_iterator_breadth_first
+  //////////////////////////////////////////////////////////////////////
+
+  ta_reachable_iterator_breadth_first::ta_reachable_iterator_breadth_first(
+      const ta* a) :
+    ta_reachable_iterator(a)
+  {
+  }
+
+  void
+  ta_reachable_iterator_breadth_first::add_state(const state* s)
+  {
+    todo.push_back(s);
+  }
+
+  const state*
+  ta_reachable_iterator_breadth_first::next_state()
+  {
+    if (todo.empty())
+      return 0;
+    const state* s = todo.front();
+    todo.pop_front();
+    return s;
+  }
+
+}

src/taalgos/reachiter.hh

@@ -0,0 +1,142 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita (LRDE).
+//
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TAALGOS_REACHITER_HH
+# define SPOT_TAALGOS_REACHITER_HH
+
+#include "misc/hash.hh"
+#include "ta/ta.hh"
+#include <stack>
+#include <deque>
+
+namespace spot
+{
+  /// \brief Iterate over all reachable states of a spot::ta.
+  /// \ingroup ta_generic
+  class ta_reachable_iterator
+  {
+  public:
+    ta_reachable_iterator(const ta* a);
+    virtual
+    ~ta_reachable_iterator();
+
+    /// \brief Iterate over all reachable states of a spot::ta.
+    ///
+    /// This is a template method that will call add_state(), next_state(),
+    /// start(), end(), process_state(), and process_link(), while it
+    /// iterates over states.
+    void
+    run();
+
+    /// \name Todo list management.
+    ///
+    /// spot::ta_reachable_iterator_depth_first and
+    /// spot::ta_reachable_iterator_breadth_first offer two precanned
+    /// implementations for these functions.
+    /// \{
+    /// \brief Called by run() to register newly discovered states.
+    virtual void
+    add_state(const state* s) = 0;
+    /// \brief Called by run() to obtain the next state to process.
+    virtual const state*
+    next_state() = 0;
+    /// \}
+
+    /// Called by add_state or next_states implementations to filter
+    /// states.  Default implementation always return true.
+    virtual bool
+    want_state(const state* s) const;
+
+    /// Called by run() before starting its iteration.
+    virtual void
+    start();
+    /// Called by run() once all states have been explored.
+    virtual void
+    end();
+
+    /// Called by run() to process a state.
+    ///
+    /// \param s The current state.
+    /// \param n A unique number assigned to \a s.
+    /// \param si The spot::ta_succ_iterator for \a s.
+    virtual void
+    process_state(const state* s, int n);
+    /// Called by run() to process a transition.
+    ///
+    /// \param in_s The source state
+    /// \param in The source state number.
+    /// \param out_s The destination state
+    /// \param out The destination state number.
+    /// \param si The spot::tgba_succ_iterator positionned on the current
+    ///             transition.
+    ///
+    /// The in_s and out_s states are owned by the
+    /// spot::ta_reachable_iterator instance and destroyed when the
+    /// instance is destroyed.
+    virtual void
+    process_link(int in, int out, const tgba_succ_iterator* si);
+
+  protected:
+
+    const ta* t_automata_; ///< The spot::ta to explore.
+
+    typedef Sgi::hash_map<const state*, int, state_ptr_hash, state_ptr_equal>
+        seen_map;
+    seen_map seen; ///< States already seen.
+  };
+
+  /// \brief An implementation of spot::ta_reachable_iterator that browses
+  /// states depth first.
+  /// \ingroup ta_generic
+  class ta_reachable_iterator_depth_first : public ta_reachable_iterator
+  {
+  public:
+    ta_reachable_iterator_depth_first(const ta* a);
+
+    virtual void
+    add_state(const state* s);
+    virtual const state*
+    next_state();
+
+  protected:
+    std::stack<const state*> todo; ///< A stack of states yet to explore.
+  };
+
+  /// \brief An implementation of spot::ta_reachable_iterator that browses
+  /// states breadth first.
+  /// \ingroup ta_generic
+  class ta_reachable_iterator_breadth_first : public ta_reachable_iterator
+  {
+  public:
+    ta_reachable_iterator_breadth_first(const ta* a);
+
+    virtual void
+    add_state(const state* s);
+    virtual const state*
+    next_state();
+
+  protected:
+    std::deque<const state*> todo; ///< A queue of states yet to explore.
+  };
+
+}
+
+#endif // SPOT_TAALGOS_REACHITER_HH

src/taalgos/sba2ta.cc

@@ -0,0 +1,353 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "ltlast/atomic_prop.hh"
+#include "ltlast/constant.hh"
+#include "tgba/formula2bdd.hh"
+#include "misc/bddop.hh"
+#include <cassert>
+#include "ltlvisit/tostring.hh"
+#include <iostream>
+#include "tgba/bddprint.hh"
+#include "tgbaalgos/gtec/nsheap.hh"
+#include <stack>
+#include "sba2ta.hh"
+
+
+using namespace std;
+
+namespace spot
+{
+
+  ta*
+  sba_to_ta(const tgba_sba_proxy* tgba_, bdd atomic_propositions_set_)
+  {
+
+    ta_explicit* ta = new spot::ta_explicit(tgba_);
+
+    // build I set:
+    bdd init_condition;
+    bdd all_props = bddtrue;
+    ta::states_set_t todo;
+
+    while ((init_condition = bdd_satoneset(all_props, atomic_propositions_set_,
+        bddtrue)) != bddfalse)
+      {
+        all_props -= init_condition;
+        state_ta_explicit* init_state = new state_ta_explicit((tgba_->get_init_state()),
+            init_condition, true);
+        ta->add_initial_state(init_state);
+        todo.insert(init_state);
+      }
+
+    while (!todo.empty())
+      {
+        ta::states_set_t::iterator todo_it = todo.begin();
+        state_ta_explicit* source = dynamic_cast<state_ta_explicit*> (*todo_it);
+        todo.erase(todo_it);
+
+        tgba_succ_iterator* tgba_succ_it = tgba_->succ_iter(
+            source->get_tgba_state());
+        for (tgba_succ_it->first(); !tgba_succ_it->done(); tgba_succ_it->next())
+          {
+            const state* tgba_state = tgba_succ_it->current_state();
+            bdd tgba_condition = tgba_succ_it->current_condition();
+            bdd satone_tgba_condition;
+            while ((satone_tgba_condition = bdd_satoneset(tgba_condition,
+                atomic_propositions_set_, bddtrue)) != bddfalse)
+              {
+
+                tgba_condition -= satone_tgba_condition;
+                state_ta_explicit* new_dest = new state_ta_explicit(tgba_state->clone(),
+                    satone_tgba_condition, false, tgba_->state_is_accepting(
+                        tgba_state));
+
+                state_ta_explicit* dest = ta->add_state(new_dest);
+
+                if (dest != new_dest)
+                  {
+                    // the state dest already exists in the testing automata
+                    delete new_dest->get_tgba_state();
+                    delete new_dest;
+                  }
+                else
+                  {
+                    todo.insert(dest);
+                  }
+
+                ta->create_transition(source, bdd_setxor(
+                    source->get_tgba_condition(), dest->get_tgba_condition()),
+                    dest);
+
+              }
+            delete tgba_state;
+          }
+        delete tgba_succ_it;
+
+      }
+
+    compute_livelock_acceptance_states(ta);
+
+    ta->delete_stuttering_transitions();
+
+    return ta;
+
+  }
+
+  namespace
+  {
+    typedef std::pair<spot::state*, tgba_succ_iterator*> pair_state_iter;
+  }
+
+  void
+  compute_livelock_acceptance_states(ta_explicit* testing_automata)
+  {
+    // We use five main data in this algorithm:
+    // * sscc: a stack of strongly stuttering-connected components (SSCC)
+    sscc_stack sscc;
+
+    // * h: a hash of all visited nodes, with their order,
+    //   (it is called "Hash" in Couvreur's paper)
+    numbered_state_heap* h =
+        numbered_state_heap_hash_map_factory::instance()->build(); ///< Heap of visited states.
+
+    // * num: the number of visited nodes.  Used to set the order of each
+    //   visited node,
+    int num = 0;
+
+    // * todo: the depth-first search stack.  This holds pairs of the
+    //   form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
+    //   over the successors of STATE.  In our use, ITERATOR should
+    //   always be freed when TODO is popped, but STATE should not because
+    //   it is also used as a key in H.
+    std::stack<pair_state_iter> todo;
+
+    // * init: the set of the depth-first search initial states
+    ta::states_set_t init_set;
+
+    ta::states_set_t::const_iterator it;
+    for (it = (testing_automata->get_initial_states_set())->begin(); it != (testing_automata->get_initial_states_set())->end(); it++)
+      {
+        state* init_state = (*it);
+        init_set.insert(init_state);
+
+      }
+
+    while (!init_set.empty())
+      {
+        // Setup depth-first search from an initial state.
+          {
+            ta::states_set_t::iterator init_set_it = init_set.begin();
+            state_ta_explicit* init = dynamic_cast<state_ta_explicit*> (*init_set_it);
+            init_set.erase(init_set_it);
+            state_ta_explicit* init_clone = init->clone();
+            numbered_state_heap::state_index_p h_init = h->find(init_clone);
+
+            if (h_init.first)
+              continue;
+
+            h->insert(init_clone, ++num);
+            sscc.push(num);
+            sscc.top().is_accepting = testing_automata->is_accepting_state(init);
+            sscc.top().is_initial = testing_automata->is_initial_state(init);
+            tgba_succ_iterator* iter = testing_automata->succ_iter(init);
+            iter->first();
+            todo.push(pair_state_iter(init, iter));
+
+          }
+
+        while (!todo.empty())
+          {
+
+            // We are looking at the next successor in SUCC.
+            tgba_succ_iterator* succ = todo.top().second;
+
+            state* curr = todo.top().first;
+
+            // If there is no more successor, backtrack.
+            if (succ->done())
+              {
+                // We have explored all successors of state CURR.
+
+                // Backtrack TODO.
+                todo.pop();
+
+                // fill rem with any component removed,
+                numbered_state_heap::state_index_p spi = h->index(curr->clone());
+                assert(spi.first);
+
+                sscc.rem().push_front(curr);
+
+                // When backtracking the root of an SSCC, we must also
+                // remove that SSCC from the ROOT stacks.  We must
+                // discard from H all reachable states from this SSCC.
+                assert(!sscc.empty());
+                if (sscc.top().index == *spi.second)
+                  {
+                    // removing states
+                    std::list<state*>::iterator i;
+                    bool is_livelock_accepting_sscc = (sscc.top().is_accepting
+                        && (sscc.rem().size() > 1));
+                    for (i = sscc.rem().begin(); i != sscc.rem().end(); ++i)
+                      {
+                        numbered_state_heap::state_index_p spi = h->index((*i)->clone());
+                        assert(spi.first->compare(*i)==0);
+                        assert(*spi.second != -1);
+                        *spi.second = -1;
+                        if (is_livelock_accepting_sscc)
+                          {//if it is an accepting sscc
+                            //add the state to G (=the livelock-accepting states set)
+
+                            state_ta_explicit * livelock_accepting_state =
+                                dynamic_cast<state_ta_explicit*> (*i);
+
+                            livelock_accepting_state->set_livelock_accepting_state(
+                                true);
+
+                          }
+
+                        if (sscc.top().is_initial)
+                          {//if it is an initial sscc
+                            //add the state to I (=the initial states set)
+
+                            state_ta_explicit * initial_state =
+                                dynamic_cast<state_ta_explicit*> (*i);
+
+                            testing_automata->add_initial_state(initial_state);
+                          }
+                      }
+
+                    is_livelock_accepting_sscc = testing_automata->is_livelock_accepting_state(
+                        *sscc.rem().begin());
+                    sscc.pop();
+                    if (is_livelock_accepting_sscc && !sscc.empty())
+                      {
+                        sscc.top().is_accepting = true;
+
+                        state_ta_explicit * livelock_accepting_state =
+                            dynamic_cast<state_ta_explicit*> (todo.top().first);
+                        livelock_accepting_state->set_livelock_accepting_state(
+                            true);
+
+                      }
+                    if (sscc.top().is_initial && !sscc.empty())
+                      sscc.top().is_initial = true;
+                  }
+
+                delete succ;
+                // Do not delete CURR: it is a key in H.
+                continue;
+              }
+
+            // Fetch the values destination state we are interested in...
+            state* dest = succ->current_state();
+
+            // ... and point the iterator to the next successor, for
+            // the next iteration.
+            succ->next();
+            // We do not need SUCC from now on.
+
+
+            // Are we going to a new state through a stuttering transition?
+            bool is_stuttering_transition = testing_automata->get_state_condition(curr)
+                == testing_automata->get_state_condition(dest);
+            state* dest_clone = dest->clone();
+            numbered_state_heap::state_index_p spi = h->find(dest_clone);
+
+            // Is this a new state?
+            if (!spi.first)
+              {
+                if (!is_stuttering_transition)
+                  {
+                    init_set.insert(dest);
+                    delete dest_clone;
+                    continue;
+                  }
+
+                // Number it, stack it, and register its successors
+                // for later processing.
+                h->insert(dest_clone, ++num);
+                sscc.push(num);
+                sscc.top().is_accepting = testing_automata->is_accepting_state(dest);
+                sscc.top().is_initial = testing_automata->is_initial_state(dest);
+                tgba_succ_iterator* iter = testing_automata->succ_iter(dest);
+                iter->first();
+                todo.push(pair_state_iter(dest, iter));
+                continue;
+              }
+
+            // If we have reached a dead component, ignore it.
+            if (*spi.second == -1)
+              continue;
+
+            if (!curr->compare(dest))
+              {
+                state_ta_explicit * self_loop_state = dynamic_cast<state_ta_explicit*> (curr);
+
+                if (testing_automata->is_accepting_state(self_loop_state))
+                  self_loop_state->set_livelock_accepting_state(true);
+
+              }
+
+            // Now this is the most interesting case.  We have reached a
+            // state S1 which is already part of a non-dead SSCC.  Any such
+            // non-dead SSCC has necessarily been crossed by our path to
+            // this state: there is a state S2 in our path which belongs
+            // to this SSCC too.  We are going to merge all states between
+            // this S1 and S2 into this SSCC.
+            //
+            // This merge is easy to do because the order of the SSCC in
+            // ROOT is ascending: we just have to merge all SSCCs from the
+            // top of ROOT that have an index greater to the one of
+            // the SSCC of S2 (called the "threshold").
+            int threshold = *spi.second;
+            std::list<state*> rem;
+            bool acc = false;
+            bool init = false;
+            while (threshold < sscc.top().index)
+              {
+                assert(!sscc.empty());
+
+                acc |= sscc.top().is_accepting;
+                init |= sscc.top().is_initial;
+
+                rem.splice(rem.end(), sscc.rem());
+                sscc.pop();
+
+              }
+            // Note that we do not always have
+            //  threshold == sscc.top().index
+            // after this loop, the SSCC whose index is threshold might have
+            // been merged with a lower SSCC.
+
+            // Accumulate all acceptance conditions into the merged SSCC.
+            sscc.top().is_accepting |= acc;
+            sscc.top().is_initial |= init;
+
+            sscc.rem().splice(sscc.rem().end(), rem);
+
+          }
+
+      }
+    delete h;
+
+  }
+
+}

src/taalgos/sba2ta.hh

@@ -0,0 +1,44 @@
+// Copyright (C) 2010 Laboratoire de Recherche et Developpement
+// de l Epita (LRDE).
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_TGBAALGOS_SBA2TA_HH
+# define SPOT_TGBAALGOS_SBA2TA_HH
+
+#include "misc/hash.hh"
+#include <list>
+#include <map>
+#include <set>
+#include "tgba/tgbatba.hh"
+#include "ltlast/formula.hh"
+#include <cassert>
+#include "misc/bddlt.hh"
+#include "ta/taexplicit.hh"
+
+
+namespace spot
+{
+  ta* sba_to_ta(const tgba_sba_proxy* tgba_to_convert, bdd atomic_propositions_set);
+
+
+  void compute_livelock_acceptance_states(ta_explicit* testing_automata);
+
+}
+
+#endif // SPOT_TGBAALGOS_SBA2TA_HH

src/tgbatest/ltl2tgba.cc

@@ -65,6 +65,9 @@
 #include "kripkeparse/public.hh"
 #include "tgbaalgos/simulation.hh"
 
+#include "taalgos/sba2ta.hh"
+#include "taalgos/dotty.hh"
+
 std::string
 ltl_defs()
 {
@@ -273,7 +276,13 @@ syntax(char* prog)
             << "  -T    time the different phases of the translation"
 	    << std::endl
 	    << "  -v    display the BDD variables used by the automaton"
-	    << std::endl;
+	    << std::endl
+
+  	  	<< "Options for Testing Automata:"
+ 	    << std::endl
+ 	    << "  -TA    Translate an LTL formula into a Testing automata"
+ 	    << std::endl;
+
   exit(2);
 }
 
@@ -332,7 +341,7 @@ main(int argc, char** argv)
   bool assume_sba = false;
   bool reduction_dir_sim = false;
   spot::tgba* temp_dir_sim = 0;
-
+  bool ta_opt = false;
 
   for (;;)
     {
@@ -660,6 +669,10 @@ main(int argc, char** argv)
 	{
 	  use_timer = true;
 	}
+      else if (!strcmp(argv[formula_index], "-TA"))
+        {
+          ta_opt = true;
+        }
       else if (!strcmp(argv[formula_index], "-taa"))
 	{
 	  translation = TransTAA;
@@ -1047,8 +1060,39 @@ main(int argc, char** argv)
 	  break;
 	}
 
+
       const spot::tgba* product_degeneralized = 0;
 
+      if (ta_opt)
+        {
+          spot::tgba_sba_proxy* degeneralized_new = 0;
+          spot::tgba_sba_proxy* degeneralized =
+              dynamic_cast<spot::tgba_sba_proxy*> (a);
+          if (degeneralized == 0)
+            degeneralized_new = degeneralized =  new spot::tgba_sba_proxy(a);
+
+          spot::ltl::atomic_prop_set* aps = atomic_prop_collect(f, 0);
+
+          bdd atomic_props_set_bdd = bdd_true();
+          for (spot::ltl::atomic_prop_set::const_iterator i = aps->begin(); i
+              != aps->end(); ++i)
+            {
+              bdd atomic_prop = bdd_ithvar(
+                  (degeneralized->get_dict())->var_map[*i]);
+
+              atomic_props_set_bdd &= atomic_prop;
+
+            }
+          delete aps;
+
+          spot::ta* testing_automata = sba_to_ta(degeneralized, atomic_props_set_bdd);
+          spot::dotty_reachable(std::cout, testing_automata);
+          delete testing_automata;
+          delete degeneralized_new;
+          output = -1;
+        }
+
+
       if (system)
         {
           product = product_to_free = a = new spot::tgba_product(system, a);