Implement spot::future_conditions_collector.

* src/tgba/futurecondcol.hh, src/tgba/futurecondcol.cc:
New files.
* src/tgba/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: Add option -FC.

ChangeLog

@@ -1,3 +1,12 @@
+2009-05-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	Implement spot::future_conditions_collector.
+
+	* src/tgba/futurecondcol.hh, src/tgba/futurecondcol.cc:
+	New files.
+	* src/tgba/Makefile.am: Adjust.
+	* src/tgbatest/ltl2tgba.cc: Add option -FC.
+
 2009-05-28  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	* src/tgbaalgos/scc.cc (dump_scc_dot): Use a bit vector instead of

src/tgba/Makefile.am

@@ -1,4 +1,4 @@
-## Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
+## Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
 ## département Systèmes Répartis Coopératifs (SRC), Université Pierre
 ## et Marie Curie.
 ##
@@ -28,6 +28,7 @@ tgba_HEADERS = \
   bdddict.hh \
   bddprint.hh \
   formula2bdd.hh \
+  futurecondcol.hh \
   public.hh \
   state.hh \
   statebdd.hh \
@@ -49,6 +50,7 @@ libtgba_la_SOURCES = \
   bdddict.cc \
   bddprint.cc \
   formula2bdd.cc \
+  futurecondcol.cc \
   statebdd.cc \
   succiterconcrete.cc \
   tgba.cc \

src/tgba/futurecondcol.cc

@@ -0,0 +1,150 @@
+// Copyright (C) 2009  Laboratoire de recherche et développement de l'Epita.
+//
+// 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 <sstream>
+#include "futurecondcol.hh"
+#include "bddprint.hh"
+
+namespace spot
+{
+
+  void
+  future_conditions_collector::map_builder_(unsigned src)
+  {
+    // The future conditions of a SCC are the conditions of the SCC
+    // augmented with the future conditions of any descendent SCC.
+    cond_set res(scc_map_.cond_set_of(src));
+    const scc_map::succ_type& next = scc_map_.succ(src);
+    for (scc_map::succ_type::const_iterator i = next.begin();
+	 i != next.end(); ++i)
+      {
+	unsigned dest = i->first;
+	map_builder_(dest);
+	res.insert(i->second);
+	res.insert(future_conds_[dest].begin(), future_conds_[dest].end());
+      }
+    future_conds_[src] = res;
+  }
+
+  future_conditions_collector::future_conditions_collector(const tgba* aut,
+							   bool show)
+    : aut_(aut), scc_map_(aut), show_(show)
+  {
+    scc_map_.build_map();
+    // Initialize future_conds_ with as much empty "cond_set"s as
+    // there are SCCs.
+    future_conds_ = fc_map(scc_map_.scc_count());
+    // Fill future_conds by recursively visiting the (acyclic) graph
+    // of SCCs.
+    map_builder_(scc_map_.initial());
+  }
+
+  future_conditions_collector::~future_conditions_collector()
+  {
+  }
+
+  const future_conditions_collector::cond_set&
+  future_conditions_collector::future_conditions(const spot::state* st) const
+  {
+    // The future conditions of a state are the future conditions of
+    // the SCC the state belongs to.
+    unsigned s = scc_map_.scc_of_state(st);
+    return future_conds_[s];
+  }
+
+  state*
+  future_conditions_collector::get_init_state() const
+  {
+    return aut_->get_init_state();
+  }
+
+  tgba_succ_iterator*
+  future_conditions_collector::succ_iter(const state* local_state,
+					 const state* global_state,
+					 const tgba* global_automaton) const
+  {
+    return aut_->succ_iter(local_state, global_state, global_automaton);
+  }
+
+  bdd_dict*
+  future_conditions_collector::get_dict() const
+  {
+    return aut_->get_dict();
+  }
+
+  std::string
+  future_conditions_collector::format_state(const state* state) const
+  {
+    if (!show_)
+      return aut_->format_state(state);
+
+    std::ostringstream str;
+    str << aut_->format_state(state);
+    str << "\\n[";
+    const cond_set& c = future_conditions(state);
+    for (cond_set::const_iterator i = c.begin(); i != c.end(); ++i)
+      {
+	if (i != c.begin())
+	  str << ", ";
+	bdd_print_formula(str, get_dict(), *i);
+      }
+    str << "]";
+    return str.str();
+  }
+
+  std::string
+  future_conditions_collector::transition_annotation
+    (const tgba_succ_iterator* t) const
+  {
+    return aut_->transition_annotation(t);
+  }
+
+  state*
+  future_conditions_collector::project_state(const state* s,
+					     const tgba* t) const
+  {
+    return aut_->project_state(s, t);
+  }
+
+  bdd
+  future_conditions_collector::all_acceptance_conditions() const
+  {
+    return aut_->all_acceptance_conditions();
+  }
+
+  bdd
+  future_conditions_collector::neg_acceptance_conditions() const
+  {
+    return aut_->neg_acceptance_conditions();
+  }
+
+  bdd
+  future_conditions_collector::compute_support_conditions
+    (const state* state) const
+  {
+    return aut_->support_conditions(state);
+  }
+
+  bdd
+  future_conditions_collector::compute_support_variables
+    (const state* state) const
+  {
+    return aut_->support_variables(state);
+  }
+}

