taexplicit.cc 13.9 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
21
22
23
24
25
26
27
28
//#define TRACE

#include <iostream>
#ifdef TRACE
#define trace std::clog
#else
#define trace while (0) std::clog
#endif

29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
#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

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

51
  ta_explicit_succ_iterator::ta_explicit_succ_iterator(
52
      const state_ta_explicit* s, bdd condition)
53
54
55
56
  {
    transitions_ = s->get_transitions(condition);
  }

57
58
59
  void
  ta_explicit_succ_iterator::first()
  {
60
61
    if (transitions_ != 0)
      i_ = transitions_->begin();
62
63
64
65
66
67
68
69
70
71
72
  }

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

  bool
  ta_explicit_succ_iterator::done() const
  {
73
74
    return transitions_ == 0 || transitions_->empty() || i_
        == transitions_->end();
75
76
77
78
79
  }

  state*
  ta_explicit_succ_iterator::current_state() const
  {
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
80
81
82
    trace
      << "***ta_explicit_succ_iterator::current_state()  if(done()) =***"
          << done() << std::endl;
83
    assert(!done());
Ala-Eddine Ben-Salem's avatar
Ala-Eddine Ben-Salem committed
84
85
86
    trace
      << "***ta_explicit_succ_iterator::current_state() (*i_)->condition =***"
          << (*i_)->condition << std::endl;
87
88
89
90
91
92
93
94
95
96
97
    state_ta_explicit* s = (*i_)->dest;
    return s;
  }

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

98
99
100
101
102
103
104
  bdd
  ta_explicit_succ_iterator::current_acceptance_conditions() const
  {
    assert(!done());
    return (*i_)->acceptance_conditions;
  }

105
106
107
108
109
110
111
112
113
  ////////////////////////////////////////
  // state_ta_explicit

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

114
115
116
117
118
119
  // 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 =
120
        transitions_by_condition.find(condition.id());
121
122
123

    if (i == transitions_by_condition.end())
      {
124
        return 0;
125
126
127
      }
    else
      {
128
        return i->second;
129
130
131
      }

  }
132
133

  void
134
135
  state_ta_explicit::add_transition(state_ta_explicit::transition* t,
      bool add_at_beginning)
136
137
138
  {
    if (transitions_ == 0)
      transitions_ = new transitions;
139

140
    transitions* trans_by_condition = get_transitions(t->condition);
141

142
    if (trans_by_condition == 0)
143
      {
144
145
        trans_by_condition = new transitions;
        transitions_by_condition[(t->condition).id()] = trans_by_condition;
146
147
148
149
150
      }

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

151
    for (it_trans = trans_by_condition->begin(); (it_trans
152
        != trans_by_condition->end() && !transition_found); ++it_trans)
153
154
      {
        transition_found = ((*it_trans)->dest == t->dest);
155
156
157
158
        if (transition_found)
          {
            (*it_trans)->acceptance_conditions |= t->acceptance_conditions;
          }
159
      }
160

161
162
    if (!transition_found)
      {
163
164
        if (add_at_beginning)
          {
165
            trans_by_condition->push_front(t);
166
167
168
169
            transitions_->push_front(t);
          }
        else
          {
170
            trans_by_condition->push_back(t);
171
172
173
            transitions_->push_back(t);
          }

174
175
176
177
178
      }
    else
      {
        delete t;
      }
179
180

  }
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218

  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
219
220
  state_ta_explicit::set_livelock_accepting_state(
      bool is_livelock_accepting_state)
221
222
223
224
225
226
227
228
229
230
  {
    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;
  }

231
232
233
234
235
236
237
  bool
  state_ta_explicit::is_hole_state() const
  {
    state_ta_explicit::transitions* trans = get_transitions();
    return trans == 0 || trans->empty();
  }

238
239
240
  int
  state_ta_explicit::compare(const spot::state* other) const
  {
241
    const state_ta_explicit* o = down_cast<const state_ta_explicit*>(other);
242
243
244
245
246
247
248
    assert(o);

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

    if (compare_value != 0)
      return compare_value;

249
250
251
252
253
254
255
256
257
258
    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;
259
260
261
262
263
  }

  size_t
  state_ta_explicit::hash() const
  {
264
265
266
    //return wang32_hash(tgba_state_->hash());
    return wang32_hash(tgba_state_->hash()) ^ wang32_hash(tgba_condition_.id());

267
268
269
270
271
272
273
274
275
  }

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

  void
276
277
278
279
280
281
282
  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();)
283
284
285
286
        {
          state_ta_explicit* dest = (*it_trans)->dest;
          bool is_stuttering_transition = (get_tgba_condition()
              == (dest)->get_tgba_condition());
287
288
          bool dest_is_livelock_accepting =
	    dest->is_livelock_accepting_state();
289

290
291
          //Before deleting stuttering transitions, propaged back livelock
          //and initial state's properties
292
293
          if (is_stuttering_transition)
            {
294
295
296
297
298
299
              if (!is_livelock_accepting_state() && dest_is_livelock_accepting)
                {
                  set_livelock_accepting_state(true);
                  stuttering_reachable_livelock
                      = dest->stuttering_reachable_livelock;
                }
300
301
302
303
304
305
306
307
308
309
310
311
              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);
312
              delete *it_trans;
313
314
315
316
              it_trans = trans->erase(it_trans);
            }
          else
            {
317
              ++it_trans;
318
319
            }
        }
