tgbaproduct.cc 5.1 KB
Newer Older
1
2
#include "tgbaproduct.hh"
#include "tgbatranslateproxy.hh"
3
#include "dictunion.hh"
4
#include <string>
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
5
#include <cassert>
6
7
8
9
10
11
12

namespace spot
{

  ////////////////////////////////////////////////////////////
  // state_bdd_product

13
  state_bdd_product::state_bdd_product(const state_bdd_product& o)
14
    : state(),
15
16
17
18
19
      left_(o.left()->clone()),
      right_(o.right()->clone())
  {
  }

20
21
22
23
24
25
  state_bdd_product::~state_bdd_product()
  {
    delete left_;
    delete right_;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
26
  int
27
28
29
30
31
32
33
34
35
36
  state_bdd_product::compare(const state* other) const
  {
    const state_bdd_product* o = dynamic_cast<const state_bdd_product*>(other);
    assert(o);
    int res = left_->compare(o->left());
    if (res != 0)
      return res;
    return right_->compare(o->right());
  }

37
38
39
40
41
42
  state_bdd_product*
  state_bdd_product::clone() const
  {
    return new state_bdd_product(*this);
  }

43
  ////////////////////////////////////////////////////////////
44
  // tgba_product_succ_iterator
45

46
  tgba_product_succ_iterator::tgba_product_succ_iterator
47
48
49
50
51
  (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)
52
53
  {
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
54

55
  tgba_product_succ_iterator::~tgba_product_succ_iterator()
56
57
58
59
60
61
  {
    delete left_;
    if (right_)
      delete right_;
  }

62
  void
63
  tgba_product_succ_iterator::step_()
64
65
66
67
68
69
70
71
72
73
  {
    left_->next();
    if (left_->done())
      {
	left_->first();
	right_->next();
      }
  }

  void
74
  tgba_product_succ_iterator::next_non_false_()
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
  {
    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
91
  void
92
  tgba_product_succ_iterator::first()
93
  {
94
95
96
    if (!right_)
      return;

97
98
    left_->first();
    right_->first();
99
100
101
102
103
104
105
106
107
    // 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;
      }
108
109
110
    next_non_false_();
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
111
  void
112
  tgba_product_succ_iterator::next()
113
114
115
116
117
  {
    step_();
    next_non_false_();
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
118
  bool
119
  tgba_product_succ_iterator::done() const
120
  {
121
    return !right_ || right_->done();
122
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
123
124


125
  state_bdd_product*
126
  tgba_product_succ_iterator::current_state()
127
  {
128
129
    return new state_bdd_product(left_->current_state(),
				 right_->current_state());
130
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
131
132

  bdd
133
  tgba_product_succ_iterator::current_condition()
134
135
136
  {
    return current_cond_;
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
137

138
  bdd tgba_product_succ_iterator::current_accepting_conditions()
139
  {
140
141
    return ((left_->current_accepting_conditions() & right_neg_)
	    | (right_->current_accepting_conditions() & left_neg_));
142
143
144
  }

  ////////////////////////////////////////////////////////////
145
  // tgba_product
146

147
  tgba_product::tgba_product(const tgba& left, const tgba& right)
148
149
150
151
152
153
154
155
156
157
    : dict_(tgba_bdd_dict_union(left.get_dict(), right.get_dict()))
  {
    // Translate the left automaton if needed.
    if (dict_.contains(left.get_dict()))
      {
	left_ = &left;
	left_should_be_freed_ = false;
      }
    else
      {
158
	left_ = new tgba_translate_proxy(left, dict_);
159
160
161
162
163
164
165
166
167
168
169
	left_should_be_freed_ = true;
      }

    // Translate the right automaton if needed.
    if (dict_.contains(right.get_dict()))
      {
	right_ = &right;
	right_should_be_freed_ = false;
      }
    else
      {
170
	right_ = new tgba_translate_proxy(right, dict_);
171
172
	right_should_be_freed_ = true;
      }
173
174
175
176
177
178
179

    all_accepting_conditions_ = ((left_->all_accepting_conditions()
				  & right_->neg_accepting_conditions())
				 | (right_->all_accepting_conditions()
				    & left_->neg_accepting_conditions()));
    neg_accepting_conditions_ = (left_->neg_accepting_conditions()
				 & right_->neg_accepting_conditions());
180
181
  }

182
  tgba_product::~tgba_product()
183
184
185
186
187
188
189
  {
    if (left_should_be_freed_)
      delete left_;
    if (right_should_be_freed_)
      delete right_;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
190
  state*
191
  tgba_product::get_init_state() const
192
  {
193
194
    return new state_bdd_product(left_->get_init_state(),
				 right_->get_init_state());
195
196
  }

197
198
  tgba_product_succ_iterator*
  tgba_product::succ_iter(const state* state) const
199
200
201
202
203
204
  {
    const state_bdd_product* s = dynamic_cast<const state_bdd_product*>(state);
    assert(s);

    tgba_succ_iterator* li = left_->succ_iter(s->left());
    tgba_succ_iterator* ri = right_->succ_iter(s->right());
205
206
207
    return new tgba_product_succ_iterator(li, ri,
					  left_->neg_accepting_conditions(),
					  right_->neg_accepting_conditions());
208
209
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
210
  const tgba_bdd_dict&
211
  tgba_product::get_dict() const
212
213
214
215
  {
    return dict_;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
216
  std::string
217
  tgba_product::format_state(const state* state) const
218
219
220
  {
    const state_bdd_product* s = dynamic_cast<const state_bdd_product*>(state);
    assert(s);
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
221
222
    return (left_->format_state(s->left())
	    + " * "
223
224
	    + right_->format_state(s->right()));
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
225

226
227
228
229
230
231
232
233
234
235
236
  bdd
  tgba_product::all_accepting_conditions() const
  {
    return all_accepting_conditions_;
  }

  bdd
  tgba_product::neg_accepting_conditions() const
  {
    return neg_accepting_conditions_;
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
237

238
}