src/tgba/futurecondcol.hh

@@ -0,0 +1,93 @@
+// Copyright (C) 2009  Laboratoire de recherche et développement de l'Epita.
+//
+// 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_FUTURECONDCOL_HH
+# define SPOT_TGBA_FUTURECONDCOL_HH
+
+#include "tgbaexplicit.hh"
+#include "tgbaalgos/scc.hh"
+
+namespace spot
+{
+
+  /// \brief Wrap a tgba to offer information about upcoming conditions.
+  /// \ingroup tgba
+  ///
+  /// This class is a spot::tgba wrapper that simply add a new method,
+  /// future_conditions(), to any spot::tgba.
+  ///
+  /// This new methods returns a set of conditions that can be
+  /// seen on a transitions accessible (maybe indirectly) from
+  /// the given state.
+  class future_conditions_collector : public tgba
+  {
+  public:
+    typedef scc_map::cond_set cond_set;
+    typedef std::vector<cond_set> fc_map;
+
+    /// \brief Create a future_conditions_collector wrapper for \a aut.
+    ///
+    /// If \a show is set to true, then the format_state() method will
+    /// include the set of conditions computed for the given state in
+    /// its output string.
+    future_conditions_collector(const tgba* aut, bool show = false);
+    virtual ~future_conditions_collector();
+
+    const cond_set& future_conditions(const spot::state* s) const;
+
+    /// \brief Format a state for output.
+    ///
+    /// If the constructor was called with \a show set to true, then
+    /// this method will include the set of conditions computed for \a
+    /// state by future_conditions() in the output string.
+    virtual std::string format_state(const state* state) const;
+
+    // The following methods simply delegate their work to the wrapped
+    // tgba.
+
+    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
+    transition_annotation(const tgba_succ_iterator* t) const;
+    virtual state* project_state(const state* s, const tgba* t) const;
+    virtual bdd all_acceptance_conditions() const;
+    virtual bdd neg_acceptance_conditions() const;
+
+    virtual bdd compute_support_conditions(const state* state) const;
+    virtual bdd compute_support_variables(const state* state) const;
+
+  private:
+    void map_builder_(unsigned s);
+
+    const tgba* aut_;		// The wrapped TGBA.
+    fc_map future_conds_;	// The map of future conditions for each
+				// strongly connected component.
+    scc_map scc_map_;		// SCC informations.
+    bool show_;		        // Wether to show future conditions
+				// in the output of format_state().
+  };
+
+}
+
+#endif // SPOT_TGBA_FUTURECONDCOL_HH

src/tgbatest/ltl2tgba.cc

@@ -39,6 +39,7 @@
 #include "tgbaalgos/lbtt.hh"
 #include "tgba/tgbatba.hh"
 #include "tgba/tgbaproduct.hh"
+#include "tgba/futurecondcol.hh"
 #include "tgbaalgos/reducerun.hh"
 #include "tgbaparse/public.hh"
 #include "tgbaalgos/dupexp.hh"
@@ -87,6 +88,8 @@ syntax(char* prog)
 	    << "  -fr7  use -r7 (see below) at each step of FM" << std::endl
 	    << "  -fr8  use -r8 (see below) at each step of FM" << std::endl
             << "  -F    read the formula from the file" << std::endl
+            << "  -FC   dump the automaton showing future conditions on states"
+	    << std::endl
 	    << "  -g    graph the accepting run on the automaton (requires -e)"
 	    << std::endl
 	    << "  -G    graph the accepting run seen as an automaton "
@@ -189,6 +192,7 @@ main(int argc, char** argv)
   bool graph_run_tgba_opt = false;
   bool opt_reduce = false;
   bool containment = false;
+  bool show_fc = false;
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* unobservables = 0;
   spot::tgba_explicit* system = 0;
@@ -317,6 +321,10 @@ main(int argc, char** argv)
 	{
 	  file_opt = true;
 	}
+      else if (!strcmp(argv[formula_index], "-FC"))
+	{
+	  show_fc = true;
+	}
       else if (!strcmp(argv[formula_index], "-g"))
 	{
 	  graph_run_opt = true;
@@ -695,6 +703,11 @@ main(int argc, char** argv)
 	    }
 	}
 
+      if (show_fc)
+	{
+	  a = new spot::future_conditions_collector(a, true);
+	}
+
       switch (output)
 	{
 	case -1:
@@ -864,6 +877,8 @@ main(int argc, char** argv)
 	  delete ec;
 	}
 
+      if (show_fc)
+	delete a;
       if (f)
         spot::ltl::destroy(f);
       delete product_degeneralized;