tgbaexplicit.hh 19.5 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
    virtual void destroy() const
80
81
    {
    }
82

83
    typedef Label label_t;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
84
85
    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
    static const int default_val;
  };
154

Pierre PARUTTO's avatar
Pierre PARUTTO committed
155
156
157
158
159
160
161
162
163
164
  /// 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>()
    {
    }
165

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
171
172
    static const std::string default_val;
  };
173

Pierre PARUTTO's avatar
Pierre PARUTTO committed
174
175
176
177
178
179
180
181
182
183
  /// 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>()
    {
    }
184

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

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

193
  /// Successor iterators used by spot::tgba_explicit.
194
  /// \ingroup tgba_representation
Pierre PARUTTO's avatar
Pierre PARUTTO committed
195
  template<typename State>
196
  class tgba_explicit_succ_iterator: public tgba_succ_iterator
197
198
  {
  public:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
    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_;
    }
215

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

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

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

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

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

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

253
  /// Graph implementation for explicit automgon
Pierre PARUTTO's avatar
Pierre PARUTTO committed
254
255
256
  /// \ingroup tgba_representation
  template<typename State, typename Type>
  class explicit_graph: public Type
257
  {
258
259
260
261
262
263
  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;
264
  protected:
265
266
    typedef Sgi::hash_map<label_t, State, label_hash_t> ls_map;
    typedef Sgi::hash_map<const State*, label_t, ptr_hash<State> > sl_map;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
267

268
  public:
269

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

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

286
287
288
289
290
291
    size_t num_states() const
    {
      // Do not use ls_.size() because it may contain aliases.
      return sl_.size();
    }

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

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

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

      return &*i;
    }

    transition*
308
    create_transition(const label_t& source, const label_t& dest)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
309
310
311
312
313
314
315
316
317
318
319
    {
      // 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)
    {
320
      return const_cast<transition*>(&(*(si->get_iterator())));
Pierre PARUTTO's avatar
Pierre PARUTTO committed
321
322
323
324
325
326
327
328
329
330
    }

    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)
331
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
332
333
      dict_->register_propositions(f, this);
      t->condition &= f;
334
335
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
336
    bool has_acceptance_condition(const ltl::formula* f) const
337
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
338
339
340
341
      return dict_->is_registered_acceptance_variable(f, this);
    }

    //old tgba explicit labelled interface
342
    bool has_state(const label_t& name)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
343
344
345
346
    {
      return ls_.find(name) != ls_.end();
    }

347
    const label_t& get_label(const State* s) const
Pierre PARUTTO's avatar
Pierre PARUTTO committed
348
349
350
    {
      typename sl_map::const_iterator i = sl_.find(s);
      assert(i != sl_.end());
351
352
353
      return i->second;
    }

354
    const label_t& get_label(const spot::state* s) const
355
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
356
      const State* se = down_cast<const State*>(s);
357
      assert(se);
358
      return get_label(se);
359
360
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
361
    transition*
362
    create_trainsition(const label_t& source, const label_t& dest)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
    {
      // 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)
	{
378
	  typename transitions_t::iterator i2;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
379
380
381
382
383
384
385
386
387
388
389
390
	  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)
      {
391
	typename transitions_t::iterator t1;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
392
393
394
395
	for (t1 = i->second.successors.begin();
	     t1 != i->second.successors.end(); ++t1)
	{
	  bdd acc = t1->acceptance_conditions;
396
	  const state_explicit<label_t, label_hash_t>* dest = t1->dest;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
397
398
399

	  // Find another transition with the same destination and
	  // acceptance conditions.
400
	  typename transitions_t::iterator t2 = t1;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
401
402
403
	  ++t2;
	  while (t2 != i->second.successors.end())
	  {
404
	    typename transitions_t::iterator t2copy = t2++;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
405
406
407
408
409
410
411
412
413
414
	    if (t2copy->acceptance_conditions == acc && t2copy->dest == dest)
	    {
	      t1->condition |= t2copy->condition;
	      i->second.successors.erase(t2copy);
	    }
	  }
	}
      }
    }

