tgbaexplicit.hh 19.7 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

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
154
    virtual void destroy()
    {
    }
155

Pierre PARUTTO's avatar
Pierre PARUTTO committed
156
157
    static const int default_val;
  };
158

Pierre PARUTTO's avatar
Pierre PARUTTO committed
159
160
161
162
163
164
165
166
167
168
  /// 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>()
    {
    }
169

Pierre PARUTTO's avatar
Pierre PARUTTO committed
170
171
172
173
    state_explicit_string(const std::string& label)
      : state_explicit<std::string, string_hash>(label)
    {
    }
174

Pierre PARUTTO's avatar
Pierre PARUTTO committed
175
176
177
    virtual void destroy()
    {
    }
178

Pierre PARUTTO's avatar
Pierre PARUTTO committed
179
180
    static const std::string default_val;
  };
181

Pierre PARUTTO's avatar
Pierre PARUTTO committed
182
183
184
185
186
187
188
189
190
191
  /// 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>()
    {
    }
192

Pierre PARUTTO's avatar
Pierre PARUTTO committed
193
194
195
196
    state_explicit_formula(const ltl::formula* label)
      : state_explicit<const ltl::formula*, ltl::formula_ptr_hash>(label)
    {
    }
197

Pierre PARUTTO's avatar
Pierre PARUTTO committed
198
199
200
    virtual void destroy()
    {
    }
201

Pierre PARUTTO's avatar
Pierre PARUTTO committed
202
203
    static const ltl::formula* default_val;
  };
204

205
  /// Successor iterators used by spot::tgba_explicit.
206
  /// \ingroup tgba_representation
Pierre PARUTTO's avatar
Pierre PARUTTO committed
207
  template<typename State>
208
  class tgba_explicit_succ_iterator: public tgba_succ_iterator
209
210
  {
  public:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
    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_;
    }
227

Pierre PARUTTO's avatar
Pierre PARUTTO committed
228
229
230
231
    virtual bool done() const
    {
      return it_ == start_->successors.end();
    }
232

Pierre PARUTTO's avatar
Pierre PARUTTO committed
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
    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());
254
      return it_->acceptance_conditions;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
255
    }
256

257
258
259
260
261
262
    typename State::transitions_t::const_iterator
    get_iterator() const
    {
      return it_;
    }

263
  private:
Pierre PARUTTO's avatar
Pierre PARUTTO committed
264
265
    const State* start_;
    typename State::transitions_t::const_iterator it_;
266
    bdd all_acceptance_conditions_;
267
268
  };

269
  /// Graph implementation for explicit automgon
Pierre PARUTTO's avatar
Pierre PARUTTO committed
270
271
272
  /// \ingroup tgba_representation
  template<typename State, typename Type>
  class explicit_graph: public Type
273
  {
274
275
276
277
278
279
  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;
280
  protected:
281
282
    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
283

284
  public:
285

Pierre PARUTTO's avatar
Pierre PARUTTO committed
286
287
288
289
    explicit_graph(bdd_dict* dict)
      : ls_(),
	sl_(),
	init_(0),
290
291
292
293
	dict_(dict),
	all_acceptance_conditions_(bddfalse),
	all_acceptance_conditions_computed_(false),
	neg_acceptance_conditions_(bddtrue)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
294
295
    {
    }
296

Pierre PARUTTO's avatar
Pierre PARUTTO committed
297
298
299
300
301
302
303
304
305
306
307
308
309
310
    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;

311
      typename transitions_t::iterator i =
Pierre PARUTTO's avatar
Pierre PARUTTO committed
312
313
314
315
316
317
	source->successors.insert(source->successors.end(), t);

      return &*i;
    }

    transition*
318
    create_transition(const label_t& source, const label_t& dest)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
319
320
321
322
323
324
325
326
327
328
329
    {
      // 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)
    {
330
      return const_cast<transition*>(&(*(si->get_iterator())));
Pierre PARUTTO's avatar
Pierre PARUTTO committed
331
332
333
334
335
336
337
338
339
340
    }

    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)
341
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
342
343
      dict_->register_propositions(f, this);
      t->condition &= f;
344
345
    }

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

    //old tgba explicit labelled interface
352
    bool has_state(const label_t& name)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
353
354
355
356
    {
      return ls_.find(name) != ls_.end();
    }

357
    const label_t& get_label(const State* s) const
Pierre PARUTTO's avatar
Pierre PARUTTO committed
358
359
360
    {
      typename sl_map::const_iterator i = sl_.find(s);
      assert(i != sl_.end());
361
362
363
      return i->second;
    }

364
    const label_t& get_label(const spot::state* s) const
365
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
366
      const State* se = down_cast<const State*>(s);
367
      assert(se);
368
      return get_label(se);
369
370
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
371
    transition*
372
    create_trainsition(const label_t& source, const label_t& dest)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
    {
      // 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)
	{
388
	  typename transitions_t::iterator i2;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
389
390
391
392
393
394
395
396
397
398
399
400
	  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)
      {
401
	typename transitions_t::iterator t1;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
402
403
404
405
	for (t1 = i->second.successors.begin();
	     t1 != i->second.successors.end(); ++t1)
	{
	  bdd acc = t1->acceptance_conditions;
406
	  const state_explicit<label_t, label_hash_t>* dest = t1->dest;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
407
408
409

	  // Find another transition with the same destination and
	  // acceptance conditions.
410
	  typename transitions_t::iterator t2 = t1;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
411
412
413
	  ++t2;
	  while (t2 != i->second.successors.end())
	  {
414
	    typename transitions_t::iterator t2copy = t2++;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
415
416
417
418
419
420
421
422
423
424
	    if (t2copy->acceptance_conditions == acc && t2copy->dest == dest)
	    {
	      t1->condition |= t2copy->condition;
	      i->second.successors.erase(t2copy);
	    }
	  }
	}
      }
    }

