tgbaexplicit.hh 20.5 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche
// et Développement de l'Epita.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
4 5 6
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7 8 9 10 11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13 14 15 16 17 18 19 20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23 24 25
#ifndef SPOT_TGBA_TGBAEXPLICIT_HH
# define SPOT_TGBA_TGBAEXPLICIT_HH

Pierre PARUTTO's avatar
Pierre PARUTTO committed
26
#include <sstream>
27
#include <list>
Pierre PARUTTO's avatar
Pierre PARUTTO committed
28

29
#include "tgba.hh"
30
#include "sba.hh"
Pierre PARUTTO's avatar
Pierre PARUTTO committed
31 32 33
#include "tgba/formula2bdd.hh"
#include "misc/hash.hh"
#include "misc/bddop.hh"
34
#include "ltlast/formula.hh"
Pierre PARUTTO's avatar
Pierre PARUTTO committed
35
#include "ltlvisit/tostring.hh"
36 37 38

namespace spot
{
39
  // How to destroy the label of a state.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56
  template<typename T>
  struct destroy_key
  {
    void destroy(T t)
    {
      (void) t;
    }
  };

  template<>
  struct destroy_key<const ltl::formula*>
  {
    void destroy(const ltl::formula* t)
    {
      t->destroy();
    }
  };
57

Pierre PARUTTO's avatar
Pierre PARUTTO committed
58
  /// States used by spot::explicit_graph implementation
59
  /// \ingroup tgba_representation
Pierre PARUTTO's avatar
Pierre PARUTTO committed
60
  template<typename Label, typename label_hash>
61
  class state_explicit: public spot::state
62 63
  {
  public:
64 65 66 67
    state_explicit()
    {
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
68 69
    state_explicit(const Label& l):
      label_(l)
70 71 72
    {
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
73
    virtual ~state_explicit()
74 75
    {
    }
76

77
    virtual void destroy() const
78 79
    {
    }
80

81
    typedef Label label_t;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
82 83
    typedef label_hash label_hash_t;

84 85 86
    struct transition
    {
      bdd condition;
87
      bdd acceptance_conditions;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
88
      const state_explicit<Label, label_hash>* dest;
89 90
    };

91 92 93
    typedef std::list<transition> transitions_t;
    transitions_t successors;

Pierre PARUTTO's avatar
Pierre PARUTTO committed
94
    const Label& label() const
95
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
96
      return label_;
97 98
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
99 100 101 102
    bool empty() const
    {
      return successors.empty();
    }
103

Pierre PARUTTO's avatar
Pierre PARUTTO committed
104 105 106 107 108 109 110 111 112 113 114 115 116
    virtual int compare(const state* other) const
    {
      const state_explicit<Label, label_hash>* s =
	down_cast<const state_explicit<Label, label_hash>*>(other);
      assert (s);

      // Do not simply return "o - this", it might not fit in an int.
      if (s < this)
	return -1;
      if (s > this)
	return 1;
      return 0;
    }
117

Pierre PARUTTO's avatar
Pierre PARUTTO committed
118 119 120 121 122
    virtual size_t hash() const
    {
      return
	reinterpret_cast<const char*>(this) - static_cast<const char*>(0);
    }
123

Pierre PARUTTO's avatar
Pierre PARUTTO committed
124 125 126 127 128
    virtual state_explicit<Label, label_hash>*
    clone() const
    {
      return const_cast<state_explicit<Label, label_hash>*>(this);
    }
129

Pierre PARUTTO's avatar
Pierre PARUTTO committed
130 131 132
  protected:
    Label label_;
  };
133

134
  /// States labeled by an int
Pierre PARUTTO's avatar
Pierre PARUTTO committed
135 136 137 138 139 140 141 142 143
  /// \ingroup tgba_representation
  class state_explicit_number:
    public state_explicit<int, identity_hash<int> >
  {
  public:
    state_explicit_number()
      : state_explicit<int, identity_hash<int> >()
    {
    }
144

Pierre PARUTTO's avatar
Pierre PARUTTO committed
145 146 147 148
    state_explicit_number(int label)
      : state_explicit<int, identity_hash<int> >(label)
    {
    }
149

Pierre PARUTTO's avatar
Pierre PARUTTO committed
150 151
    static const int default_val;
  };
152

Pierre PARUTTO's avatar
Pierre PARUTTO committed
153 154 155 156 157 158 159 160 161 162
  /// States labeled by a string
  /// \ingroup tgba_representation
  class state_explicit_string:
    public state_explicit<std::string, string_hash>
  {
  public:
    state_explicit_string():
      state_explicit<std::string, string_hash>()
    {
    }
163

Pierre PARUTTO's avatar
Pierre PARUTTO committed
164 165 166 167
    state_explicit_string(const std::string& label)
      : state_explicit<std::string, string_hash>(label)
    {
    }
168

Pierre PARUTTO's avatar
Pierre PARUTTO committed
169 170
    static const std::string default_val;
  };
171

Pierre PARUTTO's avatar
Pierre PARUTTO committed
172 173 174 175 176 177 178 179 180 181
  /// States labeled by a formula
  /// \ingroup tgba_representation
  class state_explicit_formula:
    public state_explicit<const ltl::formula*, ltl::formula_ptr_hash>
  {
  public:
    state_explicit_formula():
      state_explicit<const ltl::formula*, ltl::formula_ptr_hash>()
    {
    }
182

Pierre PARUTTO's avatar
Pierre PARUTTO committed
183 184 185 186
    state_explicit_formula(const ltl::formula* label)
      : state_explicit<const ltl::formula*, ltl::formula_ptr_hash>(label)
    {
    }
187

Pierre PARUTTO's avatar
Pierre PARUTTO committed
188 189
    static const ltl::formula* default_val;
  };
190

191
  /// Successor iterators used by spot::tgba_explicit.
192
  /// \ingroup tgba_representation
Pierre PARUTTO's avatar
Pierre PARUTTO committed
193
  template<typename State>
194
  class tgba_explicit_succ_iterator: public tgba_succ_iterator
195 196
  {
  public:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212
    tgba_explicit_succ_iterator(const State* start,
				bdd all_acc)
      : start_(start),
	all_acceptance_conditions_(all_acc)
    {
    }

    virtual void first()
    {
      it_ = start_->successors.begin();
    }

    virtual void next()
    {
      ++it_;
    }
213

Pierre PARUTTO's avatar
Pierre PARUTTO committed
214 215 216 217
    virtual bool done() const
    {
      return it_ == start_->successors.end();
    }
218

Pierre PARUTTO's avatar
Pierre PARUTTO committed
219 220 221 222 223
    virtual State* current_state() const
    {
      assert(!done());
      const State* res = down_cast<const State*>(it_->dest);
      assert(res);
224
      return const_cast<State*>(res);
Pierre PARUTTO's avatar
Pierre PARUTTO committed
225 226 227 228 229 230 231 232 233 234 235
    }

    virtual bdd current_condition() const
    {
      assert(!done());
      return it_->condition;
    }

    virtual bdd current_acceptance_conditions() const
    {
      assert(!done());
236
      return it_->acceptance_conditions;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
237
    }
238

239 240 241 242 243 244
    typename State::transitions_t::const_iterator
    get_iterator() const
    {
      return it_;
    }

245
  private:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
246 247
    const State* start_;
    typename State::transitions_t::const_iterator it_;
248
    bdd all_acceptance_conditions_;
249 250
  };

251
  /// Graph implementation for explicit automaton
Pierre PARUTTO's avatar
Pierre PARUTTO committed
252 253 254
  /// \ingroup tgba_representation
  template<typename State, typename Type>
  class explicit_graph: public Type
255
  {
256 257 258 259 260 261
  public:
    typedef typename State::label_t label_t;
    typedef typename State::label_hash_t label_hash_t;
    typedef typename State::transitions_t transitions_t;
    typedef typename State::transition transition;
    typedef State state;
262
  protected:
263
    typedef Sgi::hash_map<label_t, State, label_hash_t> ls_map;
264
    typedef Sgi::hash_map<label_t, State*, label_hash_t> alias_map;
265
    typedef Sgi::hash_map<const State*, label_t, ptr_hash<State> > sl_map;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
266

267
  public:
268

Pierre PARUTTO's avatar
Pierre PARUTTO committed
269 270 271 272
    explicit_graph(bdd_dict* dict)
      : ls_(),
	sl_(),
	init_(0),
273 274 275 276
	dict_(dict),
	all_acceptance_conditions_(bddfalse),
	all_acceptance_conditions_computed_(false),
	neg_acceptance_conditions_(bddtrue)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
277 278
    {
    }
279

Pierre PARUTTO's avatar
Pierre PARUTTO committed
280 281 282 283 284
    State* add_default_init()
    {
      return add_state(State::default_val);
    }

285 286 287 288 289
    size_t num_states() const
    {
      return sl_.size();
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
290 291 292 293 294 295 296 297 298
    transition*
    create_transition(State* source, const State* dest)
    {
      transition t;

      t.dest = dest;
      t.condition = bddtrue;
      t.acceptance_conditions = bddfalse;

299
      typename transitions_t::iterator i =
Pierre PARUTTO's avatar
Pierre PARUTTO committed
300 301 302 303 304 305
	source->successors.insert(source->successors.end(), t);

      return &*i;
    }

    transition*
306
    create_transition(const label_t& source, const label_t& dest)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
307 308 309 310 311 312 313 314 315 316 317
    {
      // It's important that the source be created before the
      // destination, so the first source encountered becomes the
      // default initial state.
      State* s = add_state(source);
      return create_transition(s, add_state(dest));
    }

    transition*
    get_transition(const tgba_explicit_succ_iterator<State>* si)
    {
318
      return const_cast<transition*>(&(*(si->get_iterator())));
Pierre PARUTTO's avatar
Pierre PARUTTO committed
319 320
    }

321 322 323 324 325 326 327 328 329
    transition*
    get_transition(const tgba_succ_iterator* si)
    {
      const tgba_explicit_succ_iterator<State>* tmp
	= down_cast<const tgba_explicit_succ_iterator<State>*>(si);
      assert(tmp);
      return get_transition(tmp);
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
330 331 332 333 334 335 336 337
    void add_condition(transition* t, const ltl::formula* f)
    {
      t->condition &= formula_to_bdd(f, dict_, this);
      f->destroy();
    }

    /// This assumes that all variables in \a f are known from dict.
    void add_conditions(transition* t, bdd f)
338
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
339 340
      dict_->register_propositions(f, this);
      t->condition &= f;
341 342
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
343
    bool has_acceptance_condition(const ltl::formula* f) const
344
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
345 346 347
      return dict_->is_registered_acceptance_variable(f, this);
    }

348
    //old tgba explicit labeled interface
349
    bool has_state(const label_t& name)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
350 351 352 353
    {
      return ls_.find(name) != ls_.end();
    }

354 355 356 357 358 359 360 361 362 363 364 365
    /// \brief Return the state associated to a given label.
    ///
    /// This is similar to add_state(), except that it returns 0 if
    /// the state does not exist.
    const State* get_state(const label_t& name)
    {
      typename ls_map::const_iterator i = ls_.find(name);
      if (i == ls_.end())
	return 0;
      return &i->second;
    }

366
    const label_t& get_label(const State* s) const
Pierre PARUTTO's avatar
Pierre PARUTTO committed
367 368 369
    {
      typename sl_map::const_iterator i = sl_.find(s);
      assert(i != sl_.end());
370 371 372
      return i->second;
    }

373
    const label_t& get_label(const spot::state* s) const
374
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
375
      const State* se = down_cast<const State*>(s);
376
      assert(se);
377
      return get_label(se);
378 379
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
380 381 382 383 384 385 386
    void
    complement_all_acceptance_conditions()
    {
      bdd all = this->all_acceptance_conditions();
      typename ls_map::iterator i;
      for (i = ls_.begin(); i != ls_.end(); ++i)
	{
387
	  typename transitions_t::iterator i2;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
388 389 390 391 392 393 394 395 396
	  for (i2 = i->second.successors.begin();
	       i2 != i->second.successors.end(); ++i2)
	    i2->acceptance_conditions = all - i2->acceptance_conditions;
	}
    }

    void
    merge_transitions()
    {
397 398
      typedef typename transitions_t::iterator trans_t;
      typedef std::map<int, trans_t> acc_map;
399 400
      typedef Sgi::hash_map<const spot::state*, acc_map,
			    ptr_hash<spot::state> > dest_map;
401

Pierre PARUTTO's avatar
Pierre PARUTTO committed
402 403 404
      typename ls_map::iterator i;
      for (i = ls_.begin(); i != ls_.end(); ++i)
	{
405 406 407 408 409 410 411 412 413
	  const spot::state* last_dest = 0;
	  dest_map dm;
	  typename dest_map::iterator dmi = dm.end();
	  typename transitions_t::iterator t1 = i->second.successors.begin();

	  // Loop over all outgoing transitions (cond,acc,dest), and
	  // store them into dest_map[dest][acc] so that we can merge
	  // conditions.
	  while (t1 != i->second.successors.end())
Pierre PARUTTO's avatar
Pierre PARUTTO committed
414
	    {
415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434
	      const spot::state* dest = t1->dest;
	      if (dest != last_dest)
		{
		  last_dest = dest;
		  dmi = dm.find(dest);
		  if (dmi == dm.end())
		    dmi = dm.insert(std::make_pair(dest, acc_map())).first;
		}
	      int acc = t1->acceptance_conditions.id();
	      typename acc_map::iterator it = dmi->second.find(acc);
	      if (it == dmi->second.end())
		{
		  dmi->second[acc] = t1;
		  ++t1;
		}
	      else
		{
		  it->second->condition |= t1->condition;
		  t1 = i->second.successors.erase(t1);
		}
Pierre PARUTTO's avatar
Pierre PARUTTO committed
435 436 437 438
	    }
	}
    }

439
    /// Return the state_explicit for \a name, creating the state if
440
    /// it does not exist.
441
    State* add_state(const label_t& name)
442
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
443 444
      typename ls_map::iterator i = ls_.find(name);
      if (i == ls_.end())
445
	{
446 447 448
	  typename alias_map::iterator j = alias_.find(name);
	  if (j != alias_.end())
	    return j->second;
449

450 451 452 453
	  State* res =
	    &(ls_.insert(std::make_pair(name, State(name))).first->second);
	  sl_[res] = name;
	  // The first state we add is the initial state.
454 455
	  // It can also be overridden with set_init_state().
	  if (!init_)
456 457
	    init_ = res;
	  return res;
458
	}
Pierre PARUTTO's avatar
Pierre PARUTTO committed
459
      return &(i->second);
460
    }
461

Pierre PARUTTO's avatar
Pierre PARUTTO committed
462
    State*
463
    set_init_state(const label_t& state)
464
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
465
      State* s = add_state(state);
466 467 468 469
      init_ = s;
      return s;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
470 471 472 473
    // tgba interface
    virtual ~explicit_graph()
    {
      typename ls_map::iterator i = ls_.begin();
474

Pierre PARUTTO's avatar
Pierre PARUTTO committed
475 476
      while (i != ls_.end())
      {
477
	label_t s = i->first;
478
	i->second.destroy();
Pierre PARUTTO's avatar
Pierre PARUTTO committed
479
	++i;
480
	destroy_key<label_t> dest;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
481 482
	dest.destroy(s);
      }
483 484 485 486 487 488

      this->dict_->unregister_all_my_variables(this);
      // These have already been destroyed by subclasses.
      // Prevent destroying by tgba::~tgba.
      this->last_support_conditions_input_ = 0;
      this->last_support_variables_input_ = 0;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
489 490 491
    }

    virtual State* get_init_state() const
492
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
493 494 495 496
      if (!init_)
	const_cast<explicit_graph<State, Type>*>(this)->add_default_init();

      return init_;
497 498
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
499 500 501 502
    virtual tgba_explicit_succ_iterator<State>*
    succ_iter(const spot::state* state,
	      const spot::state* global_state = 0,
	      const tgba* global_automaton = 0) const
503
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
504 505 506 507 508 509 510 511 512 513
      const State* s = down_cast<const State*>(state);
      assert(s);

      (void) global_state;
      (void) global_automaton;

      return
	new tgba_explicit_succ_iterator<State>(s,
					       this
					       ->all_acceptance_conditions());
514 515
    }

516 517 518 519 520 521 522 523 524 525 526 527 528

    typedef std::string (*to_string_func_t)(const label_t& t);

    void set_to_string_func(to_string_func_t f)
    {
      to_string_func_ = f;
    }

    to_string_func_t get_to_string_func() const
    {
      return to_string_func_;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
529 530 531 532 533 534
    virtual std::string format_state(const spot::state* state) const
    {
      const State* se = down_cast<const State*>(state);
      assert(se);
      typename sl_map::const_iterator i = sl_.find(se);
      assert(i != sl_.end());
535 536
      assert(to_string_func_);
      return to_string_func_(i->second);
Pierre PARUTTO's avatar
Pierre PARUTTO committed
537 538 539 540
    }

    /// Create an alias for a state.  Any reference to \a alias_name
    /// will act as a reference to \a real_name.
541
    void add_state_alias(const label_t& alias, const label_t& real)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
542
    {
543
      alias_[alias] = add_state(real);
Pierre PARUTTO's avatar
Pierre PARUTTO committed
544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559
    }


    /// \brief Copy the acceptance conditions of a tgba.
    ///
    /// If used, this function should be called before creating any
    /// transition.
    void copy_acceptance_conditions_of(const tgba *a)
    {
      assert(neg_acceptance_conditions_ == bddtrue);
      assert(all_acceptance_conditions_computed_ == false);
      bdd f = a->neg_acceptance_conditions();
      this->dict_->register_acceptance_variables(f, this);
      neg_acceptance_conditions_ = f;
    }

560

561
    /// Acceptance conditions handling
Pierre PARUTTO's avatar
Pierre PARUTTO committed
562 563 564 565 566 567 568 569 570 571 572 573
    void set_acceptance_conditions(bdd acc)
    {
      assert(neg_acceptance_conditions_ == bddtrue);
      assert(all_acceptance_conditions_computed_ == false);

      this->dict_->register_acceptance_variables(bdd_support(acc), this);
      neg_acceptance_conditions_ = compute_neg_acceptance_conditions(acc);
      all_acceptance_conditions_computed_ = true;
      all_acceptance_conditions_ = acc;
    }

    void add_acceptance_condition(transition* t, const ltl::formula* f)
574
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
575 576 577 578 579 580 581 582 583 584 585
      bdd c = get_acceptance_condition(f);
      t->acceptance_conditions |= c;
    }

    /// This assumes that all acceptance conditions in \a f are known from
    /// dict.
    void add_acceptance_conditions(transition* t, bdd f)
    {
      bdd sup = bdd_support(f);
      this->dict_->register_acceptance_variables(sup, this);
      while (sup != bddtrue)
586
	{
Pierre PARUTTO's avatar
Pierre PARUTTO committed
587 588
	  neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup));
	  sup = bdd_high(sup);
589
	}
Pierre PARUTTO's avatar
Pierre PARUTTO committed
590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611
      t->acceptance_conditions |= f;
    }

