Introduce some masked tgba.

* src/tgba/tgbamask.cc, src/tgba/tgbamask.hh,
src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh: New files.
* src/tgba/Makefile.am: Add them.
* src/tgbatest/explicit3.cc, src/tgbatest/explicit3.test:
New files.
* src/tgbatest/Makefile.am: Add them.

src/tgba/Makefile.am

@@ -45,6 +45,8 @@ tgba_HEADERS = \
   tgbabddfactory.hh \
   tgbaexplicit.hh \
   tgbakvcomplement.hh \
+  tgbamask.hh \
+  tgbaproxy.hh \
   tgbascc.hh \
   tgbaproduct.hh \
   tgbasgba.hh \
@@ -70,6 +72,8 @@ libtgba_la_SOURCES = \
   tgbaexplicit.cc \
   tgbakvcomplement.cc \
   tgbaproduct.cc \
+  tgbamask.cc \
+  tgbaproxy.cc \
   tgbasafracomplement.cc \
   tgbascc.cc \
   tgbasgba.cc \

src/tgba/tgbamask.cc

@@ -0,0 +1,183 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "tgbamask.hh"
+#include <vector>
+
+namespace spot
+{
+  namespace
+  {
+    struct transition
+    {
+      const state* dest;
+      bdd cond;
+      bdd acc;
+    };
+    typedef std::vector<transition> transitions;
+
+    struct succ_iter_filtered: public tgba_succ_iterator
+    {
+      ~succ_iter_filtered()
+      {
+	for (first(); !done(); next())
+	  it_->dest->destroy();
+      }
+
+      void first()
+      {
+	it_ = trans_.begin();
+      }
+
+      virtual void next()
+      {
+	++it_;
+      }
+
+      bool done() const
+      {
+	return it_ == trans_.end();
+      }
+
+      state* current_state() const
+      {
+	return it_->dest->clone();
+      }
+
+      bdd current_condition() const
+      {
+	return it_->cond;
+      }
+
+      bdd current_acceptance_conditions() const
+      {
+	return it_->acc;
+      }
+
+      transitions trans_;
+      transitions::const_iterator it_;
+    };
+
+
+    class tgba_mask_keep: public tgba_mask
+    {
+      const state_set& mask_;
+    public:
+      tgba_mask_keep(const tgba* masked,
+		     const state_set& mask,
+		     const state* init)
+	: tgba_mask(masked, init),
+	  mask_(mask)
+      {
+      }
+
+      bool wanted(const state* s) const
+      {
+	state_set::const_iterator i = mask_.find(s);
+	return i != mask_.end();
+      }
+    };
+
+    class tgba_mask_ignore: public tgba_mask
+    {
+      const state_set& mask_;
+    public:
+      tgba_mask_ignore(const tgba* masked,
+		       const state_set& mask,
+		       const state* init)
+	: tgba_mask(masked, init),
+	  mask_(mask)
+      {
+      }
+
+      bool wanted(const state* s) const
+      {
+	state_set::const_iterator i = mask_.find(s);
+	return i == mask_.end();
+      }
+    };
+
+
+  }
+
+
+  tgba_mask::tgba_mask(const tgba* masked,
+		       const state* init)
+    : tgba_proxy(masked),
+      init_(init)
+  {
+    if (!init)
+      init_ = masked->get_init_state();
+  }
+
+  tgba_mask::~tgba_mask()
+  {
+    init_->destroy();
+  }
+
+  state* tgba_mask::get_init_state() const
+  {
+    return init_->clone();
+  }
+
+  tgba_succ_iterator*
+  tgba_mask::succ_iter(const state* local_state,
+		       const state* global_state,
+		       const tgba* global_automaton) const
+  {
+    tgba_succ_iterator* it = original_->succ_iter(local_state,
+						  global_state,
+						  global_automaton);
+
+    succ_iter_filtered* res = new succ_iter_filtered;
+    for (it->first(); !it->done(); it->next())
+      {
+	const state* s = it->current_state();
+	if (!wanted(s))
+	  {
+	    s->destroy();
+	    continue;
+	  }
+	transition t = { s,
+			 it->current_condition(),
+			 it->current_acceptance_conditions() };
+	res->trans_.push_back(t);
+      }
+    delete it;
+    return res;
+  }
+
+
+  const tgba*
+  build_tgba_mask_keep(const tgba* to_mask,
+		       const state_set& to_keep,
+		       const state* init)
+  {
+    return new tgba_mask_keep(to_mask, to_keep, init);
+  }
+
+  const tgba*
+  build_tgba_mask_ignore(const tgba* to_mask,
+			 const state_set& to_ignore,
+			 const state* init)
+  {
+    return new tgba_mask_ignore(to_mask, to_ignore, init);
+  }
+
+}

src/tgba/tgbamask.hh

