taexplicit.cc 12.7 KB
Newer Older
1
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement
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
30
31
32
33
34
35
36
// de l Epita (LRDE).
//
// 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.

#include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
#include "taexplicit.hh"
#include "tgba/formula2bdd.hh"
#include "misc/bddop.hh"
#include <cassert>
#include "ltlvisit/tostring.hh"

#include "tgba/bddprint.hh"

namespace spot
{

  ////////////////////////////////////////
  // ta_explicit_succ_iterator

37
38
39
  ta_explicit_succ_iterator::ta_explicit_succ_iterator(
      const state_ta_explicit* s) :
    source_(s)
40
41
42
43
  {
    transitions_ = s->get_transitions();
  }

44
45
46
47
48
49
50
  ta_explicit_succ_iterator::ta_explicit_succ_iterator(
      const state_ta_explicit* s, bdd condition) :
    source_(s)
  {
    transitions_ = s->get_transitions(condition);
  }

51
52
53
  void
  ta_explicit_succ_iterator::first()
  {
54
55
    if (transitions_ != 0)
      i_ = transitions_->begin();
56
57
58
59
60
61
62
63
64
65
66
  }

  void
  ta_explicit_succ_iterator::next()
  {
    ++i_;
  }

  bool
  ta_explicit_succ_iterator::done() const
  {
67
68
    return transitions_ == 0 || transitions_->empty() || i_
        == transitions_->end();
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
  }

  state*
  ta_explicit_succ_iterator::current_state() const
  {
    assert(!done());
    state_ta_explicit* s = (*i_)->dest;
    return s;
  }

  bdd
  ta_explicit_succ_iterator::current_condition() const
  {
    assert(!done());
    return (*i_)->condition;
  }

86
87
88
89
90
  bool
  ta_explicit_succ_iterator::is_stuttering_transition() const
  {
    return source_->get_tgba_condition() == ((*i_)->dest)->get_tgba_condition();
  }
91
92
93
94
95
96
97
98
99
100

  ////////////////////////////////////////
  // state_ta_explicit

  state_ta_explicit::transitions*
  state_ta_explicit::get_transitions() const
  {
    return transitions_;
  }

101
102
103
104
105
106
  // return transitions filtred by condition
  state_ta_explicit::transitions*
  state_ta_explicit::get_transitions(bdd condition) const
  {

    Sgi::hash_map<int, transitions*, Sgi::hash<int> >::const_iterator i =
107
        transitions_by_condition.find(condition.id());
108
109
110

    if (i == transitions_by_condition.end())
      {
111
        return 0;
112
113
114
      }
    else
      {
115
        return i->second;
116
117
118
      }

  }
119
120

