tgbaexplicit.hh 18.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
Pierre PARUTTO's avatar
Pierre PARUTTO committed
2
3
4
5
6
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita.
// 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
12
13
14
15
16
17
18
19
20
21
22
23
24
//
// 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.

25
26
27
#ifndef SPOT_TGBA_TGBAEXPLICIT_HH
# define SPOT_TGBA_TGBAEXPLICIT_HH

Pierre PARUTTO's avatar
Pierre PARUTTO committed
28
#include <sstream>
29
#include <list>
Pierre PARUTTO's avatar
Pierre PARUTTO committed
30

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

namespace spot
{
41
  // How to destroy the label of a state.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
  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();
    }
  };
59

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

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
75
    virtual ~state_explicit()
76
77
    {
    }
78

79
80
81
    void destroy() const
    {
    }
82

Pierre PARUTTO's avatar
Pierre PARUTTO committed
83
84
85
    typedef Label Label_t;
    typedef label_hash label_hash_t;

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

93
94
95
    typedef std::list<transition> transitions_t;
    transitions_t successors;

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

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
106
107
108
109
110
111
112
113
114
115
116
117
118
    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;
    }
119

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

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
132
133
134
  protected:
    Label label_;
  };
135

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

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
152
153
154
    virtual void destroy()
    {
    }
155

Pierre PARUTTO's avatar
Pierre PARUTTO committed
156
157
158
159
160
161
162
163
    static const int default_val;
    static std::string to_string(int l)
    {
      std::stringstream ss;
      ss << l;
      return ss.str();
    }
  };
164

Pierre PARUTTO's avatar
Pierre PARUTTO committed
165
166
167
168
169
170
171
172
173
174
  /// 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>()
    {
    }
175

Pierre PARUTTO's avatar
Pierre PARUTTO committed
176
177
178
179
    state_explicit_string(const std::string& label)
      : state_explicit<std::string, string_hash>(label)
    {
    }
180

Pierre PARUTTO's avatar
Pierre PARUTTO committed
181
182
183
    virtual void destroy()
    {
    }
184

Pierre PARUTTO's avatar
Pierre PARUTTO committed
185
186
187
188
189
190
    static const std::string default_val;
    static std::string to_string(const std::string& l)
    {
      return l;
    }
  };
191

Pierre PARUTTO's avatar
Pierre PARUTTO committed
192
193
194
195
196
197
198
199
200
201
  /// 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>()
    {
    }
202

Pierre PARUTTO's avatar
Pierre PARUTTO committed
203
204
205
206
    state_explicit_formula(const ltl::formula* label)
      : state_explicit<const ltl::formula*, ltl::formula_ptr_hash>(label)
    {
    }
207

Pierre PARUTTO's avatar
Pierre PARUTTO committed
208
209
210
    virtual void destroy()
    {
    }
211

Pierre PARUTTO's avatar
Pierre PARUTTO committed
212
213
214
215
216
217
    static const ltl::formula* default_val;
    static std::string to_string(const ltl::formula* l)
    {
      return ltl::to_string(l);
    }
  };
218

219
  /// Successor iterators used by spot::tgba_explicit.
220
  /// \ingroup tgba_representation
Pierre PARUTTO's avatar
Pierre PARUTTO committed
221
  template<typename State>
222
  class tgba_explicit_succ_iterator: public tgba_succ_iterator
223
224
  {
  public:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
    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_;
    }
241

Pierre PARUTTO's avatar
Pierre PARUTTO committed
242
243
244
245
    virtual bool done() const
    {
      return it_ == start_->successors.end();
    }
246

Pierre PARUTTO's avatar
Pierre PARUTTO committed
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
    virtual State* current_state() const
    {
      assert(!done());

      //ugly but I can't see any other wayout
      const State* res = down_cast<const State*>(it_->dest);
      assert(res);

      return
	const_cast<State*>(res);
    }

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

    virtual bdd current_acceptance_conditions() const
    {
      assert(!done());
268
      return it_->acceptance_conditions;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
269
    }
