// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
// Développement 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_SUCCITER_HH
# define SPOT_TGBA_SUCCITER_HH

#include "state.hh"

namespace spot
{
  class tgba;

  /// \ingroup tgba_essentials
  /// \brief Iterate over the successors of a state.
  ///
  /// This class provides the basic functionalities required to
  /// iterate over the successors of a state, as well as querying
  /// transition labels.  Because transitions are never explicitely
  /// encoded, labels (conditions and acceptance conditions) can only
  /// be queried while iterating over the successors.
  class SPOT_API tgba_succ_iterator
  {
  public:
    virtual
    ~tgba_succ_iterator()
    {
    }

    /// \name Iteration
    //@{

    /// \brief Position the iterator on the first successor (if any).
    ///
    /// This method can be called several times to make multiple
    /// passes over successors.
    ///
    /// \warning One should always call \c done() (or better: check
    /// the return value of first()) to ensure there is a successor,
    /// even after \c first().  A common trap is to assume that there
    /// is at least one successor: this is wrong.
    ///
    /// \return whether there is actually a successor
    virtual bool first() = 0;

    /// \brief Jump to the next successor (if any).
    ///
    /// \warning Again, one should always call \c done() (or better:
    /// check the return value of next()) ensure there is a successor.
    ///
    /// \return whether there is actually a successor
    virtual bool next() = 0;

    /// \brief Check whether the iteration is finished.
    ///
    /// This function should be called after any call to \c first()
    /// or \c next() and before any enquiry about the current state.
    ///
    /// The usual way to do this is with a \c for loop.
    ///
    ///     for (s->first(); !s->done(); s->next())
    ///       ...
    virtual bool done() const = 0;

    //@}

    /// \name Inspection
    //@{

    /// \brief Get the state of the current successor.
    ///
    /// Note that the same state may occur at different points
    /// in the iteration.  These actually correspond to the same
    /// destination.  It just means there were several transitions,
    /// with different conditions, leading to the same state.
    ///
    /// The returned state should be destroyed (see state::destroy)
    /// by the caller after it is no longer used.
    virtual state* current_state() const = 0;
    /// \brief Get the condition on the transition leading to this successor.
    ///
    /// This is a boolean function of atomic propositions.
    virtual bdd current_condition() const = 0;
    /// \brief Get the acceptance conditions on the transition leading
    /// to this successor.
    virtual bdd current_acceptance_conditions() const = 0;

    //@}
  };

  namespace internal
  {
    struct SPOT_API succ_iterator
    {
    protected:
      tgba_succ_iterator* it_;
    public:

      succ_iterator(tgba_succ_iterator* it):
	it_(it)
      {
      }

      bool operator==(succ_iterator o) const
      {
	return it_ == o.it_;
      }

      bool operator!=(succ_iterator o) const
      {
	return it_ != o.it_;
      }

      const tgba_succ_iterator* operator*() const
      {
	return it_;
      }

      void operator++()
      {
	if (!it_->next())
	  it_ = nullptr;
      }
    };
  }
}


#endif // SPOT_TGBA_SUCCITER_HH