tgbaproxy.cc 1.96 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
// Développement de l'Epita (LRDE).
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#include "tgbaproxy.hh"

namespace spot
{
24
  tgba_proxy::tgba_proxy(const const_twa_ptr& original)
25
    : twa(original->get_dict()), original_(original)
26 27
  {
    get_dict()->register_all_variables_of(original, this);
28
    acc_.add_sets(original->acc().num_sets());
29 30 31 32 33 34 35 36 37 38 39 40
  }

  tgba_proxy::~tgba_proxy()
  {
    get_dict()->unregister_all_my_variables(this);
  }

  state* tgba_proxy::get_init_state() const
  {
    return original_->get_init_state();
  }

41
  twa_succ_iterator*
42
  tgba_proxy::succ_iter(const state* state) const
43
  {
44 45 46 47 48
    if (iter_cache_)
      {
	original_->release_iter(iter_cache_);
	iter_cache_ = nullptr;
      }
49
    return original_->succ_iter(state);
50 51 52 53 54 55 56 57 58
  }

  std::string
  tgba_proxy::format_state(const state* state) const
  {
    return original_->format_state(state);
  }

  std::string
59
  tgba_proxy::transition_annotation(const twa_succ_iterator* t) const
60 61 62 63 64
  {
    return original_->transition_annotation(t);
  }

  state*
65
  tgba_proxy::project_state(const state* s, const const_twa_ptr& t) const
66 67 68 69 70 71 72 73 74 75
  {
    return original_->project_state(s, t);
  }

  bdd
  tgba_proxy::compute_support_conditions(const state* state) const
  {
    return original_->support_conditions(state);
  }
}