tgbatba.cc 5.6 KB
Newer Older
1
2
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
#include <cassert>
#include "tgbatba.hh"
#include "bddprint.hh"
#include "ltlast/constant.hh"

namespace spot
{

  /// \brief A state for spot::tgba_tba_proxy.
  ///
  /// This state is in fact a pair of state: the state from the tgba
  /// automaton, and the "counter" (we use the accepting set
  /// BDD variable instead of an integer counter).
  class state_tba_proxy : public state
  {
  public:
    state_tba_proxy(state* s, bdd acc)
      :	s_(s), acc_(acc)
    {
    }

    /// Copy constructor
    state_tba_proxy(const state_tba_proxy& o)
      : state(),
	s_(o.real_state()->clone()),
	acc_(o.accepting_cond())
    {
    }

30
    virtual
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
    ~state_tba_proxy()
    {
      delete s_;
    }

    state*
    real_state() const
    {
      return s_;
    }

    bdd
    accepting_cond() const
    {
      return acc_;
    }

48
    virtual int
49
50
51
52
53
54
55
56
57
    compare(const state* other) const
    {
      const state_tba_proxy* o = dynamic_cast<const state_tba_proxy*>(other);
      assert(o);
      int res = s_->compare(o->real_state());
      if (res != 0)
	return res;
      return acc_.id() - o->accepting_cond().id();
    }
58
59

    virtual
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
    state_tba_proxy* clone() const
    {
      return new state_tba_proxy(*this);
    }

  private:
    state* s_;
    bdd acc_;
  };


  /// \brief Iterate over the successors of tgba_tba_proxy computed on the fly.
  class tgba_tba_proxy_succ_iterator: public tgba_succ_iterator
  {
  public:
    tgba_tba_proxy_succ_iterator(tgba_succ_iterator* it,
				 bdd acc, bdd next_acc,
				 bdd the_accepting_cond)
78
      : it_(it), acc_(acc), next_acc_(next_acc),
79
80
81
82
83
84
85
86
87
88
89
	the_accepting_cond_(the_accepting_cond)
    {
    }

    virtual
    ~tgba_tba_proxy_succ_iterator()
    {
    }

    // iteration

90
    void
91
92
93
94
95
    first()
    {
      it_->first();
    }

96
    void
97
98
99
100
101
    next()
    {
      it_->next();
    }

102
    bool
103
104
105
106
107
108
109
    done() const
    {
      return it_->done();
    }

    // inspection

110
    state_tba_proxy*
111
112
113
114
115
116
    current_state() const
    {
      state* s = it_->current_state();
      bdd acc;
      // Transition in the ACC_ accepting set should be directed
      // to the NEXT_ACC_ accepting set.
117
      if (acc_ == bddtrue
118
119
120
121
122
123
124
	  || (acc_ & it_->current_accepting_conditions()) == acc_)
	acc = next_acc_;
      else
	acc = acc_;
      return new state_tba_proxy(s, acc);
    }

125
    bdd
126
127
128
129
130
    current_condition() const
    {
      return it_->current_condition();
    }

131
    bdd
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
    current_accepting_conditions() const
    {
      return the_accepting_cond_;
    }

  protected:
    tgba_succ_iterator* it_;
    bdd acc_;
    bdd next_acc_;
    bdd the_accepting_cond_;
  };


  tgba_tba_proxy::tgba_tba_proxy(const tgba* a)
    : a_(a)
  {
    bdd all = a_->all_accepting_conditions();

    // We will use one accepting condition for this automata.
    // Let's call it Acc[True].
    int v = get_dict()
      ->register_accepting_variable(ltl::constant::true_instance(), this);
    the_accepting_cond_ = bdd_ithvar(v);

    // Now build the "cycle" of accepting conditions.

    bdd last = bdd_satone(all);
    all &= !last;

    acc_cycle_[bddtrue] = last;

    while (all != bddfalse)
      {
	bdd next = bdd_satone(all);
	all &= !next;
	acc_cycle_[last] = next;
	last = next;
      }

    acc_cycle_[last] = bddtrue;
  }

  tgba_tba_proxy::~tgba_tba_proxy()
  {
    get_dict()->unregister_all_my_variables(this);
  }

179
  state*
180
181
182
183
184
185
186
187
188
189
190
191
  tgba_tba_proxy::get_init_state() const
  {
    cycle_map::const_iterator i = acc_cycle_.find(bddtrue);
    assert(i != acc_cycle_.end());
    return new state_tba_proxy(a_->get_init_state(), i->second);
  }

  tgba_succ_iterator*
  tgba_tba_proxy::succ_iter(const state* local_state,
			    const state* global_state,
			    const tgba* global_automaton) const
  {
192
    const state_tba_proxy* s =
193
194
195
      dynamic_cast<const state_tba_proxy*>(local_state);
    assert(s);

196
    tgba_succ_iterator* it = a_->succ_iter(s->real_state(),
197
198
199
200
					   global_state, global_automaton);
    bdd acc = s->accepting_cond();
    cycle_map::const_iterator i = acc_cycle_.find(acc);
    assert(i != acc_cycle_.end());
201
    return
202
      new tgba_tba_proxy_succ_iterator(it, acc, i->second,
203
				       (acc == bddtrue)
204
205
				       ? the_accepting_cond_ : bddfalse);
  }
206
207

  bdd_dict*
208
209
210
211
  tgba_tba_proxy::get_dict() const
  {
    return a_->get_dict();
  }
212
213

  std::string
214
215
  tgba_tba_proxy::format_state(const state* state) const
  {
216
    const state_tba_proxy* s = dynamic_cast<const state_tba_proxy*>(state);
217
    assert(s);
218
    return a_->format_state(s->real_state()) + "("
219
220
      + bdd_format_set(get_dict(), s->accepting_cond()) + ")";
  }
221

222
  state*
223
224
225
226
227
228
229
230
231
232
  tgba_tba_proxy::project_state(const state* s, const tgba* t) const
  {
    const state_tba_proxy* s2 = dynamic_cast<const state_tba_proxy*>(s);
    assert(s2);
    if (t == this)
      return s2->clone();
    return a_->project_state(s2->real_state(), t);
  }


233
  bdd
234
235
236
237
  tgba_tba_proxy::all_accepting_conditions() const
  {
    return the_accepting_cond_;
  }
238
239

  bdd
240
241
242
243
  tgba_tba_proxy::neg_accepting_conditions() const
  {
    return !the_accepting_cond_;
  }
244
245
246
247
248
249
250
251
252
253
254

  bool
  tgba_tba_proxy::state_is_accepting(const state* state) const
  {
    const state_tba_proxy* s =
      dynamic_cast<const state_tba_proxy*>(state);
    assert(s);
    return bddtrue == s->accepting_cond();
  }

  bdd
255
256
  tgba_tba_proxy::compute_support_conditions(const state* state) const
  {
257
    const state_tba_proxy* s =
258
259
260
261
      dynamic_cast<const state_tba_proxy*>(state);
    assert(s);
    return a_->support_conditions(s->real_state());
  }
262
263

  bdd
264
265
  tgba_tba_proxy::compute_support_variables(const state* state) const
  {
266
    const state_tba_proxy* s =
267
268
269
270
271
272
      dynamic_cast<const state_tba_proxy*>(state);
    assert(s);
    return a_->support_variables(s->real_state());
  }

}