@@ -0,0 +1,85 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2013 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#ifndef SPOT_TGBA_TGBAMASK_HH
+# define SPOT_TGBA_TGBAMASK_HH
+
+#include "tgbaproxy.hh"
+
+namespace spot
+{
+
+  /// \ingroup tgba_on_the_fly_algorithms
+  /// \brief A masked TGBA (abstract).
+  ///
+  /// Ignores some states from a TGBA.  What state are preserved or
+  /// ignored is controlled by the wanted() method.
+  ///
+  /// This is an abstract class. You should inherit from it and
+  /// supply a wanted() method to specify which states to keep.
+  class SPOT_API tgba_mask: public tgba_proxy
+  {
+  protected:
+    /// \brief Constructor.
+    /// \param masked The automaton to mask
+    /// \param init Any state to use as initial state. This state will be
+    /// destroyed by the destructor.
+    tgba_mask(const tgba* masked, const state* init = 0);
+
+  public:
+    virtual ~tgba_mask();
+
+    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 bool wanted(const state* s) const = 0;
+
+  protected:
+    const state* init_;
+  };
+
+  /// \ingroup tgba_on_the_fly_algorithms
+  /// \brief Mask a TGBA, keeping a given set of states.
+  ///
+  /// Mask the TGBA \a to_mask, keeping only the
+  /// states from \a to_keep.  The initial state
+  /// can optionally be reset to \a init.
+  SPOT_API const tgba*
+  build_tgba_mask_keep(const tgba* to_mask,
+		       const state_set& to_keep,
+		       const state* init = 0);
+
+  /// \ingroup tgba_on_the_fly_algorithms
+  /// \brief Mask a TGBA, rejecting a given set of states.
+  ///
+  /// Mask the TGBA \a to_mask, keeping only the states that are not
+  /// in \a to_ignore.  The initial state can optionally be reset to
+  /// \a init.
+  SPOT_API const tgba*
+  build_tgba_mask_ignore(const tgba* to_mask,
+			 const state_set& to_ignore,
+			 const state* init = 0);
+
+}
+
+#endif // SPOT_TGBA_TGBAMASK_HH

src/tgba/tgbaproxy.cc

@@ -0,0 +1,95 @@
+// Copyright (C) 2013 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "tgbaproxy.hh"
+
+namespace spot
+{
+  tgba_proxy::tgba_proxy(const tgba* original)
+    : original_(original)
+  {
+    get_dict()->register_all_variables_of(original, this);
+  }
+
+  tgba_proxy::~tgba_proxy()
+  {
+    get_dict()->unregister_all_my_variables(this);
+  }
+
+  state* tgba_proxy::get_init_state() const
+  {
+    return original_->get_init_state();
+  }
+
+  tgba_succ_iterator*
+  tgba_proxy::succ_iter(const state* local_state,
+			const state* global_state,
+			const tgba* global_automaton) const
+  {
+    return original_->succ_iter(local_state, global_state, global_automaton);
+  }
+
+  bdd_dict*
+  tgba_proxy::get_dict() const
+  {
+    return original_->get_dict();
+  }
+
+  std::string
+  tgba_proxy::format_state(const state* state) const
+  {
+    return original_->format_state(state);
+  }
+
+  std::string
+  tgba_proxy::transition_annotation(const tgba_succ_iterator* t) const
+  {
+    return original_->transition_annotation(t);
+  }
+
+  state*
+  tgba_proxy::project_state(const state* s, const tgba* t) const
+  {
+    return original_->project_state(s, t);
+  }
+
+  bdd
+  tgba_proxy::all_acceptance_conditions() const
+  {
+    return original_->all_acceptance_conditions();
+  }
+
+  bdd
+  tgba_proxy::neg_acceptance_conditions() const
+  {
+    return original_->neg_acceptance_conditions();
+  }
+
+  bdd
+  tgba_proxy::compute_support_conditions(const state* state) const
+  {
+    return original_->support_conditions(state);
+  }
+
+  bdd
+  tgba_proxy::compute_support_variables(const state* state) const
+  {
+    return original_->support_variables(state);
+  }
+}
+

src/tgba/tgbaproxy.hh

@@ -0,0 +1,71 @@
+// Copyright (C) 2013 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#ifndef SPOT_TGBA_TGBAPROXY_HH
+# define SPOT_TGBA_TGBAPROXY_HH
+
+#include "tgba.hh"
+
+namespace spot
+{
+  /// \ingroup tgba_on_the_fly_algorithms
+  /// \brief A TGBA proxy.
+  ///
+  /// This implements a simple proxy to an existing
+  /// TGBA, forwarding all methods to the original.
+  /// By itself this class is pointless: better use the
+  /// original automaton right away.  However it is useful
+  /// to inherit from this class and override some of its
+  /// methods to implement some on-the-fly algorithm.
+  class SPOT_API tgba_proxy: public tgba
+  {
+  protected:
+    tgba_proxy(const tgba* original);
+
+  public:
+    virtual ~tgba_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 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;
+
+  protected:
+    virtual bdd compute_support_conditions(const state* state) const;
+    virtual bdd compute_support_variables(const state* state) const;
+
+    const tgba* original_;
+  };
+}
+
+#endif // SPOT_TGBA_TGBA_HH

