tgbaexplicit.cc 9.48 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (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 "ltlast/atomic_prop.hh"
23
#include "ltlast/constant.hh"
24
#include "ltlvisit/destroy.hh"
25
#include "tgbaexplicit.hh"
26
#include "tgba/formula2bdd.hh"
27
28
29
30
31
32
33
34
35
#include <cassert>

namespace spot
{

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

  tgba_explicit_succ_iterator::tgba_explicit_succ_iterator
36
37
  (const tgba_explicit::state* s, bdd all_acc)
    : s_(s), all_accepting_conditions_(all_acc)
38
39
40
  {
  }

41
  void
42
43
44
45
46
  tgba_explicit_succ_iterator::first()
  {
    i_ = s_->begin();
  }

47
  void
48
49
50
51
52
  tgba_explicit_succ_iterator::next()
  {
    ++i_;
  }

53
  bool
54
  tgba_explicit_succ_iterator::done() const
55
56
57
58
  {
    return i_ == s_->end();
  }

59
  state_explicit*
60
  tgba_explicit_succ_iterator::current_state() const
61
62
63
64
  {
    return new state_explicit((*i_)->dest);
  }

65
  bdd
66
  tgba_explicit_succ_iterator::current_condition() const
67
68
69
70
  {
    return (*i_)->condition;
  }

71
  bdd
72
  tgba_explicit_succ_iterator::current_accepting_conditions() const
73
  {
74
    return (*i_)->accepting_conditions & all_accepting_conditions_;
75
76
77
78
79
80
  }


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

81
  const tgba_explicit::state*
82
83
84
85
86
87
88
89
90
91
92
93
94
  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();
  }

95
96
97
98
99
100
101
  size_t
  state_explicit::hash() const
  {
    return
      reinterpret_cast<const char*>(get_state()) - static_cast<const char*>(0);
  }

102
103
104
105
106
107
  state_explicit*
  state_explicit::clone() const
  {
    return new state_explicit(*this);
  }

108
109
110
111
  ////////////////////////////////////////
  // tgba_explicit


112
113
  tgba_explicit::tgba_explicit(bdd_dict* dict)
    : dict_(dict), init_(0), all_accepting_conditions_(bddfalse),
114
115
      neg_accepting_conditions_(bddtrue),
      all_accepting_conditions_computed_(false)
116
117
118
119
120
121
122
123
124
125
126
127
128
  {
  }

  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;
      }
129
    dict_->unregister_all_my_variables(this);
130
  }
131

132
133
134
135
136
137
138
139
140
141
142
  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.
143
	// It can also be overridden with set_init_state().
144
	if (!init_)
145
146
147
148
149
150
151
	  init_ = s;

	return s;
      }
    return i->second;
  }

152
153
154
155
156
157
158
159
  void
  tgba_explicit::set_init_state(const std::string& state)
  {
    tgba_explicit::state* s = add_state(state);
    init_ = s;
  }


160
  tgba_explicit::transition*
161
  tgba_explicit::create_transition(const std::string& source,
162
163
164
165
166
167
168
				   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;
169
    t->accepting_conditions = bddfalse;
170
171
172
173
    s->push_back(t);
    return t;
  }

174
  bdd
175
  tgba_explicit::get_condition(const ltl::formula* f)
176
  {
177
    assert(dynamic_cast<const ltl::atomic_prop*>(f));
178
179
180
    int v = dict_->register_proposition(f, this);
    ltl::destroy(f);
    return bdd_ithvar(v);
181
182
  }

183
  void
184
  tgba_explicit::add_condition(transition* t, const ltl::formula* f)
185
  {
186
187
    t->condition &= formula_to_bdd(f, dict_, this);
    ltl::destroy(f);
188
189
  }

190
  void
191
  tgba_explicit::add_neg_condition(transition* t, const ltl::formula* f)
192
  {
193
    t->condition -= get_condition(f);
194
195
  }

196
197
198
199
200
201
202
  void
  tgba_explicit::add_conditions(transition* t, bdd f)
  {
    dict_->register_propositions(f, this);
    t->condition &= f;
  }