415
    /// Return the state_explicit for \a name, creating the state if
416
    /// it does not exist.
417
    State* add_state(const label_t& name)
418
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
419
420
      typename ls_map::iterator i = ls_.find(name);
      if (i == ls_.end())
421
	{
Pierre PARUTTO's avatar
Pierre PARUTTO committed
422
423
424
	  State s(name);
	  ls_[name] = s;
	  sl_[&ls_[name]] = name;
425
426
427
428

	  // 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
429
	    init_ = &ls_[name];
430

Pierre PARUTTO's avatar
Pierre PARUTTO committed
431
	  return &(ls_[name]);
432
	}
Pierre PARUTTO's avatar
Pierre PARUTTO committed
433
      return &(i->second);
434
    }
435

Pierre PARUTTO's avatar
Pierre PARUTTO committed
436
    State*
437
    set_init_state(const label_t& state)
438
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
439
      State* s = add_state(state);
440
441
442
443
      init_ = s;
      return s;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
444
445
446
447
    // tgba interface
    virtual ~explicit_graph()
    {
      typename ls_map::iterator i = ls_.begin();
448

Pierre PARUTTO's avatar
Pierre PARUTTO committed
449
450
      while (i != ls_.end())
      {
451
	label_t s = i->first;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
452
453
454
455
456
457

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

	++i;
458
	destroy_key<label_t> dest;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
459
460
	dest.destroy(s);
      }
461
462
463
464
465
466

      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
467
468
469
    }

    virtual State* get_init_state() const
470
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
471
472
473
474
      if (!init_)
	const_cast<explicit_graph<State, Type>*>(this)->add_default_init();

      return init_;
475
476
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
477
478
479
480
    virtual tgba_explicit_succ_iterator<State>*
    succ_iter(const spot::state* state,
	      const spot::state* global_state = 0,
	      const tgba* global_automaton = 0) const
481
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
482
483
484
485
486
487
488
489
490
491
      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());
492
493
    }

494
495
496
497
498
499
500
501
502
503
504
505
506

    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
507
508
509
510
511
512
    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());
513
514
      assert(to_string_func_);
      return to_string_func_(i->second);
Pierre PARUTTO's avatar
Pierre PARUTTO committed
515
516
517
518
    }

    /// Create an alias for a state.  Any reference to \a alias_name
    /// will act as a reference to \a real_name.
519
    void add_state_alias(const label_t& alias, const label_t& real)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
    {
      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;
    }

538
539

    /// Acceptance conditions handlingx
Pierre PARUTTO's avatar
Pierre PARUTTO committed
540
541
542
543
544
545
546
547
548
549
550
551
    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)
552
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
553
554
555
556
557
558
559
560
561
562
563
      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)
564
	{
Pierre PARUTTO's avatar
Pierre PARUTTO committed
565
566
	  neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup));
	  sup = bdd_high(sup);
567
	}
Pierre PARUTTO's avatar
Pierre PARUTTO committed
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
      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_;
590
591
592
593
594
    }

    void
    declare_acceptance_condition(const ltl::formula* f)
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
595
      int v = this->dict_->register_acceptance_variable(f, this);
596
597
598
599
600
      f->destroy();
      bdd neg = bdd_nithvar(v);
      neg_acceptance_conditions_ &= neg;

      // Append neg to all acceptance conditions.
Pierre PARUTTO's avatar
Pierre PARUTTO committed
601
602
      typename explicit_graph<State, tgba>::ls_map::iterator i;
      for (i = this->ls_.begin(); i != this->ls_.end(); ++i)
603
	{
604
	  typename transitions_t::iterator i2;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
605
606
	  for (i2 = i->second.successors.begin();
	       i2 != i->second.successors.end(); ++i2)
607
	    i2->acceptance_conditions &= neg;
608
609
610
611
612
	}

      all_acceptance_conditions_computed_ = false;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
