tgbabddtranslateproxy.cc 3.53 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
12
13
14
15
16
  tgba_bdd_translate_proxy_succ_iterator::
  tgba_bdd_translate_proxy_succ_iterator(tgba_succ_iterator_concrete* it,
					 bddPair* rewrite)
    : iter_(it), rewrite_(rewrite)
  {
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
17
18

  void
19
20
21
22
  tgba_bdd_translate_proxy_succ_iterator::first()
  {
    iter_->first();
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
23
24

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

  bool
31
32
33
34
35
  tgba_bdd_translate_proxy_succ_iterator::done()
  {
    return iter_->done();
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
36
  state_bdd*
37
38
39
40
41
42
43
  tgba_bdd_translate_proxy_succ_iterator::current_state()
  {
    state_bdd* s = iter_->current_state();
    s->as_bdd() = bdd_replace(s->as_bdd(), rewrite_);
    return s;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
44
  bdd
45
46
47
48
49
  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
50
  bdd
51
52
53
54
55
56
57
58
59
  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
60
  tgba_bdd_translate_proxy::tgba_bdd_translate_proxy(const tgba& from,
61
62
63
64
65
66
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
						     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
101
102

  state_bdd*
103
104
105
106
107
108
109
110
  tgba_bdd_translate_proxy::get_init_state() const
  {
    state_bdd* s = dynamic_cast<state_bdd*>(from_.get_init_state());
    assert(s);
    s->as_bdd() = bdd_replace(s->as_bdd(), rewrite_to_);
    return s;
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
111
  tgba_bdd_translate_proxy_succ_iterator*
112
113
114
115
  tgba_bdd_translate_proxy::succ_iter(const state* state) const
  {
    const state_bdd* s = dynamic_cast<const state_bdd*>(state);
    assert(s);
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
116
117
    state_bdd s2(bdd_replace(s->as_bdd(), rewrite_from_));
    tgba_succ_iterator_concrete* it =
118
119
120
121
122
      dynamic_cast<tgba_succ_iterator_concrete*>(from_.succ_iter(&s2));
    assert(it);
    return new tgba_bdd_translate_proxy_succ_iterator(it, rewrite_to_);
  }

Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
123
  const tgba_bdd_dict&
124
125
126
127
  tgba_bdd_translate_proxy::get_dict() const
  {
    return to_;
  }
Alexandre Duret-Lutz's avatar
typo    
Alexandre Duret-Lutz committed
128

129
130
131
132
133
134
135
136
137
138
  std::string
  tgba_bdd_translate_proxy::format_state(const state* state) const
  {
    const state_bdd* s = dynamic_cast<const state_bdd*>(state);
    assert(s);
    return bdd_format_set(to_, s->as_bdd());
  }


}