// -*- coding: utf-8 -*-
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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/>.

#ifndef SPOT_TGBA_SUCCITERCONCRETE_HH
# define SPOT_TGBA_SUCCITERCONCRETE_HH

#include "statebdd.hh"
#include "succiter.hh"
#include "tgbabddcoredata.hh"

namespace spot
{
  /// A concrete iterator over successors of a TGBA state.
  /// \ingroup tgba_representation
  class SPOT_API tgba_succ_iterator_concrete:
    public tgba_succ_iterator
  {
  public:
    /// \brief Build a spot::tgba_succ_iterator_concrete.
    ///
    /// \param successors The set of successors with ingoing
    ///   conditions and acceptance conditions, represented as a BDD.
    ///   The job of this iterator will be to enumerate the
    ///   satisfactions of that BDD and split them into destination
    ///   states and conditions, and compute acceptance conditions.
    /// \param d The core data of the automata.
    ///   These contains sets of variables useful to split a BDD, and
    ///   compute acceptance conditions.
    tgba_succ_iterator_concrete(const tgba_bdd_core_data& d, bdd successors)
      : data_(d)
    {
      recycle(successors);
    }

    void recycle(bdd successors)
    {
      succ_set_ = successors;
      succ_set_left_ = successors;
      current_ = bddfalse;
    }

    virtual ~tgba_succ_iterator_concrete();

    // iteration
    bool first();
    bool next();
    bool done() const;

    // inspection
    state_bdd* current_state() const;
    bdd current_condition() const;
    bdd current_acceptance_conditions() const;

  private:
    const tgba_bdd_core_data& data_; ///< Core data of the automaton.
    bdd succ_set_;	///< The set of successors.
    bdd succ_set_left_;	///< Unexplored successors (including current_).
    bdd current_;	///< \brief Current successor, as a conjunction of
			///         atomic proposition and Next variables.
    bdd current_state_;	///< \brief Current successor, as a
			///         conjunction of Now variables.
    bdd current_acc_;   ///< \brief Acceptance conditions for the current
			///         transition.
  };
}

#endif // SPOT_TGBA_SUCCITERCONCRETE_HH