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
    /// \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.
87
    class tgba_mask: public twa_proxy
88
89
90
91
92
93
    {
    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
	twa_proxy(masked),
96
97
98
99
100
	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
}