tgbaexplicit.cc 7.51 KB
Newer Older
1
#include "ltlast/atomic_prop.hh"
2
#include "ltlast/constant.hh"
3
#include "ltlvisit/destroy.hh"
4
5
6
7
8
9
10
11
12
13
#include "tgbaexplicit.hh"
#include <cassert>

namespace spot
{

  ////////////////////////////////////////
  // tgba_explicit_succ_iterator

  tgba_explicit_succ_iterator::tgba_explicit_succ_iterator
14
15
  (const tgba_explicit::state* s, bdd all_acc)
    : s_(s), all_accepting_conditions_(all_acc)
16
17
18
  {
  }

19
  void
20
21
22
23
24
  tgba_explicit_succ_iterator::first()
  {
    i_ = s_->begin();
  }

25
  void
26
27
28
29
30
  tgba_explicit_succ_iterator::next()
  {
    ++i_;
  }

31
  bool
32
  tgba_explicit_succ_iterator::done() const
33
34
35
36
  {
    return i_ == s_->end();
  }

37
  state_explicit*
38
  tgba_explicit_succ_iterator::current_state() const
39
40
41
42
  {
    return new state_explicit((*i_)->dest);
  }

43
  bdd
44
  tgba_explicit_succ_iterator::current_condition() const
45
46
47
48
  {
    return (*i_)->condition;
  }

49
  bdd
50
  tgba_explicit_succ_iterator::current_accepting_conditions() const
51
  {
52
    return (*i_)->accepting_conditions & all_accepting_conditions_;
53
54
55
56
57
58
  }


  ////////////////////////////////////////
  // state_explicit

59
  const tgba_explicit::state*
60
61
62
63
64
65
66
67
68
69
70
71
72
  state_explicit::get_state() const
  {
    return state_;
  }

  int
  state_explicit::compare(const spot::state* other) const
  {
    const state_explicit* o = dynamic_cast<const state_explicit*>(other);
    assert(o);
    return o->get_state() - get_state();
  }

73
74
75
76
77
78
  state_explicit*
  state_explicit::clone() const
  {
    return new state_explicit(*this);
  }

79
80
81
82
  ////////////////////////////////////////
  // tgba_explicit


83
84
  tgba_explicit::tgba_explicit(bdd_dict* dict)
    : dict_(dict), init_(0), all_accepting_conditions_(bddfalse),
85
86
      neg_accepting_conditions_(bddtrue),
      all_accepting_conditions_computed_(false)
87
88
89
90
91
92
93
94
95
96
97
98
99
  {
  }

  tgba_explicit::~tgba_explicit()
  {
    ns_map::iterator i;
    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
      {
	tgba_explicit::state::iterator i2;
	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
	  delete *i2;
	delete i->second;
      }
100
    dict_->unregister_all_my_variables(this);
101
  }
102

103
104
105
106
107
108
109
110
111
112
113
  tgba_explicit::state*
  tgba_explicit::add_state(const std::string& name)
  {
    ns_map::iterator i = name_state_map_.find(name);
    if (i == name_state_map_.end())
      {
	tgba_explicit::state* s = new tgba_explicit::state;
	name_state_map_[name] = s;
	state_name_map_[s] = name;

	// The first state we add is the inititial state.
114
	// It can also be overridden with set_init_state().
115
116
117
118
119
120
121
122
	if (! init_)
	  init_ = s;

	return s;
      }
    return i->second;
  }

123
124
125
126
127
128
129
130
  void
  tgba_explicit::set_init_state(const std::string& state)
  {
    tgba_explicit::state* s = add_state(state);
    init_ = s;
  }


131
  tgba_explicit::transition*
132
  tgba_explicit::create_transition(const std::string& source,
133
134
135
136
137
138
139
				   const std::string& dest)
  {
    tgba_explicit::state* s = add_state(source);
    tgba_explicit::state* d = add_state(dest);
    transition* t = new transition;
    t->dest = d;
    t->condition = bddtrue;
140
    t->accepting_conditions = bddfalse;
141
142
143
144
    s->push_back(t);
    return t;
  }

145
146
  bdd
  tgba_explicit::get_condition(ltl::formula* f)
147
148
  {
    assert(dynamic_cast<ltl::atomic_prop*>(f));
149
150
151
    int v = dict_->register_proposition(f, this);
    ltl::destroy(f);
    return bdd_ithvar(v);
152
153
  }

154
155
  void
  tgba_explicit::add_condition(transition* t, ltl::formula* f)
156
  {
157
    t->condition &= get_condition(f);
158
159
  }

160
161
  void
  tgba_explicit::add_neg_condition(transition* t, ltl::formula* f)
162
  {
163
    t->condition -= get_condition(f);
164
165
  }

166
167
  void
  tgba_explicit::declare_accepting_condition(ltl::formula* f)
168
  {
169
170
    int v = dict_->register_accepting_variable(f, this);
    ltl::destroy(f);
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
    bdd neg = bdd_nithvar(v);
    neg_accepting_conditions_ &= neg;

    // Append neg to all acceptance conditions.
    ns_map::iterator i;
    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
      {
	tgba_explicit::state::iterator i2;
	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
	  (*i2)->accepting_conditions &= neg;
      }

    all_accepting_conditions_computed_ = false;
  }

