tgtaproduct.cc 6.31 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2014, 2015 Laboratoire de Recherche et
// Développement de l Epita (LRDE).
4
5
6
7
8
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19
20
21
22
23
24
25
26
27
28
29


//#define TRACE

#include <iostream>
#ifdef TRACE
#define trace std::clog
#else
#define trace while (0) std::clog
#endif

30
#include "tgtaproduct.hh"
31
32
33
34
35
36
37
38
39
#include <string>
#include <cassert>
#include "misc/hashfunc.hh"
#include "kripke/kripke.hh"

namespace spot
{

  ////////////////////////////////////////////////////////////
40
  // tgta_succ_iterator_product
41
42
43


  ////////////////////////////////////////////////////////////
44
  // tgta_product
45

46
47
  tgta_product::tgta_product(const const_kripke_ptr& left,
			     const const_tgta_ptr& right):
48
    twa_product(left, right)
49
50
51
  {
  }

52
  const state*
53
  tgta_product::get_init_state() const
54
55
56
57
58
59
  {
    fixed_size_pool* p = const_cast<fixed_size_pool*> (&pool_);
    return new (p->allocate()) state_product(left_->get_init_state(),
        right_->get_init_state(), p);
  }

60
  twa_succ_iterator*
61
  tgta_product::succ_iter(const state* state) const
62
  {
63
    const state_product* s = down_cast<const state_product*> (state);
64
65
66
67
    assert(s);

    fixed_size_pool* p = const_cast<fixed_size_pool*> (&pool_);

68
69
70
    auto l = std::static_pointer_cast<const kripke>(left_);
    auto r = std::static_pointer_cast<const tgta>(right_);
    return new tgta_succ_iterator_product(s, l, r, p);
71
72
73
  }

  ////////////////////////////////////////////////////////////
74
75
  // tgbtgta_succ_iterator_product
  tgta_succ_iterator_product::tgta_succ_iterator_product(
76
77
      const state_product* s,
      const const_kripke_ptr& k, const const_tgta_ptr& t,
78
79
      fixed_size_pool* pool)
    : source_(s), tgta_(t), kripke_(k), pool_(pool)
80
81
  {

82
    const state* tgta_init_state = tgta_->get_init_state();
83
    if ((s->right())->compare(tgta_init_state) == 0)
84
      source_ = nullptr;
85

86
    if (!source_)
87
      {
88
        kripke_succ_it_ = nullptr;
89
90
91
        kripke_current_dest_state = kripke_->get_init_state();
        current_condition_
            = kripke_->state_condition(kripke_current_dest_state);
92
93
94
        tgta_succ_it_ = tgta_->succ_iter_by_changeset(
            tgta_init_state, current_condition_);
        tgta_succ_it_->first();
95
        trace
96
          << "*** tgta_succ_it_->done() = ***" << tgta_succ_it_->done()
97
98
99
100
101
102
103
              << std::endl;

      }
    else
      {
        kripke_source_condition = kripke_->state_condition(s->left());
        kripke_succ_it_ = kripke_->succ_iter(s->left());
104
105
        kripke_current_dest_state = nullptr;
        tgta_succ_it_ = nullptr;
106
107
      }

108
    tgta_init_state->destroy();
109
    current_state_ = nullptr;
110
111
  }

112
  tgta_succ_iterator_product::~tgta_succ_iterator_product()
113
114
  {
    // ta_->free_state(current_state_);
115
    if (current_state_)
116
      current_state_->destroy();
117
    current_state_ = nullptr;
118
    delete tgta_succ_it_;
119
    delete kripke_succ_it_;
120
    if (kripke_current_dest_state)
121
122
123
124
      kripke_current_dest_state->destroy();
  }

  void
125
  tgta_succ_iterator_product::step_()
126
  {
127
128
129
    if (!tgta_succ_it_->done())
      tgta_succ_it_->next();
    if (tgta_succ_it_->done())
130
      {
131
        delete tgta_succ_it_;
132
        tgta_succ_it_ = nullptr;
133
134
135
136
137
        next_kripke_dest();
      }
  }

  void
138
  tgta_succ_iterator_product::next_kripke_dest()
139
140
141
142
  {
    if (!kripke_succ_it_)
      return;

143
    if (!kripke_current_dest_state)
144
145
146
147
148
149
      {
        kripke_succ_it_->first();
      }
    else
      {
        kripke_current_dest_state->destroy();
150
        kripke_current_dest_state = nullptr;
151
152
153
154
        kripke_succ_it_->next();
      }

    // If one of the two successor sets is empty initially, we reset
155
156
157
    // kripke_succ_it_, so that done() can detect this situation
    // easily.  (We choose to reset kripke_succ_it_ because this
    // variable is already used by done().)
158
159
160
    if (kripke_succ_it_->done())
      {
        delete kripke_succ_it_;
161
        kripke_succ_it_ = nullptr;
162
163
164
        return;
      }

165
    kripke_current_dest_state = kripke_succ_it_->dst();
166
167
168
169
170
    bdd kripke_current_dest_condition = kripke_->state_condition(
        kripke_current_dest_state);

    current_condition_ = bdd_setxor(kripke_source_condition,
        kripke_current_dest_condition);
171
    tgta_succ_it_ = tgta_->succ_iter_by_changeset(source_->right(),
172
        current_condition_);
173
    tgta_succ_it_->first();
174
175
176

  }

177
  bool
178
  tgta_succ_iterator_product::first()
179
180
181
  {

    next_kripke_dest();
182
183
    trace << "*** first() .... if(done()) = ***" << done() << std::endl;
    return find_next_succ_();
184
185
  }

186
  bool
187
  tgta_succ_iterator_product::next()
188
189
  {
    current_state_->destroy();
190
    current_state_ = nullptr;
191
192
193

    step_();

194
    trace << "*** next() .... if(done()) = ***" << done() << std::endl;
195

196
    return find_next_succ_();
197
198
  }

199
  bool
200
  tgta_succ_iterator_product::find_next_succ_()
201
202
203
  {
    while (!done())
      {
204
        if (!tgta_succ_it_->done())
205
206
207
          {
            current_state_ = new (pool_->allocate()) state_product(
                kripke_current_dest_state->clone(),
208
                tgta_succ_it_->dst(), pool_);
209
            current_acceptance_conditions_
210
	      = tgta_succ_it_->acc();
211
            return true;
212
213
214
215
          }

        step_();
      }
216
    return false;
217
218
219
  }

  bool
220
  tgta_succ_iterator_product::done() const
221
  {
222
    if (!source_)
223
      {
224
        return !tgta_succ_it_ || tgta_succ_it_->done();
225
226
227
228
229
230
231
232
233
      }
    else
      {
        return !kripke_succ_it_ || kripke_succ_it_->done();
      }

  }

  state_product*
234
  tgta_succ_iterator_product::dst() const
235
236
  {
    trace
237
      << "*** dst() .... if(done()) = ***" << done() << std::endl;
238
239
240
241
    return current_state_->clone();
  }

  bdd
242
  tgta_succ_iterator_product::cond() const
243
244
245
246
  {
    return current_condition_;
  }

247
  acc_cond::mark_t
248
  tgta_succ_iterator_product::acc() const
249
250
251
252
253
  {
    return current_acceptance_conditions_;
  }

}