tgbatranslateproxy.cc 3.34 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()
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_promise()
57
58
59
60
61
  {
    return bdd_replace(iter_->current_promise(), rewrite_);
  }


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
92
93
94
95
96
97
98
99
100
    : 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);
      }
    for (i_from = f.prom_map.begin(); i_from != f.prom_map.end(); ++i_from)
      {
	i_to = to_.prom_map.find(i_from->first);
	assert(i_to != to_.prom_map.end());
	bdd_setpair(rewrite_to_, i_from->second, i_to->second);
	bdd_setpair(rewrite_from_, i_to->second, i_from->second);
      }
  }

101
  tgba_translate_proxy::~tgba_translate_proxy()
102
103
104
105
  {
    bdd_freepair(rewrite_from_);
    bdd_freepair(rewrite_to_);
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
106

107
  state*
108
  tgba_translate_proxy::get_init_state() const
109
  {
110
111
    state* s = from_.get_init_state();
    s->translate(rewrite_to_);
112
113
114
    return s;
  }

115
116
  tgba_translate_proxy_succ_iterator*
  tgba_translate_proxy::succ_iter(const state* s) const
117
  {
118
119
    state* s2 = s->clone();
    s2->translate(rewrite_from_);
120
121
    tgba_translate_proxy_succ_iterator *res =
      new tgba_translate_proxy_succ_iterator(from_.succ_iter(s2),
122
123
124
						 rewrite_to_);
    delete s2;
    return res;
125
126
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
127
  const tgba_bdd_dict&
128
  tgba_translate_proxy::get_dict() const
129
130
131
  {
    return to_;
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
132

133
  std::string
134
  tgba_translate_proxy::format_state(const state* s) const
135
  {
136
137
138
139
140
    state* s2 = s->clone();
    s2->translate(rewrite_from_);
    std::string res = from_.format_state(s2);
    delete s2;
    return res;
141
142
143
  }

}