tgbabddconcrete.hh 834 Bytes
Newer Older
1
2
3
#ifndef SPOT_TGBA_TGBABDDCONCRETE_HH
# define SPOT_TGBA_TGBABDDCONCRETE_HH

4
#include "tgba.hh"
5
6
7
8
9
10
#include "statebdd.hh"
#include "tgbabddfactory.hh"
#include "succiterconcrete.hh"

namespace spot
{
11
  class tgba_bdd_concrete: public tgba
12
13
14
15
16
  {
  public:
    tgba_bdd_concrete(const tgba_bdd_factory& fact);
    tgba_bdd_concrete(const tgba_bdd_factory& fact, bdd init);
    ~tgba_bdd_concrete();
17

18
    void set_init_state(bdd s);
19
20
    state_bdd* get_init_state() const;
    bdd get_init_bdd() const;
21

22
    tgba_succ_iterator_concrete* succ_iter(const state* state) const;
23

24
25
    const tgba_bdd_dict& get_dict() const;
    const tgba_bdd_core_data& get_core_data() const;
26

27
28
29
30
31
32
33
34
35
  protected:
    tgba_bdd_core_data data_;
    tgba_bdd_dict dict_;
    bdd init_;
    friend class tgba_tgba_succ_iterator;
  };
}

#endif // SPOT_TGBA_TGBABDDCONCRETE_HH