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

namespace spot
{

  // tgba_bdd_translate_proxy_succ_iterator
  // --------------------------------------
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
10

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

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

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

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

  bool
37
38
39
40
41
  tgba_bdd_translate_proxy_succ_iterator::done()
  {
    return iter_->done();
  }

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

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

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
56
  bdd
57
58
59
60
61
62
63
64
65
  tgba_bdd_translate_proxy_succ_iterator::current_promise()
  {
    return bdd_replace(iter_->current_promise(), rewrite_);
  }


  // tgba_bdd_translate_proxy
  // ------------------------

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
66
  tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from,
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
101
102
103
104
105
106
						     const tgba_bdd_dict& to)
    : 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);
      }
  }

  tgba_bdd_translate_proxy::~tgba_bdd_translate_proxy()
  {
    bdd_freepair(rewrite_from_);
    bdd_freepair(rewrite_to_);
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
107

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

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
116
  tgba_bdd_translate_proxy_succ_iterator*
117
  tgba_bdd_translate_proxy::succ_iter(const state* s) const
118
  {
119
120
121
122
123
124
125
    state* s2 = s->clone();
    s2->translate(rewrite_from_);
    tgba_bdd_translate_proxy_succ_iterator *res =
      new tgba_bdd_translate_proxy_succ_iterator(from_.succ_iter(s2),
						 rewrite_to_);
    delete s2;
    return res;
126
127
  }

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

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

}