    virtual bdd all_acceptance_conditions() const
    {
      if (!all_acceptance_conditions_computed_)
      {
	all_acceptance_conditions_ =
	  compute_all_acceptance_conditions(neg_acceptance_conditions_);
	all_acceptance_conditions_computed_ = true;
      }
      return all_acceptance_conditions_;
    }

    virtual bdd_dict* get_dict() const
    {
      return this->dict_;
    }

    virtual bdd neg_acceptance_conditions() const
    {
      return neg_acceptance_conditions_;
612 613 614 615 616
    }

    void
    declare_acceptance_condition(const ltl::formula* f)
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
617
      int v = this->dict_->register_acceptance_variable(f, this);
618 619 620 621 622
      f->destroy();
      bdd neg = bdd_nithvar(v);
      neg_acceptance_conditions_ &= neg;

      // Append neg to all acceptance conditions.
623 624 625 626 627 628

      // FIXME: Declaring acceptance conditions after the automaton
      // has been constructed is very slow because we traverse the
      // entire automaton for each new acceptance condition.  It would
      // be better to fix the automaton in a single pass after all
      // acceptance conditions have been declared.
629
      typename ls_map::iterator i;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
630
      for (i = this->ls_.begin(); i != this->ls_.end(); ++i)
631
	{
632
	  typename transitions_t::iterator i2;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
633 634
	  for (i2 = i->second.successors.begin();
	       i2 != i->second.successors.end(); ++i2)
635
	    i2->acceptance_conditions &= neg;
636 637 638 639 640
	}

