tgbamask.cc 5.17 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
// 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;
31
      acc_cond::mark_t acc;
32 33 34
    };
    typedef std::vector<transition> transitions;

35
    struct succ_iter_filtered: public twa_succ_iterator
36 37 38
    {
      ~succ_iter_filtered()
      {
39 40
	for (auto& t: trans_)
	  t.dest->destroy();
41 42
      }

43
      bool first()
44 45
      {
	it_ = trans_.begin();
46
	return it_ != trans_.end();
47 48
      }

49
      bool next()
50 51
      {
	++it_;
52
	return it_ != trans_.end();
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
      }

      bool done() const
      {
	return it_ == trans_.end();
      }

      state* current_state() const
      {
	return it_->dest->clone();
      }

      bdd current_condition() const
      {
	return it_->cond;
      }

70
      acc_cond::mark_t current_acceptance_conditions() const
71 72 73 74 75 76 77 78
      {
	return it_->acc;
      }

      transitions trans_;
      transitions::const_iterator it_;
    };

79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
    /// \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 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.
94
      tgba_mask(const const_twa_ptr& masked, const state* init = 0):
95 96 97 98 99 100
	tgba_proxy(masked),
	init_(init)
      {
	if (!init)
	  init_ = masked->get_init_state();
      }
101 102


103 104
    public:
      virtual ~tgba_mask()
105
      {
106
	init_->destroy();
107
      }
108 109

      virtual state* get_init_state() const
110
      {
111
	return init_->clone();
112
      }
113

114
      virtual twa_succ_iterator*
115
      succ_iter(const state* local_state) const
116
      {
117 118 119 120 121 122 123 124 125 126 127 128
	succ_iter_filtered* res;
	if (iter_cache_)
	  {
	    res = down_cast<succ_iter_filtered*>(iter_cache_);
	    res->trans_.clear();
	    iter_cache_ = nullptr;
	  }
	else
	  {
	    res = new succ_iter_filtered;
	  }
	for (auto it: original_->succ(local_state))
129
	  {
130
	    const spot::state* s = it->current_state();
131
	    auto acc = it->current_acceptance_conditions();
132 133 134 135 136
	    if (!wanted(s, acc))
	      {
		s->destroy();
		continue;
	      }
137 138
	    res->trans_.emplace_back
	      (transition {s, it->current_condition(), acc});
139
	  }
140
	return res;
141 142
      }

143
      virtual bool wanted(const state* s, acc_cond::mark_t acc) const = 0;
144 145 146 147

    protected:
      const state* init_;
    };
148 149 150 151 152

    class tgba_mask_keep: public tgba_mask
    {
      const state_set& mask_;
    public:
153
      tgba_mask_keep(const const_twa_ptr& masked,
154 155 156 157 158 159 160
		     const state_set& mask,
		     const state* init)
	: tgba_mask(masked, init),
	  mask_(mask)
      {
      }

161
      bool wanted(const state* s, const acc_cond::mark_t) const
162 163 164 165 166 167 168 169 170 171
      {
	state_set::const_iterator i = mask_.find(s);
	return i != mask_.end();
      }
    };

    class tgba_mask_ignore: public tgba_mask
    {
      const state_set& mask_;
    public:
172
      tgba_mask_ignore(const const_twa_ptr& masked,
173 174 175 176 177 178 179
		       const state_set& mask,
		       const state* init)
	: tgba_mask(masked, init),
	  mask_(mask)
      {
      }

180
      bool wanted(const state* s, const acc_cond::mark_t) const
181 182 183 184 185 186 187 188
      {
	state_set::const_iterator i = mask_.find(s);
	return i == mask_.end();
      }
    };

    class tgba_mask_acc_ignore: public tgba_mask
    {
189
      unsigned mask_;
190
    public:
191
      tgba_mask_acc_ignore(const const_twa_ptr& masked,
192
			   unsigned mask,
193 194 195 196 197 198
			   const state* init)
	: tgba_mask(masked, init),
	  mask_(mask)
      {
      }

199
      bool wanted(const state*, const acc_cond::mark_t acc) const
200
      {
201
	return !acc.has(mask_);
202 203 204 205 206
      }
    };

  }

207 208
  const_twa_ptr
  build_tgba_mask_keep(const const_twa_ptr& to_mask,
209 210 211
		       const state_set& to_keep,
		       const state* init)
  {
212
    return std::make_shared<tgba_mask_keep>(to_mask, to_keep, init);
213 214
  }

215 216
  const_twa_ptr
  build_tgba_mask_ignore(const const_twa_ptr& to_mask,
217 218 219
			 const state_set& to_ignore,
			 const state* init)
  {
220
    return std::make_shared<tgba_mask_ignore>(to_mask, to_ignore, init);
221 222
  }

223 224
  const_twa_ptr
  build_tgba_mask_acc_ignore(const const_twa_ptr& to_mask,
225
			     unsigned to_ignore,
226 227
			     const state* init)
  {
228
    return std::make_shared<tgba_mask_acc_ignore>(to_mask, to_ignore, init);
229 230
  }

231
}