270

271
272
273
274
275
276
    typename State::transitions_t::const_iterator
    get_iterator() const
    {
      return it_;
    }

277
  private:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
278
279
    const State* start_;
    typename State::transitions_t::const_iterator it_;
280
    bdd all_acceptance_conditions_;
281
282
  };

Pierre PARUTTO's avatar
Pierre PARUTTO committed
283
284
285
286
  /// Graph implementation for automata representation
  /// \ingroup tgba_representation
  template<typename State, typename Type>
  class explicit_graph: public Type
287
288
  {
  protected:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
289
290
291
292
293
    typedef Sgi::hash_map<typename State::Label_t, State,
			  typename State::label_hash_t> ls_map;
    typedef Sgi::hash_map<const State*, typename State::Label_t,
			  ptr_hash<State> > sl_map;

294
  public:
295
296
    typedef typename State::transition transition;

Pierre PARUTTO's avatar
Pierre PARUTTO committed
297
298
299
300
    explicit_graph(bdd_dict* dict)
      : ls_(),
	sl_(),
	init_(0),
301
302
303
304
	dict_(dict),
	all_acceptance_conditions_(bddfalse),
	all_acceptance_conditions_computed_(false),
	neg_acceptance_conditions_(bddtrue)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
305
306
    {
    }
307

Pierre PARUTTO's avatar
Pierre PARUTTO committed
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
    State* add_default_init()
    {
      return add_state(State::default_val);
    }

    transition*
    create_transition(State* source, const State* dest)
    {
      transition t;

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

      typename State::transitions_t::iterator i =
	source->successors.insert(source->successors.end(), t);

      return &*i;
    }

    transition*
    create_transition(const typename State::Label_t& source,
		      const typename State::Label_t& dest)
    {
      // 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)
    {
342
      return const_cast<transition*>(&(*(si->get_iterator())));
Pierre PARUTTO's avatar
Pierre PARUTTO committed
343
344
345
346
347
348
349
350
351
352
    }

    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)
353
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
354
355
      dict_->register_propositions(f, this);
      t->condition &= f;
356
357
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
358
    bool has_acceptance_condition(const ltl::formula* f) const
359
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
360
361
362
363
364
365
366
367
368
369
370
371
372
      return dict_->is_registered_acceptance_variable(f, this);
    }

    //old tgba explicit labelled interface
    bool has_state(const typename State::Label_t& name)
    {
      return ls_.find(name) != ls_.end();
    }

    const typename State::Label_t& get_label(const State* s) const
    {
      typename sl_map::const_iterator i = sl_.find(s);
      assert(i != sl_.end());
373
374
375
      return i->second;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
376
    const typename State::Label_t& get_label(const spot::state* s) const
377
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
378
      const State* se = down_cast<const State*>(s);
379
      assert(se);
380
      return get_label(se);
381
382
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
    transition*
    create_trainsition(const typename State::Label_t& source,
		       const typename State::Label_t& dest)
    {
      // 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));
    }

    void
    complement_all_acceptance_conditions()
    {
      bdd all = this->all_acceptance_conditions();
      typename ls_map::iterator i;
      for (i = ls_.begin(); i != ls_.end(); ++i)
	{
	  typename State::transitions_t::iterator i2;
	  for (i2 = i->second.successors.begin();
	       i2 != i->second.successors.end(); ++i2)
	    i2->acceptance_conditions = all - i2->acceptance_conditions;
	}
    }

    void
    merge_transitions()
    {
      typename ls_map::iterator i;
      for (i = ls_.begin(); i != ls_.end(); ++i)
      {
	typename State::transitions_t::iterator t1;
	for (t1 = i->second.successors.begin();
	     t1 != i->second.successors.end(); ++t1)
	{
	  bdd acc = t1->acceptance_conditions;
	  const state_explicit<typename State::Label_t,
			       typename State::label_hash_t>* dest = t1->dest;

	  // Find another transition with the same destination and
	  // acceptance conditions.
	  typename State::transitions_t::iterator t2 = t1;
	  ++t2;
	  while (t2 != i->second.successors.end())
	  {
	    typename State::transitions_t::iterator t2copy = t2++;
	    if (t2copy->acceptance_conditions == acc && t2copy->dest == dest)
	    {
	      t1->condition |= t2copy->condition;
	      i->second.successors.erase(t2copy);
	    }
	  }
	}
      }
    }

439
    /// Return the state_explicit for \a name, creating the state if
440
    /// it does not exist.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
441
    State* add_state(const typename State::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
	{
Pierre PARUTTO's avatar
Pierre PARUTTO committed
446
447
448
	  State s(name);
	  ls_[name] = s;
	  sl_[&ls_[name]] = name;
449
450
451
452

	  // The first state we add is the inititial state.
	  // It can also be overridden with set_init_state().
	  if (!init_)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
453
	    init_ = &ls_[name];
454

Pierre PARUTTO's avatar
Pierre PARUTTO committed
455
	  return &(ls_[name]);
456
	}
Pierre PARUTTO's avatar
Pierre PARUTTO committed
457
      return &(i->second);
458
    }
459

Pierre PARUTTO's avatar
Pierre PARUTTO committed
460
461
    State*
    set_init_state(const typename State::Label_t& state)
462
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
463
      State* s = add_state(state);
464
465
466
467
      init_ = s;
      return s;
    }

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
473
474
475
476
477
478
479
480
481
482
483
484
      while (i != ls_.end())
      {
	typename State::Label_t s = i->first;

	// Do not erase the same state twice(Because of possible aliases).
	if (sl_.erase(&(i->second)))
	  i->second.destroy();

	++i;
	destroy_key<typename State::Label_t> dest;
	dest.destroy(s);
      }
