// Place marking class -*- c++ -*-

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

# include "Value.h"
# include <map>
#include <cstddef>

/** @file PlaceMarking.h
 * Assignment of a place to a multi-set
 */

/* Copyright  1999-2002 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. */

/** Place marking */
class PlaceMarking
{
public:
  /** Comparison operator for values */
  struct vcmp
  {
    /** Less-than comparison */
    bool operator() (const class Value* v1, const class Value* v2) const {
      return *v1 < *v2;
    }
  };
  /** The marking, mapping token values to non-zero multiplicities */
  typedef std::map<class Value*,card_t,struct vcmp> TokenMap;
  /** Iterator to the token map */
  typedef TokenMap::iterator iterator;
  /** Constant iterator to the token map */
  typedef TokenMap::const_iterator const_iterator;

  /** (cardinality,value) pair for sort () */
  class card_value
  {
  public:
    /** Default constructor */
    card_value () : card (0), value (0) {}
    /** Constructor
     * @param c		cardinality
     * @param v		value
     */
    card_value (card_t c, const class Value* v) : card (c), value (v) {
      assert (c && v);
    }
    /** Copy constructor */
    card_value (const class card_value& other) :
      card (other.card), value (other.value) {}
    /** Assignment operator */
    class card_value& operator= (const class card_value& other) {
      card = other.card; value = other.value; return *this;
    }
    /** Destructor */
    ~card_value () {}
    /** Three-way comparison
     * @param v1	first object
     * @param v2	second object
     * @return		less than, equal to, or greater than zero
     */
    static int cmp (const class card_value& v1,
		    const class card_value& v2) {
      return v1.card - v2.card;
    }
    /** Cardinality */
    card_t card;
    /** Value */
    const class Value* value;
  };

  /** Constructor */
  PlaceMarking () :
    myPlace (NULL),
# ifndef NDEBUG
    myType (NULL),
# endif // NDEBUG
    myTokens () {}
  /** Copy constructor */
  explicit PlaceMarking (const class PlaceMarking& old) :
    myPlace (old.myPlace),
# ifndef NDEBUG
    myType (old.myType),
# endif // NDEBUG
    myTokens () {
    for (const_iterator i = old.begin (); i != old.end (); i++)
      if (i->second)
	myTokens.insert (TokenMap::value_type (i->first->copy (), i->second));
  }
  /** Assignment operator */
  class PlaceMarking& operator= (const class PlaceMarking& other) {
    assert (!myPlace || myPlace == other.myPlace);
    myPlace = other.myPlace;
    assert (!myType || myType == other.myType);
#ifndef NDEBUG
    myType = other.myType;
#endif // NDEBUG
    clear ();
    for (const_iterator i = other.myTokens.begin ();
	 i != other.myTokens.end (); i++)
      if (i->second)
	myTokens.insert (TokenMap::value_type (i->first->copy (), i->second));
    return *this;
  }
  /** Destructor */
  ~PlaceMarking () {
    for (const_iterator i = begin (); i != end (); i++)
      delete i->first;
  }

  /** Determine the Place associated with the PlaceMarking */
  const class Place* getPlace () const { return myPlace; }

# ifndef NDEBUG
  /** Set the Place associated with the PlaceMarking
   * @param place	The place whose marking this is
   */
  void setPlace (const class Place* place);

  /** Set the Type associated with the PlaceMarking
   * @param type	The type of this marking
   */
  void setType (const class Type* type);

  /** Determine the Type associated with the PlaceMarking
   */
  const class Type* getType () const { return myType; }
# else // NDEBUG
  void setPlace (const class Place* place) { myPlace = place; }
# endif // NDEBUG

  /** Get the value of tokens pointed by an iterator
   * @param i	an iterator pointing to the value
   */
  static const class Value& getValue (const_iterator i) {
    return *i->first;
  }
  /** Get the number of tokens having the specified value
   * @param i	an iterator pointing to the value
   */
  static card_t getCount (const_iterator i) {
    return i->second;
  }
  /** Set the number of tokens having the specified value
   * @param i	an iterator pointing to the value
   * @param cnt	new count
   */
  void setCount (iterator i, card_t cnt) {
    assert (i != end ());
    assert (i->first && i->second);
    i->second = cnt;
  }