      all_acceptance_conditions_computed_ = false;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
641
    bdd get_acceptance_condition(const ltl::formula* f)
642
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
643 644 645 646 647 648
      bdd_dict::fv_map::iterator i = this->dict_->acc_map.find(f);
      assert(this->has_acceptance_condition(f));
      f->destroy();
      bdd v = bdd_ithvar(i->second);
      v &= bdd_exist(neg_acceptance_conditions_, v);
      return v;
649 650
    }

651 652
  protected:

Pierre PARUTTO's avatar
Pierre PARUTTO committed
653
    virtual bdd compute_support_conditions(const spot::state* in) const
654
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
655 656
      const State* s = down_cast<const State*>(in);
      assert(s);
657
      const transitions_t& st = s->successors;
658

Pierre PARUTTO's avatar
Pierre PARUTTO committed
659
      bdd res = bddfalse;
660

661
      typename transitions_t::const_iterator i;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
662 663
      for (i = st.begin(); i != st.end(); ++i)
	res |= i->condition;
664

Pierre PARUTTO's avatar
Pierre PARUTTO committed
665 666 667 668
      return res;
    }

    virtual bdd compute_support_variables(const spot::state* in) const
669
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
670 671
      const State* s = down_cast<const State*>(in);
      assert(s);
672
      const transitions_t& st = s->successors;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
