tgbatranslateproxy.hh 1.79 KB
Newer Older
1
2
#ifndef SPOT_TGBA_TGBATRANSLATEPROXY_HH
# define SPOT_TGBA_TGBATRANSLATEPROXY_HH
3
4
5
6
7

#include "tgba.hh"

namespace spot
{
8
  /// \brief Proxy for a spot::tgba_succ_iterator_concrete that renumber
9
  /// BDD variables on the fly.
10
  class tgba_translate_proxy_succ_iterator: public tgba_succ_iterator
11
12
  {
  public:
13
14
15
    tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it,
				       bddPair* rewrite);
    virtual ~tgba_translate_proxy_succ_iterator();
16
17
18
19

    // iteration
    void first();
    void next();
20
    bool done() const;
21
22

    // inspection
23
    state* current_state();
24
    bdd current_condition();
25
    bdd current_accepting_conditions();
26
  protected:
27
    tgba_succ_iterator* iter_;
28
29
30
31
32
33
    bddPair* rewrite_;
  };


  /// \brief Proxy for a spot::tgba_bdd_concrete that renumber BDD variables
  /// on the fly.
34
  class tgba_translate_proxy: public tgba
35
36
  {
  public:
37
    /// \brief Constructor.
38
39
    /// \param from The spot::tgba to masquerade.
    /// \param to The new dictionary to use.
40
41
    tgba_translate_proxy(const tgba& from,
			 const tgba_bdd_dict& to);
42

43
    virtual ~tgba_translate_proxy();
44

45
    virtual state* get_init_state() const;
46

47
    virtual tgba_translate_proxy_succ_iterator*
48
49
50
51
    succ_iter(const state* state) const;

    virtual const tgba_bdd_dict& get_dict() const;

52
53
    virtual std::string format_state(const state* state) const;

54
55
56
57
    virtual bdd all_accepting_conditions() const;

    virtual bdd neg_accepting_conditions() const;

58
59
60
61
62
  private:
    const tgba& from_;		///< The spot::tgba to masquerade.
    tgba_bdd_dict to_;		///< The new dictionar to use.
    bddPair* rewrite_to_;	///< The rewriting pair for from->to.
    bddPair* rewrite_from_;	///< The rewriting pair for to->from.
63
64
    bdd all_accepting_conditions_;
    bdd neg_accepting_conditions_;
65
  };
66

67
68
}

69
#endif // SPOT_TGBA_TGBATRANSLATEPROXY_HH