485
486
487
488
489
490

      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
491
492
493
    }

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

      return init_;
499
500
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
501
502
503
504
    virtual tgba_explicit_succ_iterator<State>*
    succ_iter(const spot::state* state,
	      const spot::state* global_state = 0,
	      const tgba* global_automaton = 0) const
505
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
506
507
508
509
510
511
512
513
514
515
      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());
516
517
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
    //no need?
    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());
      return State::to_string(i->second);
    }

    /// old implementation in tgba_explicit_string
    /// Create an alias for a state.  Any reference to \a alias_name
    /// will act as a reference to \a real_name.
    void add_state_alias(const typename State::Label_t& alias,
			 const typename State::Label_t& real)
    {
      ls_[alias] = *(add_state(real));
    }


    /// \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;
    }

551
552

    /// Acceptance conditions handlingx
Pierre PARUTTO's avatar
Pierre PARUTTO committed
553
554
555
556
557
558
559
560
561
562
563
564
    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)
565
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
566
567
568
569
570
571
572
573
574
575
576
      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)
577
	{
Pierre PARUTTO's avatar
Pierre PARUTTO committed
578
579
	  neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup));
	  sup = bdd_high(sup);
580
	}
Pierre PARUTTO's avatar
Pierre PARUTTO committed
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
      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_;
603
604
605
606
607
    }

    void
    declare_acceptance_condition(const ltl::formula* f)
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
608
      int v = this->dict_->register_acceptance_variable(f, this);
609
610
611
612
613
      f->destroy();
      bdd neg = bdd_nithvar(v);
      neg_acceptance_conditions_ &= neg;

      // Append neg to all acceptance conditions.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
614
615
      typename explicit_graph<State, tgba>::ls_map::iterator i;
      for (i = this->ls_.begin(); i != this->ls_.end(); ++i)
616
	{
Pierre PARUTTO's avatar
Pierre PARUTTO committed
617
618
619
	  typename State::transitions_t::iterator i2;
	  for (i2 = i->second.successors.begin();
	       i2 != i->second.successors.end(); ++i2)
620
	    i2->acceptance_conditions &= neg;
621
622
623
624
625
	}

      all_acceptance_conditions_computed_ = false;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
626
  protected:
627