src/tgbatest/.gitignore

@@ -8,6 +8,7 @@ eltl2tgba
 expldot
 explicit
 explicit2
+explicit3
 explprod
 input
 intvcomp

src/tgbatest/Makefile.am

@@ -35,6 +35,7 @@ check_PROGRAMS = \
   complement \
   explicit \
   explicit2 \
+  explicit3 \
   expldot \
   explprod \
   intvcomp \
@@ -53,6 +54,7 @@ bitvect_SOURCES  = bitvect.cc
 complement_SOURCES = complementation.cc
 explicit_SOURCES = explicit.cc
 explicit2_SOURCES = explicit2.cc
+explicit3_SOURCES = explicit3.cc
 expldot_SOURCES  = powerset.cc
 expldot_CXXFLAGS = -DDOTTY
 explprod_SOURCES = explprod.cc

src/tgbatest/explicit3.cc

@@ -0,0 +1,98 @@
+// Copyright (C) 2013 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include <iostream>
+#include <cassert>
+#include "ltlenv/defaultenv.hh"
+#include "tgba/tgbaexplicit.hh"
+#include "tgbaalgos/dotty.hh"
+#include "ltlast/allnodes.hh"
+#include "tgba/tgbamask.hh"
+
+int
+main()
+{
+  spot::ltl::default_environment& e =
+    spot::ltl::default_environment::instance();
+
+  const spot::ltl::formula* a = e.require("a");
+  const spot::ltl::formula* b = e.require("b");
+  const spot::ltl::formula* c = e.require("c");
+
+  spot::bdd_dict* dict = new spot::bdd_dict();
+  spot::tgba_explicit_number* aut = new spot::tgba_explicit_number(dict);
+
+  typedef spot::state_explicit_number::transition trans;
+
+  {
+    trans* t = aut->create_transition(0, 1);
+    aut->add_condition(t, a->clone());
+  }
+  {
+    trans* t = aut->create_transition(1, 2);
+    aut->add_condition(t, a->clone());
+  }
+  {
+    trans* t = aut->create_transition(2, 0);
+    aut->add_condition(t, a->clone());
+  }
+  {
+    trans* t = aut->create_transition(1, 3);
+    aut->add_condition(t, b->clone());
+  }
+  {
+    trans* t = aut->create_transition(3, 4);
+    aut->add_condition(t, c->clone());
+  }
+  {
+    trans* t = aut->create_transition(4, 3);
+    aut->add_condition(t, c->clone());
+    aut->declare_acceptance_condition(b->clone());
+    aut->add_acceptance_condition(t, b->clone());
+  }
+
+  a->destroy();
+  b->destroy();
+  c->destroy();
+
+  spot::dotty_reachable(std::cout, aut);
+
+  spot::state_set s;
+  s.insert(aut->get_state(0));
+  s.insert(aut->get_state(1));
+  s.insert(aut->get_state(2));
+
+  const spot::tgba* mk = build_tgba_mask_keep(aut, s);
+  spot::dotty_reachable(std::cout, mk);
+  delete mk;
+
+  const spot::tgba* mi = build_tgba_mask_ignore(aut, s);
+  spot::dotty_reachable(std::cout, mi);
+  delete mi;
+
+  const spot::tgba* mi2 = build_tgba_mask_ignore(aut, s, aut->get_state(1));
+  spot::dotty_reachable(std::cout, mi2);
+  delete mi2;
+
+  delete aut;
+  delete dict;
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+}

src/tgbatest/explicit3.test

@@ -0,0 +1,68 @@
+#!/bin/sh
+# Copyright (C) 2013 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 3 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 this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+set -e
+
+run 0 ../explicit3 | tee stdout
+cat >expected <<EOF
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="0"]
+  1 -> 2 [label="a\n"]
+  2 [label="1"]
+  2 -> 3 [label="a\n"]
+  2 -> 4 [label="b\n"]
+  3 [label="2"]
+  3 -> 1 [label="a\n"]
+  4 [label="3"]
+  4 -> 5 [label="c\n"]
+  5 [label="4"]
+  5 -> 4 [label="c\n{Acc[b]}"]
+}
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="0"]
+  1 -> 2 [label="a\n"]
+  2 [label="1"]
+  2 -> 3 [label="a\n"]
+  3 [label="2"]
+  3 -> 1 [label="a\n"]
+}
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="0"]
+}
+digraph G {
+  0 [label="", style=invis, height=0]
+  0 -> 1
+  1 [label="1"]
+  1 -> 2 [label="b\n"]
+  2 [label="3"]
+  2 -> 3 [label="c\n"]
+  3 [label="4"]
+  3 -> 2 [label="c\n{Acc[b]}"]
+}
+EOF
+
+cmp expected stdout