203
  void
204
  tgba_explicit::declare_accepting_condition(const ltl::formula* f)
205
  {
206
207
    int v = dict_->register_accepting_variable(f, this);
    ltl::destroy(f);
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
    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;
	  }
      }
236
237
  }

238
  bool
239
  tgba_explicit::has_accepting_condition(const ltl::formula* f) const
240
  {
241
    return dict_->is_registered_accepting_variable(f, this);
242
243
244
  }

  bdd
245
  tgba_explicit::get_accepting_condition(const ltl::formula* f)
246
  {
247
    const ltl::constant* c = dynamic_cast<const ltl::constant*>(f);
248
249
250
251
252
253
254
255
256
257
258
259
    if (c)
      {
	switch (c->val())
	  {
	  case ltl::constant::True:
	    return bddtrue;
	  case ltl::constant::False:
	    return bddfalse;
	  }
	/* Unreachable code.  */
	assert(0);
      }
260
    bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
261
262
263
    assert(has_accepting_condition(f));
    /* If this second assert fails and the first doesn't,
       things are badly broken.  This has already happened. */
264
    assert(i != dict_->acc_map.end());
265
    ltl::destroy(f);
266
    bdd v = bdd_ithvar(i->second);
267
268
    v &= bdd_exist(neg_accepting_conditions_, v);
    return v;
269
270
  }

271
  void
272
  tgba_explicit::add_accepting_condition(transition* t, const ltl::formula* f)
273
  {
274
275
    bdd c = get_accepting_condition(f);
    t->accepting_conditions |= c;
276
277
  }

278
279
280
281
282
283
284
285
286
287
288
289
290
  void
  tgba_explicit::add_accepting_conditions(transition* t, bdd f)
  {
    bdd sup = bdd_support(f);
    dict_->register_accepting_variables(sup, this);
    while (sup != bddtrue)
      {
	neg_accepting_conditions_ &= bdd_nithvar(bdd_var(sup));
	sup = bdd_high(sup);
      }
    t->accepting_conditions |= f;
  }

291
  state*
292
293
  tgba_explicit::get_init_state() const
  {
294
295
296
    // Fix empty automata by adding a lone initial state.
    if (!init_)
      const_cast<tgba_explicit*>(this)->add_state("empty");
297
298
299
    return new state_explicit(init_);
  }

300
  tgba_succ_iterator*
301
302
303
  tgba_explicit::succ_iter(const spot::state* state,
			   const spot::state* global_state,
			   const tgba* global_automaton) const
304
305
306
  {
    const state_explicit* s = dynamic_cast<const state_explicit*>(state);
    assert(s);
307
308
    (void) global_state;
    (void) global_automaton;
309
310
    return new tgba_explicit_succ_iterator(s->get_state(),
					   all_accepting_conditions());
311
  }
312

313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
  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;
  }

341
  bdd_dict*
342
343
344
345
346
  tgba_explicit::get_dict() const
  {
    return dict_;
  }

347
  std::string
348
349
350
351
352
353
354
355
356
  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;
  }

357
358
359
360
361
362
  bdd
  tgba_explicit::all_accepting_conditions() const
  {
    if (!all_accepting_conditions_computed_)
      {
	bdd all = bddfalse;
363
364
365
366
367
368
369
370

	// Build all_accepting_conditions_ from neg_accepting_conditions_
	// I.e., transform !A & !B & !C into
	//        A & !B & !C
	//     + !A &  B & !C
	//     + !A & !B &  C
	bdd cur = neg_accepting_conditions_;
	while (cur != bddtrue)
371
	  {
372
373
374
	    assert(cur != bddfalse);

	    bdd v = bdd_ithvar(bdd_var(cur));
375
	    all |= v & bdd_exist(neg_accepting_conditions_, v);
376
377
378

	    assert(bdd_high(cur) != bddtrue);
	    cur = bdd_low(cur);
379
380
381
382
383
384
385
386
387
388
389
390
391
	  }
	all_accepting_conditions_ = all;
	all_accepting_conditions_computed_ = true;
      }
    return all_accepting_conditions_;
  }

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

392
}