  void
121
122
123
124
  state_ta_explicit::add_transition(state_ta_explicit::transition* t)
  {
    if (transitions_ == 0)
      transitions_ = new transitions;
125

126
127
128
129
    transitions* transitions_condition = get_transitions(t->condition);

    if (transitions_condition == 0)
      {
130
131
132
133
134
135
136
137
138
139
140
        transitions_condition = new transitions;
        transitions_by_condition[(t->condition).id()] = transitions_condition;
      }

    state_ta_explicit::transitions::iterator it_trans;
    bool transition_found = false;

    for (it_trans = transitions_condition->begin(); (it_trans
        != transitions_condition->end() && !transition_found); it_trans++)
      {
        transition_found = ((*it_trans)->dest == t->dest);
141
      }
142

143
144
145
146
147
148
149
150
151
    if (!transition_found)
      {
        transitions_condition->push_back(t);
        transitions_->push_back(t);
      }
    else
      {
        delete t;
      }
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
179
180
181
182
183
184
185
186
187
188
189
190
191

  const state*
  state_ta_explicit::get_tgba_state() const
  {
    return tgba_state_;
  }

  const bdd
  state_ta_explicit::get_tgba_condition() const
  {
    return tgba_condition_;
  }

  bool
  state_ta_explicit::is_accepting_state() const
  {
    return is_accepting_state_;
  }

  bool
  state_ta_explicit::is_initial_state() const
  {
    return is_initial_state_;
  }

  void
  state_ta_explicit::set_accepting_state(bool is_accepting_state)
  {
    is_accepting_state_ = is_accepting_state;
  }

  bool
  state_ta_explicit::is_livelock_accepting_state() const
  {
    return is_livelock_accepting_state_;
  }

  void
192
193
  state_ta_explicit::set_livelock_accepting_state(
      bool is_livelock_accepting_state)
194
195
196
197
198
199
200
201
202
203
  {
    is_livelock_accepting_state_ = is_livelock_accepting_state;
  }

  void
  state_ta_explicit::set_initial_state(bool is_initial_state)
  {
    is_initial_state_ = is_initial_state;
  }

204
205
206
207
208
209
210
  bool
  state_ta_explicit::is_hole_state() const
  {
    state_ta_explicit::transitions* trans = get_transitions();
    return trans == 0 || trans->empty();
  }

211
212
213
  int
  state_ta_explicit::compare(const spot::state* other) const
  {
214
    const state_ta_explicit* o = down_cast<const state_ta_explicit*> (other);
215
216
217
218
219
220
221
    assert(o);

    int compare_value = tgba_state_->compare(o->tgba_state_);

    if (compare_value != 0)
      return compare_value;

222
223
224
225
226
227
228
229
230
231
    compare_value = tgba_condition_.id() - o->tgba_condition_.id();

    //    if (compare_value != 0)
    //      return compare_value;
    //
    //    //unique artificial_livelock_accepting_state
    //    if (o->is_the_artificial_livelock_accepting_state())
    //      return is_the_artificial_livelock_accepting_state();

    return compare_value;
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
  }

  size_t
  state_ta_explicit::hash() const
  {
    return wang32_hash(tgba_state_->hash()) ^ wang32_hash(tgba_condition_.id());
  }

  state_ta_explicit*
  state_ta_explicit::clone() const
  {
    return new state_ta_explicit(*this);
  }

  void
247
248
249
250
251
252
253
  state_ta_explicit::delete_stuttering_and_hole_successors()
  {
    state_ta_explicit::transitions* trans = get_transitions();
    state_ta_explicit::transitions::iterator it_trans;

    if (trans != 0)
      for (it_trans = trans->begin(); it_trans != trans->end();)
254
255
256
257
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
        {
          state_ta_explicit* dest = (*it_trans)->dest;
          bool is_stuttering_transition = (get_tgba_condition()
              == (dest)->get_tgba_condition());
          bool dest_is_livelock_accepting = dest->is_livelock_accepting_state();

          //Before deleting stuttering transitions, propaged back livelock and initial state's properties
          if (is_stuttering_transition)
            {
              if (dest_is_livelock_accepting)
                set_livelock_accepting_state(true);
              if (dest->is_initial_state())
                set_initial_state(true);
            }

          //remove hole successors states
          state_ta_explicit::transitions* dest_trans =
              (dest)->get_transitions();
          bool dest_trans_empty = dest_trans == 0 || dest_trans->empty();
          if (is_stuttering_transition || (dest_trans_empty
              && (!dest_is_livelock_accepting)))
            {
              get_transitions((*it_trans)->condition)->remove(*it_trans);
              delete (*it_trans);
              it_trans = trans->erase(it_trans);
            }
          else
            {
              it_trans++;
            }
        }
285
286
287

  }

288
289
290
291
292
293
294
295
296
  void
  state_ta_explicit::free_transitions()
  {
    state_ta_explicit::transitions* trans = get_transitions();
    state_ta_explicit::transitions::iterator it_trans;
    // We don't destroy the transitions in the state's destructor because
    // they are not cloned.
    if (trans != 0)
      for (it_trans = trans->begin(); it_trans != trans->end(); it_trans++)
297
298
299
        {
          delete *it_trans;
        }
300
301
302
    delete trans;

    Sgi::hash_map<int, transitions*, Sgi::hash<int> >::iterator i =
303
        transitions_by_condition.begin();
304
305
    while (i != transitions_by_condition.end())
      {
306
307
        delete i->second;
        ++i;
308
      }
309
310
311
312
313
314
315

  }

  ////////////////////////////////////////
  // ta_explicit


316
317
318
  ta_explicit::ta_explicit(const tgba* tgba_,
      state_ta_explicit* artificial_initial_state) :
    tgba_(tgba_), artificial_initial_state_(artificial_initial_state)
319
  {
320
    get_dict()->register_all_variables_of(&tgba_, this);
321
322
323
324
325
326
    if (artificial_initial_state != 0)
      {
        state_ta_explicit* is = add_state(artificial_initial_state);
        assert(is == artificial_initial_state);
      }

327
328
329
330
331
332
333
  }

  ta_explicit::~ta_explicit()
  {
    ta::states_set_t::iterator it;
    for (it = states_set_.begin(); it != states_set_.end(); it++)
      {
334
        state_ta_explicit* s = down_cast<state_ta_explicit*> (*it);
335

336
337
338
        s->free_transitions();
        s->get_tgba_state()->destroy();
        delete s;
339
      }
340
341
    get_dict()->unregister_all_my_variables(this);
    delete tgba_;
342
343
344
345
346
347
  }

  state_ta_explicit*
  ta_explicit::add_state(state_ta_explicit* s)
  {
    std::pair<ta::states_set_t::iterator, bool> add_state_to_ta =
348
        states_set_.insert(s);
349

350
    return static_cast<state_ta_explicit*> (*add_state_to_ta.first);
351
352
353

  }

354
  void
355
  ta_explicit::add_to_initial_states_set(state* state, bdd condition)
356
  {
357
358
    state_ta_explicit * s = down_cast<state_ta_explicit*> (state);
    assert(s);
359
    s->set_initial_state(true);
360
361
362
363
364
365
366
367
    if (condition == bddfalse)
      condition = get_state_condition(s);
    std::pair<ta::states_set_t::iterator, bool> add_state =
        initial_states_set_.insert(s);
    if (get_artificial_initial_state() != 0)
      if (add_state.second)
        create_transition((state_ta_explicit*) get_artificial_initial_state(),
            condition, s);
368
369
370
371

  }

  void
372
373
  ta_explicit::delete_stuttering_and_hole_successors(spot::state* s)
  {
374
375
    state_ta_explicit * state = down_cast<state_ta_explicit*> (s);
    assert(state);
376
    state->delete_stuttering_and_hole_successors();
377
378
    if (state->is_initial_state())
      add_to_initial_states_set(state);
379
380
381
382
383
384

  }

  void
  ta_explicit::create_transition(state_ta_explicit* source, bdd condition,
      state_ta_explicit* dest)
385
386
387
388
389
390
391
392
  {
    state_ta_explicit::transition* t = new state_ta_explicit::transition;
    t->dest = dest;
    t->condition = condition;
    source->add_transition(t);

  }

393
  const ta::states_set_t
394
395
  ta_explicit::get_initial_states_set() const
  {
396
    return initial_states_set_;
397
398
399
400
401
402

  }

  bdd
  ta_explicit::get_state_condition(const spot::state* initial_state) const
  {
403
    const state_ta_explicit* sta =
404
        down_cast<const state_ta_explicit*> (initial_state);
405
    assert(sta);
406
407
408
409
410
411
    return sta->get_tgba_condition();
  }

  bool
  ta_explicit::is_accepting_state(const spot::state* s) const
  {
412
413
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
    assert(sta);
414
415
416
417
418
419
    return sta->is_accepting_state();
  }

  bool
  ta_explicit::is_initial_state(const spot::state* s) const
  {
420
421
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
    assert(sta);
422
423
424
425
426
427
    return sta->is_initial_state();
  }

  bool
  ta_explicit::is_livelock_accepting_state(const spot::state* s) const
  {
428
429
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
    assert(sta);
430
431
432
433
434
435
    return sta->is_livelock_accepting_state();
  }

  ta_succ_iterator*
  ta_explicit::succ_iter(const spot::state* state) const
  {
436
    const state_ta_explicit* s = down_cast<const state_ta_explicit*> (state);
437
438
439
440
    assert(s);
    return new ta_explicit_succ_iterator(s);
  }

441
442
443
  ta_succ_iterator*
  ta_explicit::succ_iter(const spot::state* state, bdd condition) const
  {
444
    const state_ta_explicit* s = down_cast<const state_ta_explicit*> (state);
445
446
447
448
    assert(s);
    return new ta_explicit_succ_iterator(s, condition);
  }

449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
  bdd_dict*
  ta_explicit::get_dict() const
  {
    return tgba_->get_dict();
  }

  const tgba*
  ta_explicit::get_tgba() const
  {
    return tgba_;
  }

  std::string
  ta_explicit::format_state(const spot::state* s) const
  {
464
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
465
    assert(sta);
466
467
468
469

    if (sta->get_tgba_condition() == bddtrue)
      return tgba_->format_state(sta->get_tgba_state());

470
    return tgba_->format_state(sta->get_tgba_state()) + "\n"
471
        + bdd_format_formula(get_dict(), sta->get_tgba_condition());
472
473
474
475
476
477
478
479
480
481

  }

  void
  ta_explicit::delete_stuttering_transitions()
  {
    ta::states_set_t::iterator it;
    for (it = states_set_.begin(); it != states_set_.end(); it++)
      {

482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
        const state_ta_explicit* source =
            static_cast<const state_ta_explicit*> (*it);

        state_ta_explicit::transitions* trans = source->get_transitions();
        state_ta_explicit::transitions::iterator it_trans;

        if (trans != 0)
          for (it_trans = trans->begin(); it_trans != trans->end();)
            {
              if (source->get_tgba_condition()
                  == ((*it_trans)->dest)->get_tgba_condition())
                {
                  delete *it_trans;
                  it_trans = trans->erase(it_trans);
                }
              else
                {
                  it_trans++;
                }
            }
502
503
504
505
      }

  }

506
507
508
509
510
  void
  ta_explicit::free_state(const spot::state*) const
  {
  }

511
}