taexplicit.cc 13.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
// 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.

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

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

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

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

53
54
55
56
57
58
59
  ta_explicit_succ_iterator::ta_explicit_succ_iterator(
      const state_ta_explicit* s, bdd condition) :
    source_(s)
  {
    transitions_ = s->get_transitions(condition);
  }

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

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

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

  state*
  ta_explicit_succ_iterator::current_state() const
  {
83
    trace << "***ta_explicit_succ_iterator::current_state()  if(done()) =***" << done() << std::endl;
84
    assert(!done());
85
    trace << "***ta_explicit_succ_iterator::current_state() (*i_)->condition =***" << (*i_)->condition << std::endl;
86
87
88
89
90
91
92
93
94
95
96
    state_ta_explicit* s = (*i_)->dest;
    return s;
  }

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

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

104
105
106
107
108
  bool
  ta_explicit_succ_iterator::is_stuttering_transition() const
  {
    return source_->get_tgba_condition() == ((*i_)->dest)->get_tgba_condition();
  }
109
110
111
112
113
114
115
116
117
118

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

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

119
120
121
122
123
124
  // 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 =
125
        transitions_by_condition.find(condition.id());
126
127
128

    if (i == transitions_by_condition.end())
      {
129
        return 0;
130
131
132
      }
    else
      {
133
        return i->second;
134
135
136
      }

  }
137
138

  void
139
140
  state_ta_explicit::add_transition(state_ta_explicit::transition* t,
      bool add_at_beginning)
141
142
143
  {
    if (transitions_ == 0)
      transitions_ = new transitions;
144

145
146
147
148
    transitions* transitions_condition = get_transitions(t->condition);

    if (transitions_condition == 0)
      {
149
150
151
152
153
154
155
156
157
158
159
        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);
160
161
162
163
        if (transition_found)
          {
            (*it_trans)->acceptance_conditions |= t->acceptance_conditions;
          }
164
      }
165

166
167
    if (!transition_found)
      {
168
169
170
171
172
173
174
175
176
177
178
        if (add_at_beginning)
          {
            transitions_condition->push_front(t);
            transitions_->push_front(t);
          }
        else
          {
            transitions_condition->push_back(t);
            transitions_->push_back(t);
          }

179
180
181
182
183
      }
    else
      {
        delete t;
      }
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
219
220
221
222
223

  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
224
225
  state_ta_explicit::set_livelock_accepting_state(
      bool is_livelock_accepting_state)
226
227
228
229
230
231
232
233
234
235
  {
    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;
  }

236
237
238
239
240
241
242
  bool
  state_ta_explicit::is_hole_state() const
  {
    state_ta_explicit::transitions* trans = get_transitions();
    return trans == 0 || trans->empty();
  }

243
244
245
  int
  state_ta_explicit::compare(const spot::state* other) const
  {
246
    const state_ta_explicit* o = down_cast<const state_ta_explicit*> (other);
247
248
249
250
251
252
253
    assert(o);

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

    if (compare_value != 0)
      return compare_value;

254
255
256
257
258
259
260
261
262
263
    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;
264
265
266
267
268
  }

  size_t
  state_ta_explicit::hash() const
  {
269
    return wang32_hash(tgba_state_->hash());
270
271
272
273
274
275
276
277
278
  }

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

  void
279
280
281
282
283
284
285
  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();)
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
314
315
316
        {
          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++;
            }
        }
317
318
319

  }

320
321
322
323
324
325
326
327
328
  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++)
329
330
331
        {
          delete *it_trans;
        }
332
333
334
    delete trans;

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

  }

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


348
  ta_explicit::ta_explicit(const tgba* tgba, bdd all_acceptance_conditions,
349
      state_ta_explicit* artificial_initial_state) :
350
351
    tgba_(tgba), all_acceptance_conditions_(all_acceptance_conditions),
        artificial_initial_state_(artificial_initial_state)
352
  {
353
    get_dict()->register_all_variables_of(&tgba_, this);
354
355
356
357
358
359
    if (artificial_initial_state != 0)
      {
        state_ta_explicit* is = add_state(artificial_initial_state);
        assert(is == artificial_initial_state);
      }

360
361
362
363
364
365
366
  }

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

369
370
371
        s->free_transitions();
        s->get_tgba_state()->destroy();
        delete s;
372
      }
373
374
    get_dict()->unregister_all_my_variables(this);
    delete tgba_;
375
376
377
378
379
380
  }

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

383
    return static_cast<state_ta_explicit*> (*add_state_to_ta.first);
384
385
386

  }

387
  void
388
  ta_explicit::add_to_initial_states_set(state* state, bdd condition)
389
  {
390
391
    state_ta_explicit * s = down_cast<state_ta_explicit*> (state);
    assert(s);
392
    s->set_initial_state(true);
393
394
395
396
397
398
399
    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(),
400
            condition, bddfalse, s);
401
402
403
404

  }

  void
405
406
  ta_explicit::delete_stuttering_and_hole_successors(spot::state* s)
  {
407
408
    state_ta_explicit * state = down_cast<state_ta_explicit*> (s);
    assert(state);
409
    state->delete_stuttering_and_hole_successors();
410
411
    if (state->is_initial_state())
      add_to_initial_states_set(state);
412
413
414

  }

415
416
417

  void
  ta_explicit::create_transition(state_ta_explicit* source, bdd condition,
418
      bdd acceptance_conditions, state_ta_explicit* dest, bool add_at_beginning)
419
420
421
422
423
  {
    state_ta_explicit::transition* t = new state_ta_explicit::transition;
    t->dest = dest;
    t->condition = condition;
    t->acceptance_conditions = acceptance_conditions;
424
    source->add_transition(t, add_at_beginning);
425
426
427

  }

428
  const ta::states_set_t
429
430
  ta_explicit::get_initial_states_set() const
  {
431
    return initial_states_set_;
432
433
434
435
436
437

  }

  bdd
  ta_explicit::get_state_condition(const spot::state* initial_state) const
  {
438
    const state_ta_explicit* sta =
439
        down_cast<const state_ta_explicit*> (initial_state);
440
    assert(sta);
441
442
443
444
445
446
    return sta->get_tgba_condition();
  }

  bool
  ta_explicit::is_accepting_state(const spot::state* s) const
  {
447
448
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
    assert(sta);
449
450
451
452
453
454
    return sta->is_accepting_state();
  }

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

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

  ta_succ_iterator*
  ta_explicit::succ_iter(const spot::state* state) const
  {
471
    const state_ta_explicit* s = down_cast<const state_ta_explicit*> (state);
472
473
474
475
    assert(s);
    return new ta_explicit_succ_iterator(s);
  }

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

484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
  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
  {
499
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*> (s);
500
    assert(sta);
501
502
503
504

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

505
    return tgba_->format_state(sta->get_tgba_state()) + "\n"
506
        + bdd_format_formula(get_dict(), sta->get_tgba_condition());
507
508
509
510
511
512
513
514
515
516

  }

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

517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
        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++;
                }
            }
537
538
539
540
      }

  }

541
542
543
544
545
  void
  ta_explicit::free_state(const spot::state*) const
  {
  }

546
}