tgbaexplicit.cc 7.77 KB
Newer Older
1
// Copyright (C) 2003, 2004, 2009  Laboratoire d'Informatique de Paris 6 (LIP6),
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// dpartement Systmes Rpartis Coopratifs (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
23
#include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
24
#include "tgbaexplicit.hh"
25
#include "tgba/formula2bdd.hh"
26
#include "misc/bddop.hh"
27
#include <cassert>
28
#include "ltlvisit/tostring.hh"
29
30
31
32
33
34
35
36

namespace spot
{

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

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

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

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

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

60
  state_explicit*
61
  tgba_explicit_succ_iterator::current_state() const
62
  {
63
    assert(!done());
64
65
66
    return new state_explicit((*i_)->dest);
  }

67
  bdd
68
  tgba_explicit_succ_iterator::current_condition() const
69
  {
70
    assert(!done());
71
72
73
    return (*i_)->condition;
  }

74
  bdd
75
  tgba_explicit_succ_iterator::current_acceptance_conditions() const
76
  {
77
    assert(!done());
78
    return (*i_)->acceptance_conditions & all_acceptance_conditions_;
79
80
81
82
83
84
  }


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

85
  const tgba_explicit::state*
86
87
88
89
90
91
92
93
94
95
96
97
98
  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();
  }

99
100
101
102
103
104
105
  size_t
  state_explicit::hash() const
  {
    return
      reinterpret_cast<const char*>(get_state()) - static_cast<const char*>(0);
  }

106
107
108
109
110
111
  state_explicit*
  state_explicit::clone() const
  {
    return new state_explicit(*this);
  }

112
113
114
115
  ////////////////////////////////////////
  // tgba_explicit


116
  tgba_explicit::tgba_explicit(bdd_dict* dict)
117
118
119
    : dict_(dict), init_(0), all_acceptance_conditions_(bddfalse),
      neg_acceptance_conditions_(bddtrue),
      all_acceptance_conditions_computed_(false)
120
121
122
123
124
  {
  }

  tgba_explicit::~tgba_explicit()
  {
125
    dict_->unregister_all_my_variables(this);
126
  }
127

128
  tgba_explicit::transition*
129
  tgba_explicit::create_transition(state* source, const state* dest)
130
131
  {
    transition* t = new transition;
132
    t->dest = dest;
133
    t->condition = bddtrue;
134
    t->acceptance_conditions = bddfalse;
135
    source->push_back(t);
136
137
    return t;
  }
138
  void
139
  tgba_explicit::add_condition(transition* t, const ltl::formula* f)
140
  {
141
    t->condition &= formula_to_bdd(f, dict_, this);
142
    f->destroy();
143
144
  }

145
146
147
148
149
150
151
  void
  tgba_explicit::add_conditions(transition* t, bdd f)
  {
    dict_->register_propositions(f, this);
    t->condition &= f;
  }

152
153
154
155
156
157
158
159
160
161
  void
  tgba_explicit::copy_acceptance_conditions_of(const tgba *a)
  {
    assert(neg_acceptance_conditions_ == bddtrue);
    assert(all_acceptance_conditions_computed_ == false);
    bdd f = a->neg_acceptance_conditions();
    dict_->register_acceptance_variables(f, this);
    neg_acceptance_conditions_ = f;
  }

162
  bool
163
  tgba_explicit::has_acceptance_condition(const ltl::formula* f) const
164
  {
165
    return dict_->is_registered_acceptance_variable(f, this);
166
167
168
  }

  bdd
169
  tgba_explicit::get_acceptance_condition(const ltl::formula* f)
170
  {
171
    bdd_dict::fv_map::iterator i = dict_->acc_map.find(f);
172
    assert(has_acceptance_condition(f));
173
174
    /* If this second assert fails and the first doesn't,
       things are badly broken.  This has already happened. */
175
    assert(i != dict_->acc_map.end());
176
    f->destroy();
177
    bdd v = bdd_ithvar(i->second);
178
    v &= bdd_exist(neg_acceptance_conditions_, v);
179
    return v;
180
181
  }

182
  void
183
  tgba_explicit::add_acceptance_condition(transition* t, const ltl::formula* f)
184
  {
185
186
    bdd c = get_acceptance_condition(f);
    t->acceptance_conditions |= c;
187
188
  }

189
  void
190
  tgba_explicit::add_acceptance_conditions(transition* t, bdd f)
191
192
  {
    bdd sup = bdd_support(f);
193
    dict_->register_acceptance_variables(sup, this);
194
195
    while (sup != bddtrue)
      {
196
	neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup));
197
198
	sup = bdd_high(sup);
      }
199
    t->acceptance_conditions |= f;
200
201
  }

202
  state*
203
204
  tgba_explicit::get_init_state() const
  {
205
206
    // Fix empty automata by adding a lone initial state.
    if (!init_)
207
      const_cast<tgba_explicit*>(this)->add_default_init();
208
209
210
    return new state_explicit(init_);
  }

211
  tgba_succ_iterator*
212
213
214
  tgba_explicit::succ_iter(const spot::state* state,
			   const spot::state* global_state,
			   const tgba* global_automaton) const
215
216
217
  {
    const state_explicit* s = dynamic_cast<const state_explicit*>(state);
    assert(s);
218
219
    (void) global_state;
    (void) global_automaton;
220
    return new tgba_explicit_succ_iterator(s->get_state(),
221
					   all_acceptance_conditions());
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
249
250
251
  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;
  }

252
  bdd_dict*
253
254
255
256
257
  tgba_explicit::get_dict() const
  {
    return dict_;
  }

258
  bdd
259
  tgba_explicit::all_acceptance_conditions() const
260
  {
261
    if (!all_acceptance_conditions_computed_)
262
      {
263
264
	all_acceptance_conditions_ =
	  compute_all_acceptance_conditions(neg_acceptance_conditions_);
265
	all_acceptance_conditions_computed_ = true;
266
      }
267
    return all_acceptance_conditions_;
268
269
270
  }

  bdd
271
  tgba_explicit::neg_acceptance_conditions() const
272
  {
273
    return neg_acceptance_conditions_;
274
275
  }

276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
  tgba_explicit::state*
  tgba_explicit_string::add_default_init()
  {
    return add_state("empty");
  }

  std::string
  tgba_explicit_string::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;
  }

  tgba_explicit_formula::~tgba_explicit_formula()
  {
    ns_map::iterator i;
    for (i = name_state_map_.begin(); i != name_state_map_.end(); ++i)
      i->first->destroy();
  }

  tgba_explicit::state* tgba_explicit_formula::add_default_init()
  {
    return add_state(ltl::constant::true_instance());
  }

  std::string
  tgba_explicit_formula::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 ltl::to_string(i->second);
  }

314
}