673 674 675

      bdd res = bddtrue;

676
      typename transitions_t::const_iterator i;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
677 678 679 680
      for (i = st.begin(); i != st.end(); ++i)
	res &= bdd_support(i->condition);

      return res;
681
    }
682

683
    ls_map ls_;
684
    alias_map alias_;
685 686 687 688 689
    sl_map sl_;
    State* init_;

    bdd_dict* dict_;

Pierre PARUTTO's avatar
Pierre PARUTTO committed
690 691 692
    mutable bdd all_acceptance_conditions_;
    mutable bool all_acceptance_conditions_computed_;
    bdd neg_acceptance_conditions_;
693
    to_string_func_t to_string_func_;
694 695 696 697 698 699
  };

  template <typename State>
  class tgba_explicit: public explicit_graph<State, tgba>
  {
  public:
700
    tgba_explicit(bdd_dict* dict): explicit_graph<State, tgba>(dict)
701 702 703 704 705 706
    {
    }

    virtual ~tgba_explicit()
    {
    }
707

Pierre PARUTTO's avatar
Pierre PARUTTO committed
708 709 710 711
  private:
    // Disallow copy.
    tgba_explicit(const tgba_explicit<State>& other);
    tgba_explicit& operator=(const tgba_explicit& other);
712
  };
