// Unified token -*- c++ -*-

#ifndef TOKEN_H_
# define TOKEN_H_
# ifdef __GNUC__
#  pragma interface
# endif // __GNUC__

/** @file Token.h
 * Tokens used in the unification process
 */

/* Copyright  1999-2003 Marko Mkel (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA 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 2, or (at your option)
   any later version.

   MARIA 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.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

# include "GlobalMarking.h"
# include "Marking.h"
# include "s_list.h"

/** List of tokens to be unified */
struct unif
{
  /** next token */
  struct unif* next;
  /** variables that are bound from this token */
  class VariableSet* vars;
  /** flag: does the token have variable multiplicity? */
  bool varMult;
  /** index of the input place in the net */
  unsigned place;
  /** the token */
  const class Marking* m;
  /** flag: is the token multiset-valued? */
  bool isSet;
};

/** Unified token */
class Token
{
  typedef PlaceMarking::iterator iterator;
  typedef PlaceMarking::const_iterator const_iterator;

public:
  /** Constructor
   * @param cardinality		cardinality of the token
   * @param placeMarking	the PlaceMarking containing the actual token(s)
   * @param unifier		unification structure
   */
  Token (card_t cardinality,
	 class PlaceMarking& placeMarking,
	 const struct unif& unifier) :
    myIsReserved (false), myCardinality (cardinality),
    myPlaceMarking (placeMarking), myValue (0), myUnifier (unifier),
    myIterator (placeMarking.begin ()), myUnifiedUndefined (0)
  {
    assert (myCardinality > 0);
    assert (myUnifier.isSet || !myPlaceMarking.empty ());
  }
private:
  /** Copy constructor */
  Token (const class Token& old);
  /** Assignment operator */
  class Token& operator= (const class Token& old);
public:
  /** Destructor */
  ~Token ();

  /** Get the unification structure */
  const struct unif& getUnifier () const { return myUnifier; }

  /** Determine the cardinality of the actual token */
  card_t getCardinality () const { return myCardinality; }

  /** Find the next candidate for the concrete token
   * @return	true if a candidate was found
   */
  bool getConcrete () {
    assert (!myIsReserved);
    for (; myIterator != end (); myIterator++)
      if (myCardinality <= myPlaceMarking.getCount (myIterator))
	return true;
    return false;
  }

  /** Find the next candidate for the concrete token, disregarding multiplicity
   * @return	true if a candidate was found
   */
  bool getConcreteUnfold () {
    assert (!myIsReserved);
    return myIterator != end ();
  }

  /** Get the value of the concrete token candidate */
  const class Value& getValue () const {
    assert (myIterator != myPlaceMarking.end ());
    return PlaceMarking::getValue (myIterator);
  }

  /** Try to bind the token to a concrete token (and set myIterator to it)
   * @param valuation	the valuation to observe
   * @return		true if the token could be bound
   */
  bool isBindable (const class Valuation& valuation);

  /** Try to bind the token to a concrete token, disregarding multiplicity
   * @param valuation	the valuation to observe
   * @return		true if the token could be bound
   */
  bool isBindableUnfold (const class Valuation& valuation);

private:
  const_iterator begin () const { return myPlaceMarking.begin (); }
  const_iterator end () const { return myPlaceMarking.end (); }
  iterator begin () { return myPlaceMarking.begin (); }
  iterator end () { return myPlaceMarking.end (); }
public:

  /** Advance the iterator to the concrete tokens
   * @return	false if the iterator reached the end
   */
  bool next () {
    assert (!myIsReserved);
    assert (myIterator != end ());
    return ++myIterator != end ();
  }

  /** Determine whether the token has been bound to a concrete token */
  bool isReserved () const { return myIsReserved; }
  /** Bind the token to a concrete token */
  void reserve () {
    assert (!myIsReserved);
    if (myValue)
      myPlaceMarking -= *myValue;
    else
      myPlaceMarking.reserve (myIterator, myCardinality);
    myIsReserved = true;
  }
  /** Remove the reservation (binding) of the concrete token */
  void free () {
    assert (myIsReserved);
    if (myValue) {
      if (!myPlaceMarking.add (*myValue, 1))
	assert (false);
    }
    else
      myPlaceMarking.free (myIterator, myCardinality);
    myIsReserved = false;
  }
  /** Undefine the variables that were unified from this token
   * @param valuation	the valuation where the variables are defined
   */
  void undefine (class Valuation& valuation);

