tgbatranslateproxy.cc 3.78 KB
Newer Older
1
#include "tgbatranslateproxy.hh"
2
#include "bddprint.hh"
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
3
#include <cassert>
4
5
6
7

namespace spot
{

8
  // tgba_translate_proxy_succ_iterator
9
  // --------------------------------------
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
10

11
12
13
  tgba_translate_proxy_succ_iterator::
  tgba_translate_proxy_succ_iterator(tgba_succ_iterator* it,
				     bddPair* rewrite)
14
15
16
    : iter_(it), rewrite_(rewrite)
  {
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
17

18
  tgba_translate_proxy_succ_iterator::~tgba_translate_proxy_succ_iterator()
19
20
21
22
  {
    delete iter_;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
23
  void
24
  tgba_translate_proxy_succ_iterator::first()
25
26
27
  {
    iter_->first();
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
28
29

  void
30
  tgba_translate_proxy_succ_iterator::next()
31
32
33
  {
    iter_->next();
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
34
35

  bool
36
  tgba_translate_proxy_succ_iterator::done() const
37
38
39
40
  {
    return iter_->done();
  }

41
  state*
42
  tgba_translate_proxy_succ_iterator::current_state()
43
  {
44
45
    state* s = iter_->current_state();
    s->translate(rewrite_);
46
47
48
    return s;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
49
  bdd
50
  tgba_translate_proxy_succ_iterator::current_condition()
51
52
53
54
  {
    return bdd_replace(iter_->current_condition(), rewrite_);
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
55
  bdd
56
  tgba_translate_proxy_succ_iterator::current_accepting_conditions()
57
  {
58
    return bdd_replace(iter_->current_accepting_conditions(), rewrite_);
59
60
61
  }


62
  // tgba_translate_proxy
63
64
  // ------------------------

65
66
  tgba_translate_proxy::tgba_translate_proxy(const tgba& from,
					     const tgba_bdd_dict& to)
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
    : from_(from), to_(to)
  {
    const tgba_bdd_dict& f = from.get_dict();
    rewrite_to_ = bdd_newpair();
    rewrite_from_ = bdd_newpair();

    tgba_bdd_dict::fv_map::const_iterator i_from;
    tgba_bdd_dict::fv_map::const_iterator i_to;

    for (i_from = f.now_map.begin(); i_from != f.now_map.end(); ++i_from)
      {
	i_to = to_.now_map.find(i_from->first);
	assert(i_to != to_.now_map.end());
	bdd_setpair(rewrite_to_, i_from->second, i_to->second);
	bdd_setpair(rewrite_to_, i_from->second + 1, i_to->second + 1);
	bdd_setpair(rewrite_from_, i_to->second, i_from->second);
	bdd_setpair(rewrite_from_, i_to->second + 1, i_from->second + 1);
      }
    for (i_from = f.var_map.begin(); i_from != f.var_map.end(); ++i_from)
      {
	i_to = to_.var_map.find(i_from->first);
	assert(i_to != to_.var_map.end());
	bdd_setpair(rewrite_to_, i_from->second, i_to->second);
	bdd_setpair(rewrite_from_, i_to->second, i_from->second);
      }
92
    for (i_from = f.acc_map.begin(); i_from != f.acc_map.end(); ++i_from)
93
      {
94
95
	i_to = to_.acc_map.find(i_from->first);
	assert(i_to != to_.acc_map.end());
96
97
98
	bdd_setpair(rewrite_to_, i_from->second, i_to->second);
	bdd_setpair(rewrite_from_, i_to->second, i_from->second);
      }
99
100
101
102
103

    all_accepting_conditions_ = bdd_replace(from.all_accepting_conditions(),
					    rewrite_to_);
    neg_accepting_conditions_ = bdd_replace(from.neg_accepting_conditions(),
					    rewrite_to_);
104
105
  }

106
  tgba_translate_proxy::~tgba_translate_proxy()
107
108
109
110
  {
    bdd_freepair(rewrite_from_);
    bdd_freepair(rewrite_to_);
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
111

112
  state*
113
  tgba_translate_proxy::get_init_state() const
114
  {
115
116
    state* s = from_.get_init_state();
    s->translate(rewrite_to_);
117
118
119
    return s;
  }

120
121
  tgba_translate_proxy_succ_iterator*
  tgba_translate_proxy::succ_iter(const state* s) const
122
  {
123
124
    state* s2 = s->clone();
    s2->translate(rewrite_from_);
125
126
    tgba_translate_proxy_succ_iterator *res =
      new tgba_translate_proxy_succ_iterator(from_.succ_iter(s2),
127
128
129
						 rewrite_to_);
    delete s2;
    return res;
130
131
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
132
  const tgba_bdd_dict&
133
  tgba_translate_proxy::get_dict() const
134
135
136
  {
    return to_;
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
137

138
  std::string
139
  tgba_translate_proxy::format_state(const state* s) const
140
  {
141
142
143
144
145
    state* s2 = s->clone();
    s2->translate(rewrite_from_);
    std::string res = from_.format_state(s2);
    delete s2;
    return res;
146
147
  }

148
149
150
151
152
153
154
155
156
157
158
  bdd
  tgba_translate_proxy::all_accepting_conditions() const
  {
    return all_accepting_conditions_;
  }

  bdd tgba_translate_proxy::neg_accepting_conditions() const
  {
    return neg_accepting_conditions_;
  }

159
}