A wrapper around tgba to produce state-labeled automata.

* src/tgba/tgbasgba.hh, src/tgba/tgbasgba.hh: Here.
* src/tgbatest/ltl2tgba.cc: New option `-lS' for state-labeled
automata.
* src/tgba/Makefile.am: Adjust and sort files in tgba_HEADERS
and libtgba_la_SOURCES.

src/tgba/Makefile.am

@@ -40,13 +40,14 @@ tgba_HEADERS = \
   tgbabddconcreteproduct.hh \
   tgbabddcoredata.hh \
   tgbabddfactory.hh \
-  tgbascc.hh \
-  tgbasafracomplement.hh \
   tgbaexplicit.hh \
-  tgbaproduct.hh \
-  tgbatba.hh \
-  tgbareduc.hh \
   tgbafromfile.hh \
+  tgbascc.hh \
+  tgbaproduct.hh \
+  tgbareduc.hh \
+  tgbasgba.hh \
+  tgbasafracomplement.hh \
+  tgbatba.hh \
   tgbaunion.hh
 
 noinst_LTLIBRARIES = libtgba.la
@@ -55,18 +56,19 @@ libtgba_la_SOURCES = \
   bddprint.cc \
   formula2bdd.cc \
   futurecondcol.cc \
-  statebdd.cc \
   succiterconcrete.cc \
+  statebdd.cc \
   tgba.cc \
   tgbabddconcrete.cc \
   tgbabddconcretefactory.cc \
   tgbabddconcreteproduct.cc \
   tgbabddcoredata.cc \
-  tgbascc.cc \
-  tgbasafracomplement.cc \
+  tgbafromfile.cc \
   tgbaexplicit.cc \
   tgbaproduct.cc \
-  tgbatba.cc \
   tgbareduc.cc \
-  tgbafromfile.cc \
+  tgbasafracomplement.cc \
+  tgbascc.cc \
+  tgbasgba.cc \
+  tgbatba.cc \
   tgbaunion.cc

src/tgba/tgbasgba.cc

@@ -0,0 +1,249 @@
+// Copyright (C) 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// 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 "tgbasgba.hh"
+#include "bddprint.hh"
+#include "ltlast/constant.hh"
+#include "misc/hashfunc.hh"
+
+namespace spot
+{
+  namespace
+  {
+    /// \brief A state for spot::tgba_sgba_proxy.
+    class state_sgba_proxy: public state
+    {
+    public:
+      state_sgba_proxy(state* s, bdd acc)
+	:	s_(s), acc_(acc)
+      {
+      }
+
+      /// Copy constructor
+      state_sgba_proxy(const state_sgba_proxy& o)
+	: state(),
+	  s_(o.real_state()->clone()),
+	  acc_(o.acc_)
+      {
+      }
+
+      virtual
+      ~state_sgba_proxy()
+      {
+	delete s_;
+      }
+
+      state*
+      real_state() const
+      {
+	return s_;
+      }
+
+      bdd
+      acceptance_cond() const
+      {
+	return acc_;
+      }
+
+      virtual int
+      compare(const state* other) const
+      {
+	const state_sgba_proxy* o =
+          dynamic_cast<const state_sgba_proxy*>(other);
+	assert(o);
+	int res = s_->compare(o->real_state());
+	if (res != 0)
+	  return res;
+	return acc_.id() - o->acc_.id();
+      }
+
+      virtual size_t
+      hash() const
+      {
+	return wang32_hash(s_->hash()) ^ wang32_hash(acc_.id());
+      }
+
+      virtual
+      state_sgba_proxy* clone() const
+      {
+	return new state_sgba_proxy(*this);
+      }
+
+    private:
+      state* s_;
+      bdd acc_;
+    };
+
+
+    /// \brief Iterate over the successors of tgba_sgba_proxy computed
+    /// on the fly.
+    class tgba_sgba_proxy_succ_iterator: public tgba_succ_iterator
+    {
+    public:
+      tgba_sgba_proxy_succ_iterator(tgba_succ_iterator* it)
+	: it_(it)
+      {
+      }
+
+      virtual
+      ~tgba_sgba_proxy_succ_iterator()
+      {
+	delete it_;
+      }
+
+      // iteration
+
+      void
+      first()
+      {
+	it_->first();
+      }
+
+      void
+      next()
+      {
+	it_->next();
+      }
+
+      bool
+      done() const
+      {
+	return it_->done();
+      }
+
+      // inspection
+
+      state_sgba_proxy*
+      current_state() const
+      {
+	return new state_sgba_proxy(it_->current_state(),
+                                   it_->current_acceptance_conditions());
+      }
+
+      bdd
+      current_condition() const
+      {
+	return it_->current_condition();
+      }
+
+      bdd
+      current_acceptance_conditions() const
+      {
+	return it_->current_acceptance_conditions();
+      }
+
+    protected:
+      tgba_succ_iterator* it_;
+      friend class ::spot::tgba_sgba_proxy;
+    };
+
+  } // anonymous
+
+  tgba_sgba_proxy::tgba_sgba_proxy(const tgba* a)
+    : a_(a)
+  {
+    get_dict()->register_all_variables_of(a, this);
+  }
+
+  tgba_sgba_proxy::~tgba_sgba_proxy()
+  {
+    get_dict()->unregister_all_my_variables(this);
+  }
+
+  state*
+  tgba_sgba_proxy::get_init_state() const
+  {
+    return new state_sgba_proxy(a_->get_init_state(), bddfalse);
+  }
+
+  tgba_succ_iterator*
+  tgba_sgba_proxy::succ_iter(const state* local_state,
+			    const state* global_state,
+			    const tgba* global_automaton) const
+  {
+    const state_sgba_proxy* s =
+      dynamic_cast<const state_sgba_proxy*>(local_state);
+    assert(s);
+
+    tgba_succ_iterator* it = a_->succ_iter(s->real_state(),
+					   global_state, global_automaton);
+
+    return new tgba_sgba_proxy_succ_iterator(it);
+  }
+
+  bdd_dict*
+  tgba_sgba_proxy::get_dict() const
+  {
+    return a_->get_dict();
+  }
+
+  std::string
+  tgba_sgba_proxy::format_state(const state* state) const
+  {
+    const state_sgba_proxy* s = dynamic_cast<const state_sgba_proxy*>(state);
+    assert(s);
+    std::string a = bdd_format_accset(get_dict(), s->acceptance_cond());
+    if (a != "")
+      a = " " + a;
+    return a_->format_state(s->real_state()) + a;
+  }
+
+  bdd
+  tgba_sgba_proxy::all_acceptance_conditions() const
+  {
+    return a_->all_acceptance_conditions();
+  }
+
+  bdd
+  tgba_sgba_proxy::neg_acceptance_conditions() const
+  {
+    return a_->neg_acceptance_conditions();
+  }
+
+  bdd
+  tgba_sgba_proxy::state_acceptance_conditions(const state* state) const
+  {
+    const state_sgba_proxy* s =
+      dynamic_cast<const state_sgba_proxy*>(state);
+    assert(s);
+    return s->acceptance_cond();
+  }
+
+  bdd
+  tgba_sgba_proxy::compute_support_conditions(const state* state) const
+  {
+    const state_sgba_proxy* s =
+      dynamic_cast<const state_sgba_proxy*>(state);
+    assert(s);
+    return a_->support_conditions(s->real_state());
+  }
+
+  bdd
+  tgba_sgba_proxy::compute_support_variables(const state* state) const
+  {
+    const state_sgba_proxy* s =
+      dynamic_cast<const state_sgba_proxy*>(state);
+    assert(s);
+    return a_->support_variables(s->real_state());
+  }
+
+}

src/tgba/tgbasgba.hh

@@ -0,0 +1,73 @@
+// Copyright (C) 2009 Laboratoire d'Informatique de Paris
+// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
+// Université Pierre et Marie Curie.
+//
+// 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_TGBA_TGBASGBA_HH
+# define SPOT_TGBA_TGBASGBA_HH
+
+#include "tgba.hh"
+#include "misc/bddlt.hh"
+
+namespace spot
+{
+
+  /// \brief Change the labeling-mode of spot::tgba on the fly, producing a
+  /// state-based generalized Büchi automaton.
+  /// \ingroup tgba_on_the_fly_algorithms
+  ///
+  /// This class acts as a proxy in front of a spot::tgba, that should
+  /// label on states on-the-fly.  The result is still a spot::tgba,
+  /// but acceptances conditions are also on states.
+  class tgba_sgba_proxy : public tgba
+  {
+  public:
+    tgba_sgba_proxy(const tgba* a);
+
+    virtual ~tgba_sgba_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_acceptance_conditions() const;
+    virtual bdd neg_acceptance_conditions() const;
+
+    /// \brief Retrieve the acceptance condition of a state.
+    bdd state_acceptance_conditions(const state* state) const;
+  protected:
+    virtual bdd compute_support_conditions(const state* state) const;
+    virtual bdd compute_support_variables(const state* state) const;
+
+  private:
+    const tgba* a_;
+    // Disallow copy.
+    tgba_sgba_proxy(const tgba_sgba_proxy&);
+    tgba_sgba_proxy& operator=(const tgba_sgba_proxy&);
+  };
+
+}
+#endif // SPOT_TGBA_TGBASGBA_HH

src/tgbatest/ltl2tgba.cc

@@ -38,6 +38,7 @@
 #include "tgbaalgos/dotty.hh"
 #include "tgbaalgos/lbtt.hh"
 #include "tgba/tgbatba.hh"
+#include "tgba/tgbasgba.hh"
 #include "tgba/tgbaproduct.hh"
 #include "tgba/futurecondcol.hh"
 #include "tgbaalgos/reducerun.hh"
@@ -100,6 +101,7 @@ syntax(char* prog)
 	    << "  -KV   verbosely dump the graph of SCCs in dot format"
 	    << std::endl
             << "  -L    fair-loop approximation (implies -f)" << std::endl
+            << "  -lS   label acceptance conditions on states" << std::endl
 	    << "  -m    try to reduce accepting runs, in a second pass"
 	    << std::endl
 	    << "  -N    display the never clain for Spin "
@@ -169,6 +171,7 @@ main(int argc, char** argv)
   bool debug_opt = false;
   bool paper_opt = false;
   enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
+  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
   bool fm_opt = false;
   int fm_red = spot::ltl::Reduce_None;
   bool fm_exprop_opt = false;
@@ -350,6 +353,10 @@ main(int argc, char** argv)
 	  fair_loop_approx = true;
 	  fm_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-lS"))
+	{
+	  labeling_opt = StateLabeled;
+	}
       else if (!strcmp(argv[formula_index], "-m"))
 	{
 	  opt_reduce = true;
@@ -581,6 +588,7 @@ main(int argc, char** argv)
 	}
 
       spot::tgba_tba_proxy* degeneralized = 0;
+      spot::tgba_sgba_proxy* state_labeled = 0;
 
       unsigned int n_acc = a->number_of_acceptance_conditions();
       if (echeck_inst
@@ -592,6 +600,10 @@ main(int argc, char** argv)
 	a = degeneralized = new spot::tgba_tba_proxy(a);
       else if (degeneralize_opt == DegenSBA)
 	a = degeneralized = new spot::tgba_sba_proxy(a);
+      else if (labeling_opt == StateLabeled)
+      {
+        a = state_labeled = new spot::tgba_sgba_proxy(a);
+      }
 
       spot::tgba_reduc* aut_red = 0;
       if (reduc_aut != spot::Reduce_None)
@@ -887,6 +899,7 @@ main(int argc, char** argv)
       delete expl;
       delete aut_red;
       delete degeneralized;
+      delete state_labeled;
       delete to_free;
       delete echeck_inst;
     }