  void
  tgba_explicit::complement_all_accepting_conditions()
  {
    bdd all = all_accepting_conditions();
    ns_map::iterator i;
    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
      {
	tgba_explicit::state::iterator i2;
	for (i2 = i->second->begin(); i2 != i->second->end(); ++i2)
	  {
	    (*i2)->accepting_conditions = all - (*i2)->accepting_conditions;
	  }
      }
199
200
  }

201
202
203
  bool
  tgba_explicit::has_accepting_condition(ltl::formula* f) const
  {
204
    return dict_->is_registered_accepting_variable(f, this);
205
206
207
208
  }

  bdd
  tgba_explicit::get_accepting_condition(ltl::formula* f)
209
  {
210
211
212
213
214
215
216
217
218
219
220
221
222
    ltl::constant* c = dynamic_cast<ltl::constant*>(f);
    if (c)
      {
	switch (c->val())
	  {
	  case ltl::constant::True:
	    return bddtrue;
	  case ltl::constant::False:
	    return bddfalse;
	  }
	/* Unreachable code.  */
	assert(0);
      }
223
    bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
224
225
226
    assert(has_accepting_condition(f));
    /* If this second assert fails and the first doesn't,
       things are badly broken.  This has already happened. */
227
    assert(i != dict_->acc_map.end());
228
    ltl::destroy(f);
229
    bdd v = bdd_ithvar(i->second);
230
231
    v &= bdd_exist(neg_accepting_conditions_, v);
    return v;
232
233
  }

234
235
  void
  tgba_explicit::add_accepting_condition(transition* t, ltl::formula* f)
236
  {
237
238
    bdd c = get_accepting_condition(f);
    t->accepting_conditions |= c;
239
240
  }

241
  state*
242
243
244
245
246
  tgba_explicit::get_init_state() const
  {
    return new state_explicit(init_);
  }

247
  tgba_succ_iterator*
248
249
250
  tgba_explicit::succ_iter(const spot::state* state,
			   const spot::state* global_state,
			   const tgba* global_automaton) const
251
252
253
  {
    const state_explicit* s = dynamic_cast<const state_explicit*>(state);
    assert(s);
254
255
    (void) global_state;
    (void) global_automaton;
256
257
    return new tgba_explicit_succ_iterator(s->get_state(),
					   all_accepting_conditions());
258
  }
259

260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
  bdd
  tgba_explicit::compute_support_conditions(const spot::state* in) const
  {
    const state_explicit* s = dynamic_cast<const state_explicit*>(in);
    assert(s);
    const state* st = s->get_state();

    bdd res = bddtrue;
    tgba_explicit::state::const_iterator i;
    for (i = st->begin(); i != st->end(); ++i)
      res |= (*i)->condition;
    return res;
  }

  bdd
  tgba_explicit::compute_support_variables(const spot::state* in) const
  {
    const state_explicit* s = dynamic_cast<const state_explicit*>(in);
    assert(s);
    const state* st = s->get_state();

    bdd res = bddtrue;
    tgba_explicit::state::const_iterator i;
    for (i = st->begin(); i != st->end(); ++i)
      res &= bdd_support((*i)->condition);
    return res;
  }

288
  bdd_dict*
289
290
291
292
293
  tgba_explicit::get_dict() const
  {
    return dict_;
  }

294
  std::string
295
296
297
298
299
300
301
302
303
  tgba_explicit::format_state(const spot::state* s) const
  {
    const state_explicit* se = dynamic_cast<const state_explicit*>(s);
    assert(se);
    sn_map::const_iterator i = state_name_map_.find(se->get_state());
    assert(i != state_name_map_.end());
    return i->second;
  }

304
305
306
307
308
309
  bdd
  tgba_explicit::all_accepting_conditions() const
  {
    if (!all_accepting_conditions_computed_)
      {
	bdd all = bddfalse;
310
311
	bdd_dict::fv_map::const_iterator i;
	for (i = dict_->acc_map.begin(); i != dict_->acc_map.end(); ++i)
312
	  {
313
	    bdd v = bdd_ithvar(i->second);
314
315
316
317
318
319
320
321
322
323
324
325
326
327
	    all |= v & bdd_exist(neg_accepting_conditions_, v);
	  }
	all_accepting_conditions_ = all;
	all_accepting_conditions_computed_ = true;
      }
    return all_accepting_conditions_;
  }

  bdd
  tgba_explicit::neg_accepting_conditions() const
  {
    return neg_accepting_conditions_;
  }

328
}