  /** Accessors to the token map */
  /*@{*/
  const_iterator begin () const { return myTokens.begin (); }
  const_iterator end () const { return myTokens.end (); }
  iterator begin () { return myTokens.begin (); }
  iterator end () { return myTokens.end (); }
  const_iterator find (const class Value* value) const {
    return myTokens.find (const_cast<class Value*>(value));
  }
  iterator find (const class Value* value) {
    return myTokens.find (const_cast<class Value*>(value));
  }
  size_t size () const { return myTokens.size (); }
  bool empty () const { return myTokens.empty (); }
  void clear () {
    for (const_iterator i = begin (); i != end (); i++)
      delete i->first;
    myTokens.clear ();
  }
  /*@}*/

  /** Equality comparison
   * @param other	multi-set to be compared with
   * @return		true if the multi-sets are equal
   */
  bool operator== (const class PlaceMarking& other) const {
    const_iterator i, j;
    assert (getType () == other.getType () || empty () || other.empty ());
    for (i = begin (), j = other.begin ();
	 i != end () && j != other.end ();
	 i++, j++) {
      if (!i->second) while (++i != end ()) if (i->second) break;
      if (!j->second) while (++j != other.end ()) if (j->second) break;
      if (i == end () || j == other.end ()) break;
      assert (i->first && j->first);
      if (j->second != i->second || !(*j->first == *i->first))
	return false;
    }
    if (i != end () && !i->second)
      while (++i != end ())
	if (i->second) break;
    if (j != other.end () && !j->second)
      while (++j != other.end ())
	if (j->second) break;
    return i == end () && j == other.end ();
  }

  /** Subset comparison
   * @param other	a superset candidate
   * @return		true if this is a subset of other
   */
  bool operator<= (const class PlaceMarking& other) const {
    assert (getType () == other.getType () || empty () || other.empty ());
    const_iterator i = begin (), j;
    if (i == end ())
      return true;
    for (j = other.begin (); j != other.end (); j++) {
      if (!i->second) {
	while (++i != end ()) if (i->second) break;
	if (i == end ()) return true;
      }
      if (!j->second) {
	while (++j != other.end ()) if (j->second) break;
	if (j == other.end ()) break;
      }
      assert (i->first && j->first);
      if (*i->first < *j->first)
	return false;
      else if (*j->first < *i->first);
      else if (j->second < i->second)
	return false;
      else if (++i == end ())
	return true;
    }
    if (!i->second)
      while (++i != end ()) if (i->second) break;
    return i == end ();
  }
  /** Subset comparison, ignoring multiplicities
   * @param other	a superset candidate
   * @return		true if this is a subset of other
   */
  bool isSubset (const class PlaceMarking& other) const {
    assert (getType () == other.getType () || empty () || other.empty ());
    const_iterator i = begin (), j;
    if (i == end ())
      return true;
    for (j = other.begin (); j != other.end (); j++) {
      if (!i->second) {
	while (++i != end ()) if (i->second) break;
	if (i == end ()) return true;
      }
      if (!j->second) {
	while (++j != other.end ()) if (j->second) break;
	if (j == other.end ()) break;
      }
      assert (i->first && j->first);
      if (*i->first < *j->first)
	return false;
      else if (*j->first < *i->first);
      else if (++i == end ())
	return true;
    }
    if (!i->second)
      while (++i != end ()) if (i->second) break;
    return i == end ();
  }
  /** Multiset intersection
   * @param other	a set to be intersected with this
   * @return		the intersection
   */
  class PlaceMarking& operator&= (const class PlaceMarking& other) {
    assert (getType () == other.getType () || other.empty ());
    iterator i;
    const_iterator j;
    for (j = other.begin (); j != other.end (); j++)
      if (j->second && (i = find (j->first)) != end () && i->second)
	if (i->second > j->second)
	  i->second = j->second;
    for (i = begin (); i != end (); i++)
      if (i->second && (j = other.find (i->first)) == other.end ())
	i->second = 0;
    return *this;
  }
  /** Multiset difference
   * @param other	a set to be subtracted from this
   * @return		the difference
   */
  class PlaceMarking& operator-= (const class PlaceMarking& other) {
    assert (getType () == other.getType () || other.empty ());
    iterator i;
    const_iterator j;
    for (j = other.begin (); j != other.end (); j++) {
      if (j->second && (i = find (j->first)) != end () && i->second) {
	if (i->second > j->second)
	  i->second -= j->second;
	else
	  i->second = 0;
      }
    }
    return *this;
  }
  /** Multiset union (or sum)
   * @param other	a set to be added to this
   * @param count	token multiplier
   * @return		whether the operation this+=count*other succeeded
   */
  bool add (const class PlaceMarking& other,
	    card_t count) {
    assert (getType () == other.getType () || other.empty ());
    assert (count > 0);
    for (const_iterator j = other.begin (); j != other.end (); j++) {
      card_t p = j->second;
      if (!p) continue;
      if (p >= CARD_T_MAX / count)
	return false;
      p *= count;
      class Value* v = j->first->copy ();
      std::pair<iterator,bool> result =
	myTokens.insert (TokenMap::value_type (v, p));
      if (!result.second) {
	delete v;
	if (p >= CARD_T_MAX - result.first->second)
	  return false;
	result.first->second += p;
      }
    }
    return true;
  }