425
    /// Return the state_explicit for \a name, creating the state if
426
    /// it does not exist.
427
    State* add_state(const label_t& name)
428
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
429
430
      typename ls_map::iterator i = ls_.find(name);
      if (i == ls_.end())
431
	{
Pierre PARUTTO's avatar
Pierre PARUTTO committed
432
433
434
	  State s(name);
	  ls_[name] = s;
	  sl_[&ls_[name]] = name;
435
436
437
438

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
441
	  return &(ls_[name]);
442
	}
Pierre PARUTTO's avatar
Pierre PARUTTO committed
443
      return &(i->second);
444
    }
445

Pierre PARUTTO's avatar
Pierre PARUTTO committed
446
    State*
447
    set_init_state(const label_t& state)
448
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
449
      State* s = add_state(state);
450
451
452
453
      init_ = s;
      return s;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
454
455
456
457
    // tgba interface
    virtual ~explicit_graph()
    {
      typename ls_map::iterator i = ls_.begin();
458

Pierre PARUTTO's avatar
Pierre PARUTTO committed
459
460
      while (i != ls_.end())
      {
461
	label_t s = i->first;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
462
463
464
465
466
467

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

	++i;
468
	destroy_key<label_t> dest;
Pierre PARUTTO's avatar
Pierre PARUTTO committed
469
470
	dest.destroy(s);
      }
471
472
473
474
475
476

      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
477
478
479
    }

    virtual State* get_init_state() const
480
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
481
482
483
484
      if (!init_)
	const_cast<explicit_graph<State, Type>*>(this)->add_default_init();

      return init_;
485
486
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
487
488
489
490
    virtual tgba_explicit_succ_iterator<State>*
    succ_iter(const spot::state* state,
	      const spot::state* global_state = 0,
	      const tgba* global_automaton = 0) const
491
    {
Pierre PARUTTO's avatar
Pierre PARUTTO committed
492
493
494
495
496
497
498
499
500
501
      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());
502
503
    }

504
505
506
507
508
509
510
511
512
513
514
515
516

    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
517
518
519
520
521
522
    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());
523
524
      assert(to_string_func_);
      return to_string_func_(i->second);
Pierre PARUTTO's avatar
Pierre PARUTTO committed
525
526
527
528
529
    }

    /// 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.
530
    void add_state_alias(const label_t& alias, const label_t& real)
Pierre PARUTTO's avatar
Pierre PARUTTO committed
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
    {
      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;
    }

549
550

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

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

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

      all_acceptance_conditions_computed_ = false;
    }

Pierre PARUTTO's avatar
Pierre PARUTTO committed
624
  protected:
625

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

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
642
      bdd res = bddfalse;
643

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

Pierre PARUTTO's avatar
Pierre PARUTTO committed
648
649
650
651
      return res;
    }

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

      bdd res = bddtrue;

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

      return res;
664
    }
665

666
667
668
669
670
671
    ls_map ls_;
    sl_map sl_;
    State* init_;

    bdd_dict* dict_;

Pierre PARUTTO's avatar
Pierre PARUTTO committed
672
673
674
    mutable bdd all_acceptance_conditions_;
    mutable bool all_acceptance_conditions_computed_;
    bdd neg_acceptance_conditions_;
675
    to_string_func_t to_string_func_;
676
677
678
679
680
681
  };

  template <typename State>
  class tgba_explicit: public explicit_graph<State, tgba>
  {
  public:
682
    tgba_explicit(bdd_dict* dict): explicit_graph<State,tgba>(dict)
683
684
685
686
687
688
    {
    }

    virtual ~tgba_explicit()
    {
    }
689

Pierre PARUTTO's avatar
Pierre PARUTTO committed
690
691
692
693
  private:
    // Disallow copy.
    tgba_explicit(const tgba_explicit<State>& other);
    tgba_explicit& operator=(const tgba_explicit& other);
694
  };
Pierre PARUTTO's avatar
Pierre PARUTTO committed
695

696
697
698
699
  template <typename State>
  class sba_explicit: public explicit_graph<State, sba>
  {
  public:
700
    sba_explicit(bdd_dict* dict): explicit_graph<State, sba>(dict)
701
702
703
704
705
706
707
    {
    }

    virtual ~sba_explicit()
    {
    }

708
    virtual bool state_is_accepting(const spot::state* s) const
709
    {
710
711
      // Assume that an accepting state has only accepting output transitions
      // So we need only to check one to decide
712
      tgba_explicit_succ_iterator<State>* it = this->succ_iter(s);
713
714
715
716
      it->first();

      // no transition
      if (it->done())
717
      {
718
719
	delete it;
	return false;
720
721
      }

722
      bool res = it->current_acceptance_conditions() != bddfalse;
723
724
      delete it;

725
      return res;
726
727
728
729
730
731
732
733
734
    }

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


735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
  // 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)
    {
      set_to_string_func(to_string);
    };

    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)
    {
      set_to_string_func(to_string);
    };

    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)
    {
      set_to_string_func(to_string);
    };

    // Enable UTF8 output for the formulae that label states.
    void enable_utf8()
    {
      set_to_string_func(to_utf8_string);
    }

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


804
  // Typedefs for tgba
805
806
807
808
809
810
  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;
811

812
  // Typedefs for sba
813
814
815
816
817
818
  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;
819
820
821
}

#endif // SPOT_TGBA_TGBAEXPLICIT_HH