Pierre PARUTTO's avatar
Pierre PARUTTO committed
628
    bdd get_acceptance_condition(const ltl::formula* f)
629
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
630
631
632
633
634
635
      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;
636
637
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
638
    virtual bdd compute_support_conditions(const spot::state* in) const
639
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
640
641
642
      const State* s = down_cast<const State*>(in);
      assert(s);
      const typename State::transitions_t& st = s->successors;
643

Pierre PARUTTO's avatar
Pierre PARUTTO committed
644
      bdd res = bddfalse;
645

Pierre PARUTTO's avatar
Pierre PARUTTO committed
646
647
648
      typename State::transitions_t::const_iterator i;
      for (i = st.begin(); i != st.end(); ++i)
	res |= i->condition;
649

Pierre PARUTTO's avatar
Pierre PARUTTO committed
650
651
652
653
      return res;
    }

    virtual bdd compute_support_variables(const spot::state* in) const
654
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
655
656
657
658
659
660
661
662
663
664
665
      const State* s = down_cast<const State*>(in);
      assert(s);
      const typename State::transitions_t& st = s->successors;

      bdd res = bddtrue;

      typename State::transitions_t::const_iterator i;
      for (i = st.begin(); i != st.end(); ++i)
	res &= bdd_support(i->condition);

      return res;
666
    }
667

668
669
670
671
672
673
    ls_map ls_;
    sl_map sl_;
    State* init_;

    bdd_dict* dict_;

Pierre PARUTTO's avatar
Pierre PARUTTO committed
674
675
676
    mutable bdd all_acceptance_conditions_;
    mutable bool all_acceptance_conditions_computed_;
    bdd neg_acceptance_conditions_;
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
  };

  template <typename State>
  class tgba_explicit: public explicit_graph<State, tgba>
  {
  public:
    typedef typename State::transition transition;
    typedef State state;

    tgba_explicit(bdd_dict* dict):
      explicit_graph<State,tgba>(dict)
    {
    }

    virtual ~tgba_explicit()
    {
    }
694

Pierre PARUTTO's avatar
Pierre PARUTTO committed
695
696
697
698
  private:
    // Disallow copy.
    tgba_explicit(const tgba_explicit<State>& other);
    tgba_explicit& operator=(const tgba_explicit& other);
699
  };
Pierre PARUTTO's avatar
Pierre PARUTTO committed
700

701
702
703
704
705
706
  template <typename State>
  class sba_explicit: public explicit_graph<State, sba>
  {
  public:
    typedef typename State::transition transition;
    typedef State state;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
707

708
709
710
711
712
713
714
715
716
    sba_explicit(bdd_dict* dict):
      explicit_graph<State, sba>(dict)
    {
    }

    virtual ~sba_explicit()
    {
    }

717
    virtual bool state_is_accepting(const spot::state* s) const
718
    {
719
720
      // Assume that an accepting state has only accepting output transitions
      // So we need only to check one to decide
721
      tgba_explicit_succ_iterator<State>* it = this->succ_iter(s);
722
723
724
725
      it->first();

      // no transition
      if (it->done())
726
      {
727
728
	delete it;
	return false;
729
730
      }

731
      bool res = it->current_acceptance_conditions() != bddfalse;
732
733
      delete it;

734
      return res;
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
  // Typedefs for tgba
Pierre PARUTTO's avatar
Pierre PARUTTO committed
745
746
747
  typedef tgba_explicit<state_explicit_string> tgba_explicit_string;
  typedef tgba_explicit<state_explicit_formula> tgba_explicit_formula;
  typedef tgba_explicit<state_explicit_number> tgba_explicit_number;
748

749
  // Typedefs for sba
750
751
752
  typedef sba_explicit<state_explicit_string> sba_explicit_string;
  typedef sba_explicit<state_explicit_formula> sba_explicit_formula;
  typedef sba_explicit<state_explicit_number> sba_explicit_number;
753
754
755
}

#endif // SPOT_TGBA_TGBAEXPLICIT_HH