  /** Set union (initialize all non-zero multiplicities to 1)
   * @param other	a set to be added to this
   */
  void setUnion (const class PlaceMarking& other) {
    assert (getType () == other.getType () || other.empty ());
    for (const_iterator j = other.begin (); j != other.end (); j++) {
      if (!j->second) continue;
      class Value* v = j->first->copy ();
      std::pair<iterator,bool> result =
	myTokens.insert (TokenMap::value_type (v, 1));
      if (!result.second) {
	delete v;
	result.first->second = 1;
      }
    }
  }

  /** Add a number of specified tokens to the place marking.
   * @param value	Value of the tokens
   * @param amount	Number of tokens to be added
   * @return		false on cardinality overflow; normally true
   */
  bool add (class Value& value, card_t amount);

  /** Remove a number of specified tokens from the place marking.
   * @param value	Value of the tokens
   * @param amount	Number of tokens to be removed
   */
  void remove (const class Value& value, card_t amount);

  /** Remove a value from the place marking
   * @param i		Iterator to the value to be removed
   */
  void remove (iterator i) {
    assert (i != end () && i->second);
    i->second = 0;
  }

  /** Reserve a number of tokens having the specified value.
   * @param i		Iterator to the value to be reserved
   * @param amount	Amount of tokens to reserve
   */
  void reserve (iterator i, card_t amount) {
    assert (i != end () && amount > 0);
    assert (i->second >= amount);
    i->second -= amount;
  }

  /** Free a number of previously reserved tokens
   * @param i		Iterator to the value to be freed
   * @param amount	Amount of tokens to be freed
   */
  void free (iterator i, card_t amount) {
    assert (i != end () && amount > 0);
    assert (i->second <= CARD_T_MAX - amount);
    i->second += amount;
  }

  /** Encode this marking
   * @param buf		buffer to receive the encoded marking
   * @param valuation	valuation for verifying implicit places (optional)
   * @return		false in case of an integrity violation
   */
  bool encode (class BitPacker& buf,
	       const class Valuation* valuation) const;

  /** Decode a marking to this
   * @param buf		buffer containing the encoded marking
   */
  void decode (class BitUnpacker& buf);

  /** Display this object
   * @param printer	The printer object
   */
  void display (const class Printer& printer) const;

  /** Sort the distinct values of the marking by multiplicity
   * @param histogram	size()-element array for the results
   * @return		total cardinality of the marking; CARD_T_MAX=overflow
   */
  card_t sort (class card_value* histogram) const;

private:
  /** The place */
  const class Place* myPlace;
# ifndef NDEBUG
  /** The type */
  const class Type* myType;
# endif // NDEBUG
  /** The tokens */
  TokenMap myTokens;
};

#endif // PLACEMARKING_H_