  /** Set the "reserved" status (needed by the unfolding algorithm) */
  void setReservedUnfold (bool reserved) { myIsReserved = reserved; }
  /** Augment the collection of removed tokens
   * @param pm	the collection
   * @return	true if the operation succeeded
   */
  bool copyRemoved (class PlaceMarking& pm) const {
    assert (myIsReserved);
    return myValue
      ? pm.add (*myValue, 1)
      : pm.add (*PlaceMarking::getValue (myIterator).copy (), myCardinality);
  }

  /** Determine whether the valuations are compatible with the concrete tokens
   * @param valuation	the valuation to observe
   * @return		true if the token is compatible
   */
  bool isCompatible (const class Valuation& valuation) const {
    return myUnifier.m->getToken ()->isCompatible (getValue (), valuation);
  }

  /** Update the set of unified possibly undefined variables
   * @param valuation	the valuation to observe
   */
  void addUnified (const class Valuation& valuation);
  /** See if a possibly undefined variable is already unified */
  bool isUnified (const class VariableDefinition& var) const;
# ifndef NDEBUG
  /** Assert that the token can be popped from the stack */
  void assertPop () const {
    assert (this && myCardinality);
    assert (myUnifier.isSet || myIterator != myPlaceMarking.end ());
  }
  /** Assert that none of the variables to unify have values
   * @param valuation	the valuation to observe
   */
  void assertUndefined (const class Valuation& valuation) const;
  /** Assert that all of the variables to unify have values
   * @param valuation	the valuation to observe
   */
  void assertDefined (const class Valuation& valuation) const;
# endif // NDEBUG

private:
  /** Flag: has the token been reserved from the place? */
  bool myIsReserved;
  /** Cardinality of the actual token */
  card_t myCardinality;
  /** PlaceMarking to which the Token belongs */
  class PlaceMarking& myPlaceMarking;
  /** PlaceMarking to which the Token evaluates */
  class PlaceMarking* myValue;
  /** the unification structure */
  const struct unif& myUnifier;
  /** Iterator to the PlaceMarking */
  iterator myIterator;
  /** Previously unified possibly undefined variables */
  class VariableSet* myUnifiedUndefined;
};

/** List of unified tokens */
class TokenList
{
public:
  /** List of tokens */
  typedef slist<class Token*> List;
  /** Iterator to the list of tokens */
  typedef List::iterator iterator;
  /** Constant iterator to the list of tokens */
  typedef List::const_iterator const_iterator;

  /** Constructor */
  TokenList () : myList () {}
private:
  /** Copy constructor */
  TokenList (const class TokenList& old);
  /** Assignment operator */
  class TokenList& operator= (const class TokenList& old);
public:
  /** Destructor */
  ~TokenList () {
    for (iterator i = begin (); i != end (); i++)
      delete *i;
  }

  /** @name Accessors to the token list */
  /*@{*/
  bool empty () const { return myList.empty (); }
  size_t size () const { return myList.size (); }
  iterator begin () { return myList.begin (); }
  iterator end () { return myList.end (); }
  const_iterator begin () const { return myList.begin (); }
  const_iterator end () const { return myList.end (); }

  void insert (class Token& token) { myList.push_front (&token); }
  void clear () {
    for (iterator i = begin (); i != end (); i++)
      delete *i;
    myList.clear ();
  }
  /*@}*/

  /** Peek at the topmost token on the stack */
  const class Token& top () const {
    assert (!empty ());
    return **begin ();
  }
  /** Pop a token from the stack */
  class Token& pop () {
    assert (!empty ());
    iterator i = begin (); class Token* token = *i; myList.erase (i);
#ifndef NDEBUG
    token->assertPop ();
#endif // NDEBUG
    return *token;
  }
  /** Push a token to the stack */
  void push (class Token& token) {
    myList.push_front (&token);
  }

  /** Determine whether the valuations are compatible with the concrete tokens
   * @param valuation	the valuation to observe
   * @return		true if all tokens are compatible
   */
  bool isCompatible (const class Valuation& valuation) const {
    for (const_iterator i = begin (); i != end (); i++)
      if (!(*i)->isCompatible (valuation))
	return false;
    return true;
  }

private:
  /** The list of tokens */
  List myList;
};

#endif // TOKEN_H_