613
  protected:
614

Pierre PARUTTO's avatar
Pierre PARUTTO committed
615
    bdd get_acceptance_condition(const ltl::formula* f)
616
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
617
618
619
620
621
622
      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;
623
624
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
625
    virtual bdd compute_support_conditions(const spot::state* in) const
626
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
627
628
      const State* s = down_cast<const State*>(in);
      assert(s);
629
      const transitions_t& st = s->successors;
630

Pierre PARUTTO's avatar
Pierre PARUTTO committed
631
      bdd res = bddfalse;
632

633
      typename transitions_t::const_iterator i;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
634
635
      for (i = st.begin(); i != st.end(); ++i)
	res |= i->condition;
636

Pierre PARUTTO's avatar
Pierre PARUTTO committed
637
638
639
640
      return res;
    }

    virtual bdd compute_support_variables(const spot::state* in) const
641
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
642
643
      const State* s = down_cast<const State*>(in);
      assert(s);
644
      const transitions_t& st = s->successors;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
645
646
647

      bdd res = bddtrue;

648
      typename transitions_t::const_iterator i;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
649
650
651
652
      for (i = st.begin(); i != st.end(); ++i)
	res &= bdd_support(i->condition);

      return res;
653
    }
654

655
656
657
658
659
660
    ls_map ls_;
    sl_map sl_;
    State* init_;

    bdd_dict* dict_;

Pierre PARUTTO's avatar
Pierre PARUTTO committed
661
662
663
    mutable bdd all_acceptance_conditions_;
    mutable bool all_acceptance_conditions_computed_;
    bdd neg_acceptance_conditions_;
664
    to_string_func_t to_string_func_;
665
666
667
668
669
670
  };

  template <typename State>
  class tgba_explicit: public explicit_graph<State, tgba>
  {
  public:
671
    tgba_explicit(bdd_dict* dict): explicit_graph<State, tgba>(dict)
672
673
674
675
676
677
    {
    }

    virtual ~tgba_explicit()
    {
    }
678

Pierre PARUTTO's avatar
Pierre PARUTTO committed
679
680
681
682
  private:
    // Disallow copy.
    tgba_explicit(const tgba_explicit<State>& other);
    tgba_explicit& operator=(const tgba_explicit& other);
683
  };
Pierre PARUTTO's avatar
Pierre PARUTTO committed
684

685
686
687
688
  template <typename State>
  class sba_explicit: public explicit_graph<State, sba>
  {
  public:
689
    sba_explicit(bdd_dict* dict): explicit_graph<State, sba>(dict)
690
691
692
693
694
695
696
    {
    }

    virtual ~sba_explicit()
    {
    }

697
    virtual bool state_is_accepting(const spot::state* s) const
698
    {
699
      const State* st = down_cast<const State*>(s);
700
701
      // Assume that an accepting state has only accepting output transitions
      // So we need only to check one to decide
702
      if (st->successors.empty())
703
	return false;
704
      return st->successors.front().acceptance_conditions != bddfalse;
705
706
707
708
709
710
711
712
713
    }

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


714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
  // 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)
    {
730
      this->set_to_string_func(to_string);
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
    };

    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)
    {
747
      this->set_to_string_func(to_string);
748
749
750
751
752
753
754
755
756
757
758
759
760
761
    };

    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)
    {
762
      this->set_to_string_func(to_string);
763
764
765
766
767
    };

    // Enable UTF8 output for the formulae that label states.
    void enable_utf8()
    {
768
      this->set_to_string_func(to_utf8_string);
769
770
771
772
773
774
775
776
777
778
779
780
781
782
    }

    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);
    }
  };


783
  // Typedefs for tgba
784
785
786
787
788
789
  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;
790

791
  // Typedefs for sba
792
793
794
795
796
797
  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;
798
799
800
}

#endif // SPOT_TGBA_TGBAEXPLICIT_HH