tgbaexplicit.cc 6.4 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
114
115
116
117
118
119
120
121
122
  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.
	if (! init_)
	  init_ = s;

	return s;
      }
    return i->second;
  }

  tgba_explicit::transition*
123
  tgba_explicit::create_transition(const std::string& source,
124
125
126
127
128
129
130
				   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;
131
    t->accepting_conditions = bddfalse;
132
133
134
135
    s->push_back(t);
    return t;
  }

136
137
  bdd
  tgba_explicit::get_condition(ltl::formula* f)
138
139
  {
    assert(dynamic_cast<ltl::atomic_prop*>(f));
140
141
142
    int v = dict_->register_proposition(f, this);
    ltl::destroy(f);
    return bdd_ithvar(v);
143
144
  }

145
146
  void
  tgba_explicit::add_condition(transition* t, ltl::formula* f)
147
  {
148
    t->condition &= get_condition(f);
149
150
  }

151
152
  void
  tgba_explicit::add_neg_condition(transition* t, ltl::formula* f)
153
  {
154
    t->condition -= get_condition(f);
155
156
  }

157
158
  void
  tgba_explicit::declare_accepting_condition(ltl::formula* f)
159
  {
160
161
162
    int v = dict_->register_accepting_variable(f, this);
    ltl::destroy(f);
    neg_accepting_conditions_ &= bdd_nithvar(v);
163
164
  }

165
166
167
  bool
  tgba_explicit::has_accepting_condition(ltl::formula* f) const
  {
168
    return dict_->is_registered(f, this);
169
170
171
172
  }

  bdd
  tgba_explicit::get_accepting_condition(ltl::formula* f)
173
  {
174
175
176
177
178
179
180
181
182
183
184
185
186
    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);
      }
187
188
    bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
    assert(i != dict_->acc_map.end());
189
    ltl::destroy(f);
190
    bdd v = bdd_ithvar(i->second);
191
192
    v &= bdd_exist(neg_accepting_conditions_, v);
    return v;
193
194
  }

195
196
  void
  tgba_explicit::add_accepting_condition(transition* t, ltl::formula* f)
197
  {
198
199
    bdd c = get_accepting_condition(f);
    t->accepting_conditions |= c;
200
201
  }

202
  state*
203
204
205
206
207
  tgba_explicit::get_init_state() const
  {
    return new state_explicit(init_);
  }

208
  tgba_succ_iterator*
209
210
211
  tgba_explicit::succ_iter(const spot::state* state,
			   const spot::state* global_state,
			   const tgba* global_automaton) const
212
213
214
  {
    const state_explicit* s = dynamic_cast<const state_explicit*>(state);
    assert(s);
215
216
    (void) global_state;
    (void) global_automaton;
217
218
    return new tgba_explicit_succ_iterator(s->get_state(),
					   all_accepting_conditions());
219
  }
220

221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
  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;
  }

249
  bdd_dict*
250
251
252
253
254
  tgba_explicit::get_dict() const
  {
    return dict_;
  }

255
  std::string
256
257
258
259
260
261
262
263
264
  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;
  }

265
266
267
268
269
270
  bdd
  tgba_explicit::all_accepting_conditions() const
  {
    if (!all_accepting_conditions_computed_)
      {
	bdd all = bddfalse;
271
272
	bdd_dict::fv_map::const_iterator i;
	for (i = dict_->acc_map.begin(); i != dict_->acc_map.end(); ++i)
273
	  {
274
	    bdd v = bdd_ithvar(i->second);
275
276
277
278
279
280
281
282
283
284
285
286
287
288
	    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_;
  }

289
}