Pierre PARUTTO's avatar
Pierre PARUTTO committed
713

714 715 716 717
  template <typename State>
  class sba_explicit: public explicit_graph<State, sba>
  {
  public:
718
    sba_explicit(bdd_dict* dict): explicit_graph<State, sba>(dict)
719 720 721 722 723 724 725
    {
    }

    virtual ~sba_explicit()
    {
    }

726
    virtual bool state_is_accepting(const spot::state* s) const
727
    {
728
      const State* st = down_cast<const State*>(s);
729 730
      // Assume that an accepting state has only accepting output transitions
      // So we need only to check one to decide
731
      if (st->successors.empty())
732
	return false;
733
      return (st->successors.front().acceptance_conditions
734
	      == this->all_acceptance_conditions());
735 736 737 738 739 740 741 742 743
    }

  private:
    // Disallow copy.
    sba_explicit(const sba_explicit<State>& other);
    sba_explicit& operator=(const sba_explicit& other);
  };


744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759
  // It is tempting to write
  //
  // template<template<typename T>class graph, typename Type>
  // class explicit_conf: public graph<T>
  //
  // to simplify the typedefs at the end of the file, however swig
  // cannot parse this syntax.

  /// Configuration of graph automata
  /// \ingroup tgba_representation
  template<class graph, typename Type>
  class explicit_conf: public graph
  {
  public:
    explicit_conf(bdd_dict* d): graph(d)
    {
760
      this->set_to_string_func(to_string);
761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776
    };

    static std::string to_string(const typename Type::label_t& l)
    {
      std::stringstream ss;
      ss << l;
      return ss.str();
    }
  };

  template<class graph>
  class explicit_conf<graph, state_explicit_string>: public graph
  {
  public:
    explicit_conf(bdd_dict* d): graph(d)
    {
777
      this->set_to_string_func(to_string);
778 779 780 781 782 783 784 785 786 787 788 789 790 791
    };

    static std::string to_string(const std::string& l)
    {
      return l;
    }
  };

  template<class graph>
  class explicit_conf<graph, state_explicit_formula>: public graph
  {
  public:
    explicit_conf(bdd_dict* d): graph(d)
    {
792
      this->set_to_string_func(to_string);
793 794 795 796 797
    };

    // Enable UTF8 output for the formulae that label states.
    void enable_utf8()
    {
798
      this->set_to_string_func(to_utf8_string);
799 800 801 802 803 804 805 806 807 808 809 810 811 812
    }

    static std::string to_string(const ltl::formula* const& l)
    {
      return ltl::to_string(l);
    }

    static std::string to_utf8_string(const ltl::formula* const& l)
    {
      return ltl::to_utf8_string(l);
    }
  };


813
  // Typedefs for tgba
814 815 816 817 818 819
  typedef explicit_conf<tgba_explicit<state_explicit_string>,
			state_explicit_string> tgba_explicit_string;
  typedef explicit_conf<tgba_explicit<state_explicit_formula>,
			state_explicit_formula> tgba_explicit_formula;
  typedef explicit_conf<tgba_explicit<state_explicit_number>,
			state_explicit_number> tgba_explicit_number;
820

821
  // Typedefs for sba
822 823 824 825 826 827
  typedef explicit_conf<sba_explicit<state_explicit_string>,
			state_explicit_string> sba_explicit_string;
  typedef explicit_conf<sba_explicit<state_explicit_formula>,
			state_explicit_formula> sba_explicit_formula;
  typedef explicit_conf<sba_explicit<state_explicit_number>,
			state_explicit_number> sba_explicit_number;
828 829 830
}

#endif // SPOT_TGBA_TGBAEXPLICIT_HH