320
321
322

  }

323
324
325
  void
  state_ta_explicit::free_transitions()
  {
326
    state_ta_explicit::transitions* trans = transitions_;
327
328
329
330
    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)
331
      for (it_trans = trans->begin(); it_trans != trans->end(); ++it_trans)
332
333
334
        {
          delete *it_trans;
        }
335
336
337
    delete trans;

    Sgi::hash_map<int, transitions*, Sgi::hash<int> >::iterator i =
338
        transitions_by_condition.begin();
339
340
    while (i != transitions_by_condition.end())
      {
341
342
        delete i->second;
        ++i;
343
      }
344

345
    transitions_ = 0;
346
347
348
349
350
351
  }

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


352
  ta_explicit::ta_explicit(const tgba* tgba, bdd all_acceptance_conditions,
353
354
355
356
357
358
			   state_ta_explicit* artificial_initial_state,
			   bool own_tgba) :
    tgba_(tgba),
    all_acceptance_conditions_(all_acceptance_conditions),
    artificial_initial_state_(artificial_initial_state),
    own_tgba_(own_tgba)
359
  {
360
    get_dict()->register_all_variables_of(&tgba_, this);
361
362
363
364
365
    if (artificial_initial_state != 0)
      {
        state_ta_explicit* is = add_state(artificial_initial_state);
        assert(is == artificial_initial_state);
      }
366
367
368
369
370
  }

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

375
376
377
        s->free_transitions();
        s->get_tgba_state()->destroy();
        delete s;
378
      }
379
    get_dict()->unregister_all_my_variables(this);
380
381
    if (own_tgba_)
      delete tgba_;
382
383
384
385
386
387
  }

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

390
    return static_cast<state_ta_explicit*>(*add_state_to_ta.first);
391
392
  }

393
  void
394
  ta_explicit::add_to_initial_states_set(state* state, bdd condition)
395
  {
396
    state_ta_explicit* s = down_cast<state_ta_explicit*>(state);
397
    s->set_initial_state(true);
398
399
400
401
402
403
    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)
404
405
406
407
408
	{
	  state_ta_explicit* i =
	    down_cast<state_ta_explicit*>(get_artificial_initial_state());
	  create_transition(i, condition, bddfalse, s);
	}
409
410
411
  }

  void
412
413
  ta_explicit::delete_stuttering_and_hole_successors(spot::state* s)
  {
414
    state_ta_explicit * state = down_cast<state_ta_explicit*>(s);
415
    assert(state);
416
    state->delete_stuttering_and_hole_successors();
417
418
    if (state->is_initial_state())
      add_to_initial_states_set(state);
419
420
421

  }

422
423
  void
  ta_explicit::create_transition(state_ta_explicit* source, bdd condition,
424
425
				 bdd acceptance_conditions,
				 state_ta_explicit* dest, bool add_at_beginning)
426
427
428
429
430
  {
    state_ta_explicit::transition* t = new state_ta_explicit::transition;
    t->dest = dest;
    t->condition = condition;
    t->acceptance_conditions = acceptance_conditions;
431
    source->add_transition(t, add_at_beginning);
432
433
434

  }

435
  const ta::states_set_t
436
437
  ta_explicit::get_initial_states_set() const
  {
438
    return initial_states_set_;
439
440
441
442
443
444

  }

  bdd
  ta_explicit::get_state_condition(const spot::state* initial_state) const
  {
445
    const state_ta_explicit* sta =
446
        down_cast<const state_ta_explicit*>(initial_state);
447
    assert(sta);
448
449
450
451
452
453
    return sta->get_tgba_condition();
  }

  bool
  ta_explicit::is_accepting_state(const spot::state* s) const
  {
454
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
455
    assert(sta);
456
457
458
459
460
461
    return sta->is_accepting_state();
  }

  bool
  ta_explicit::is_initial_state(const spot::state* s) const
  {
462
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
463
    assert(sta);
464
465
466
467
468
469
    return sta->is_initial_state();
  }

  bool
  ta_explicit::is_livelock_accepting_state(const spot::state* s) const
  {
470
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
471
    assert(sta);
472
473
474
475
476
477
    return sta->is_livelock_accepting_state();
  }

  ta_succ_iterator*
  ta_explicit::succ_iter(const spot::state* state) const
  {
478
    const state_ta_explicit* s = down_cast<const state_ta_explicit*>(state);
479
480
481
482
    assert(s);
    return new ta_explicit_succ_iterator(s);
  }

483
484
485
  ta_succ_iterator*
  ta_explicit::succ_iter(const spot::state* state, bdd condition) const
  {
486
    const state_ta_explicit* s = down_cast<const state_ta_explicit*>(state);
487
488
489
490
    assert(s);
    return new ta_explicit_succ_iterator(s, condition);
  }

491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
  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
  {
506
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
507
    assert(sta);
508
509
510
511

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

512
    return tgba_->format_state(sta->get_tgba_state()) + "\n"
513
        + bdd_format_formula(get_dict(), sta->get_tgba_condition());
514
515
516
517
518
519
520

  }

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

524
        const state_ta_explicit* source =
525
            static_cast<const state_ta_explicit*>(*it);
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540

        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
                {
541
                  ++it_trans;
542
543
                }
            }
544
545
546
547
      }

  }

548
549
550
551
552
  void
  ta_explicit::free_state(const spot::state*) const
  {
  }

553
}