tgtaproduct.cc 6.45 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2014-2018 Laboratoire de Recherche et Développement de
3
// 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


//#define TRACE

23
#include "config.h"
24 25 26 27 28 29 30
#include <iostream>
#ifdef TRACE
#define trace std::clog
#else
#define trace while (0) std::clog
#endif

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

namespace spot
{

  ////////////////////////////////////////////////////////////
41
  // tgta_succ_iterator_product
42 43 44


  ////////////////////////////////////////////////////////////
45
  // tgta_product
46

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

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

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

67 68
    fixed_size_pool<pool_type::Safe>* p =
      const_cast<fixed_size_pool<pool_type::Safe>*> (&pool_);
69

70 71 72
    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);
73 74 75
  }

  ////////////////////////////////////////////////////////////
76 77
  // tgbtgta_succ_iterator_product
  tgta_succ_iterator_product::tgta_succ_iterator_product(
78 79
      const state_product* s,
      const const_kripke_ptr& k, const const_tgta_ptr& t,
80
      fixed_size_pool<pool_type::Safe>* pool)
81
    : source_(s), tgta_(t), kripke_(k), pool_(pool)
82 83
  {

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

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

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

110
    tgta_init_state->destroy();
111
    current_state_ = nullptr;
112 113
  }

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

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

  void
140
  tgta_succ_iterator_product::next_kripke_dest()
141 142 143 144
  {
    if (!kripke_succ_it_)
      return;

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

    // If one of the two successor sets is empty initially, we reset
157 158 159
    // 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().)
160 161 162
    if (kripke_succ_it_->done())
      {
        delete kripke_succ_it_;
163
        kripke_succ_it_ = nullptr;
164 165 166
        return;
      }

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

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

  }

179
  bool
180
  tgta_succ_iterator_product::first()
181 182 183
  {

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

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

    step_();

196
    trace << "*** next() .... if(done()) = ***" << done() << std::endl;
197

198
    return find_next_succ_();
199 200
  }

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

        step_();
      }
218
    return false;
219 220 221
  }

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

  }

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

  bdd
244
  tgta_succ_iterator_product::cond() const
245 246 247 248
  {
    return current_condition_;
  }

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

}