tgbaproduct.cc 7.45 KB
Newer Older
1
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// dpartement Systmes Rpartis Coopratifs (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.

22
#include "tgbaproduct.hh"
23
#include <string>
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
24
#include <cassert>
25
26
27
28
29

namespace spot
{

  ////////////////////////////////////////////////////////////
30
  // state_product
31

32
  state_product::state_product(const state_product& o)
33
    : state(),
34
35
36
37
38
      left_(o.left()->clone()),
      right_(o.right()->clone())
  {
  }

39
  state_product::~state_product()
40
41
42
43
44
  {
    delete left_;
    delete right_;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
45
  int
46
  state_product::compare(const state* other) const
47
  {
48
    const state_product* o = dynamic_cast<const state_product*>(other);
49
50
51
52
53
54
55
    assert(o);
    int res = left_->compare(o->left());
    if (res != 0)
      return res;
    return right_->compare(o->right());
  }

56
57
58
59
60
61
62
  size_t
  state_product::hash() const
  {
    // We assume that size_t has at least 32bits.
    return (left_->hash() << 16) + (right_->hash() & 0xFFFF);
  }

63
64
  state_product*
  state_product::clone() const
65
  {
66
    return new state_product(*this);
67
68
  }

69
  ////////////////////////////////////////////////////////////
70
  // tgba_succ_iterator_product
71

72
  tgba_succ_iterator_product::tgba_succ_iterator_product
73
74
75
76
77
  (tgba_succ_iterator* left, tgba_succ_iterator* right,
   bdd left_neg, bdd right_neg)
    : left_(left), right_(right),
      left_neg_(left_neg),
      right_neg_(right_neg)
78
79
  {
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
80

81
  tgba_succ_iterator_product::~tgba_succ_iterator_product()
82
83
  {
    delete left_;
84
    delete right_;
85
86
  }

87
  void
88
  tgba_succ_iterator_product::step_()
89
90
91
92
93
94
95
96
97
98
  {
    left_->next();
    if (left_->done())
      {
	left_->first();
	right_->next();
      }
  }

  void
99
  tgba_succ_iterator_product::next_non_false_()
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
  {
    while (!done())
      {
	bdd l = left_->current_condition();
	bdd r = right_->current_condition();
	bdd current_cond = l & r;

	if (current_cond != bddfalse)
	  {
	    current_cond_ = current_cond;
	    return;
	  }
	step_();
      }
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
116
  void
117
  tgba_succ_iterator_product::first()
118
  {
119
120
121
    if (!right_)
      return;

122
123
    left_->first();
    right_->first();
124
125
126
127
128
129
130
131
    // If one of the two successor set is empty initially, we reset
    // right_, so that done() can detect this situation easily.  (We
    // choose to reset right_ because this variable is already used by
    // done().)
    if (left_->done() || right_->done())
      {
	delete right_;
	right_ = 0;
132
	return;
133
      }
134
135
136
    next_non_false_();
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
137
  void
138
  tgba_succ_iterator_product::next()
139
140
141
142
143
  {
    step_();
    next_non_false_();
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
144
  bool
145
  tgba_succ_iterator_product::done() const
146
  {
147
    return !right_ || right_->done();
148
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
149
150


151
152
  state_product*
  tgba_succ_iterator_product::current_state() const
153
  {
154
155
    return new state_product(left_->current_state(),
			     right_->current_state());
156
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
157
158

  bdd
159
  tgba_succ_iterator_product::current_condition() const
160
161
162
  {
    return current_cond_;
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
163

164
  bdd tgba_succ_iterator_product::current_acceptance_conditions() const
165
  {
166
167
    return ((left_->current_acceptance_conditions() & right_neg_)
	    | (right_->current_acceptance_conditions() & left_neg_));
168
169
170
  }

  ////////////////////////////////////////////////////////////
171
  // tgba_product
172

173
174
  tgba_product::tgba_product(const tgba* left, const tgba* right)
    : dict_(left->get_dict()), left_(left), right_(right)
175
  {
176
    assert(dict_ == right->get_dict());
177

178
179
    bdd lna = left_->neg_acceptance_conditions();
    bdd rna = right_->neg_acceptance_conditions();
180
181
182
    left_acc_complement_ = bdd_exist(lna, bdd_support(rna));
    right_acc_complement_ = bdd_exist(rna, bdd_support(lna));

183
    all_acceptance_conditions_ = ((left_->all_acceptance_conditions()
184
				  & right_acc_complement_)
185
				 | (right_->all_acceptance_conditions()
186
				    & left_acc_complement_));
187
    neg_acceptance_conditions_ = lna & rna;
188

189
190
    dict_->register_all_variables_of(&left_, this);
    dict_->register_all_variables_of(&right_, this);
191
192
  }

193
  tgba_product::~tgba_product()
194
  {
195
    dict_->unregister_all_my_variables(this);
196
197
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
198
  state*
199
  tgba_product::get_init_state() const
200
  {
201
202
    return new state_product(left_->get_init_state(),
			     right_->get_init_state());
203
204
  }

205
  tgba_succ_iterator_product*
206
207
208
  tgba_product::succ_iter(const state* local_state,
			  const state* global_state,
			  const tgba* global_automaton) const
209
  {
210
211
    const state_product* s =
      dynamic_cast<const state_product*>(local_state);
212
213
    assert(s);

214
215
    // If global_automaton is not specified, THIS is the root of a
    // product tree.
216
    if (!global_automaton)
217
218
219
220
221
222
223
224
225
      {
	global_automaton = this;
	global_state = local_state;
      }

    tgba_succ_iterator* li = left_->succ_iter(s->left(),
					      global_state, global_automaton);
    tgba_succ_iterator* ri = right_->succ_iter(s->right(),
					       global_state, global_automaton);
226
    return new tgba_succ_iterator_product(li, ri,
227
228
					  left_acc_complement_,
					  right_acc_complement_);
229
230
  }

231
232
233
  bdd
  tgba_product::compute_support_conditions(const state* in) const
  {
234
    const state_product* s = dynamic_cast<const state_product*>(in);
235
236
237
238
239
240
241
242
243
    assert(s);
    bdd lsc = left_->support_conditions(s->left());
    bdd rsc = right_->support_conditions(s->right());
    return lsc & rsc;
  }

  bdd
  tgba_product::compute_support_variables(const state* in) const
  {
244
    const state_product* s = dynamic_cast<const state_product*>(in);
245
246
247
248
249
250
    assert(s);
    bdd lsc = left_->support_variables(s->left());
    bdd rsc = right_->support_variables(s->right());
    return lsc & rsc;
  }

251
  bdd_dict*
252
  tgba_product::get_dict() const
253
254
255
256
  {
    return dict_;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
257
  std::string
258
  tgba_product::format_state(const state* state) const
259
  {
260
    const state_product* s = dynamic_cast<const state_product*>(state);
261
    assert(s);
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
262
263
    return (left_->format_state(s->left())
	    + " * "
264
265
	    + right_->format_state(s->right()));
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
266

267
268
269
  state*
  tgba_product::project_state(const state* s, const tgba* t) const
  {
270
    const state_product* s2 = dynamic_cast<const state_product*>(s);
271
272
273
274
275
276
277
278
279
    assert(s2);
    if (t == this)
      return s2->clone();
    state* res = left_->project_state(s2->left(), t);
    if (res)
      return res;
    return right_->project_state(s2->right(), t);
  }

280
  bdd
281
  tgba_product::all_acceptance_conditions() const
282
  {
283
    return all_acceptance_conditions_;
284
285
286
  }

  bdd
287
  tgba_product::neg_acceptance_conditions() const
288
  {
289
    return neg_acceptance_conditions_;
290
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
291

292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
  std::string
  tgba_product::transition_annotation(const tgba_succ_iterator* t) const
  {
    const tgba_succ_iterator_product* i =
      dynamic_cast<const tgba_succ_iterator_product*>(t);
    assert(i);
    std::string left = left_->transition_annotation(i->left_);
    std::string right = right_->transition_annotation(i->right_);
    if (left == "")
      return right;
    if (right == "")
      return left;
    return "<" + left + ", " + right + ">";
  }

307
}