taexplicit.cc 13.9 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et 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
#include "ltlast/atomic_prop.hh"
#include "ltlast/constant.hh"
#include "taexplicit.hh"
#include "tgba/formula2bdd.hh"
#include <cassert>
#include "ltlvisit/tostring.hh"

#include "tgba/bddprint.hh"

namespace spot
{

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

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

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

56
  bool
57 58
  ta_explicit_succ_iterator::first()
  {
59 60 61 62
    if (!transitions_)
      return false;
    i_ = transitions_->begin();
    return i_ != transitions_->end();
63 64
  }

65
  bool
66 67 68
  ta_explicit_succ_iterator::next()
  {
    ++i_;
69
    return i_ != transitions_->end();
70 71 72 73 74
  }

  bool
  ta_explicit_succ_iterator::done() const
  {
75
    return !transitions_ || i_ == transitions_->end();
76 77 78 79 80
  }

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

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

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

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

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

115 116 117 118 119
  // return transitions filtred by condition
  state_ta_explicit::transitions*
  state_ta_explicit::get_transitions(bdd condition) const
  {

120
    std::unordered_map<int, transitions*, std::hash<int> >::const_iterator i =
121
        transitions_by_condition.find(condition.id());
122 123 124

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

  }
133 134

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

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

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

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

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

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

175 176 177 178 179
      }
    else
      {
        delete t;
      }
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 219

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

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

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

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

    if (compare_value != 0)
      return compare_value;

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

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

268 269 270 271 272 273 274 275 276
  }

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

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

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

  }

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

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

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

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


353
  ta_explicit::ta_explicit(const const_twa_ptr& tgba,
354
			   unsigned n_acc,
355
			   state_ta_explicit* artificial_initial_state):
356
    ta(tgba->get_dict()),
357
    tgba_(tgba),
358
    artificial_initial_state_(artificial_initial_state)
359
  {
360
    get_dict()->register_all_variables_of(&tgba_, this);
361
    acc().add_sets(n_acc);
362
    acc().set_generalized_buchi();
363 364 365 366
    if (artificial_initial_state != 0)
      {
        state_ta_explicit* is = add_state(artificial_initial_state);
        assert(is == artificial_initial_state);
367
	(void)is;
368
      }
369 370 371 372 373
  }

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

378 379 380
        s->free_transitions();
        s->get_tgba_state()->destroy();
        delete s;
381
      }
382
    get_dict()->unregister_all_my_variables(this);
383 384 385 386 387 388
  }

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

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

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

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

  }

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

  }

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

  }

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

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

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

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

  ta_succ_iterator*
  ta_explicit::succ_iter(const spot::state* state) 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);
  }

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

492
  bdd_dict_ptr
493 494 495 496 497
  ta_explicit::get_dict() const
  {
    return tgba_->get_dict();
  }

498
  const_twa_ptr
499 500 501 502 503 504 505 506
  ta_explicit::get_tgba() const
  {
    return tgba_;
  }

  std::string
  ta_explicit::format_state(const spot::state* s) const
  {
507
    const state_ta_explicit* sta = down_cast<const state_ta_explicit*>(s);
508
    assert(sta);
509 510 511 512

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

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

  }

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

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

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

  }

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

554
}