tgbabddconcrete.cc 1020 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
#include "tgbabddconcrete.hh"

namespace spot
{
  tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact)
    : data_(fact.get_core_data()), dict_(fact.get_dict())
  {
  }

  tgba_bdd_concrete::tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init)
    : data_(fact.get_core_data()), dict_(fact.get_dict()), init_(init)
  {
  }

  tgba_bdd_concrete::~tgba_bdd_concrete()
  {
  }

  void
  tgba_bdd_concrete::set_init_state(bdd s)
  {
    init_ = s;
  }

  state_bdd
  tgba_bdd_concrete::get_init_state() const
  {
    return init_;
  }

  tgba_succ_iterator_concrete*
32
  tgba_bdd_concrete::succ_iter(state_bdd state) const
33
  {
34
    bdd succ_set = bdd_replace(bdd_exist(data_.relation & state.as_bdd(),
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
					 data_.now_set),
			       data_.next_to_now);
    return new tgba_succ_iterator_concrete(data_, succ_set);
  }

  const tgba_bdd_dict&
  tgba_bdd_concrete::get_dict() const
  {
    return dict_;
  }

  const tgba_bdd_core_data&
  tgba_bdd_concrete::get_core_data() const
  {
    return data_;
  }

}