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

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "PlaceMarking.h"
#include "Place.h"
#include "BitBuffer.h"
#include "Marking.h"
#include "CardType.h"

#include <assert.h>
#include <string.h>

/** @file PlaceMarking.C
 * 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. */

#ifndef NDEBUG
void
PlaceMarking::setPlace (const class Place* place)
{
  assert (!place || !myPlace);
  if (place)
    setType (&place->getType ());
  myPlace = place;
}

void
PlaceMarking::setType (const class Type* type)
{
  assert (!myPlace && !myType);
  myType = type;
}
#endif // NDEBUG

bool
PlaceMarking::add (class Value& value, card_t amount)
{
  assert (myType->isConstrained (value));
  assert (amount > 0);
  std::pair<iterator, bool> result =
    myTokens.insert (TokenMap::value_type (&value, amount));
  if (!result.second) {
    delete &value;
    if (amount >= CARD_T_MAX - result.first->second)
      return false;
    result.first->second += amount;
  }
  return true;
}

void
PlaceMarking::remove (const class Value& value, card_t amount)
{
  assert (myType->isConstrained (value));
  assert (amount > 0);
  iterator i = find (&value);
  assert (i != end ());
  assert (i->second >= amount);
  i->second -= amount;
}

bool
PlaceMarking::encode (class BitPacker& buf,
		      const class Valuation* valuation) const
{
  assert (myPlace && !myPlace->isConstant ());
  if (myPlace->isImplicit ()) {
    if (!valuation)
      return true;
    const class Marking* marking = myPlace->getInitMarking ();
    assert (!!marking);
    class PlaceMarking p;
    p.setPlace (myPlace);
    return marking->add (p, 1, *valuation) && p == *this;
  }

  /** Number of distinct tokens */
  size_t distinct = size ();
  /** Array of sorted cardinality,value pairs */
  class card_value* histogram = distinct ? new class card_value[distinct] : 0;
  /** Total cardinality */
  card_t total = distinct ? sort (histogram) : 0;

  if (total == CARD_T_MAX) {
  capacity:
    delete[] histogram;
    return false;
  }

  // Encode the total number of tokens
  if (const class Constraint* c = myPlace->getCapacity ()) {
    card_t n;
    if (!CardType::convert (n, total, *c))
      goto capacity;
    if (unsigned cap = myPlace->getCapacityBits ()) {
      if (cap > 2 && !myPlace->isNonempty ()) {
	if (!total)
	  goto empty;
	buf.append (1, 1);
      }
      buf.append (n, cap);
    }
    if (!total)
      goto none;
  }
  else {
    assert (!myPlace->isNonempty ());
    // variable-length code:
    // 0		0
    // 1..8		10xxx
    // 9..264		110xxxxxxxx
    // 265..65800	1110xxxxxxxxxxxxxxxx
    // 65801..		1111xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
    if (!total) {
    empty:
      buf.append (0, 1);
      goto none;
    }
    else {
      buf.append (1, 1);
      if (total <= 8)
	buf.append (0, 1), buf.append (total - 1, 3);
      else {
	buf.append (1, 1);
	if (total <= 8 + 256)
	  buf.append (0, 1), buf.append (total - (1 + 8), 8);
	else {
	  buf.append (1, 1);
	  if (total <= 8 + 256 + 65536)
	    buf.append (0, 1), buf.append (total - (1 + 8 + 256), 16);
	  else
	    buf.append (1, 1), buf.append (total, CARD_T_BIT);
	}
      }
    }
  }

  // Encode the number of distinct tokens
  assert (distinct && distinct <= total);
  if (total > 1)
    buf.append (distinct - 1, log2 (total));

  // Encode each distinct token in descending order of multiplicity
  while (distinct--) {
    // Encode the multiplicity (distinct has been decremented by one)
    assert (total >= distinct + 1);
    /** Lower multiplicity bound, inclusive */
    const card_t low = (total + distinct) / (distinct + 1);
    /** Higher multiplicity bound, inclusive */
    const card_t high = total - distinct;
    assert (low <= high);
    // Update the total cardinality of remaining tokens
    assert (total >= histogram[distinct].card);
    total -= histogram[distinct].card;

    assert (histogram[distinct].card >= low &&
	    histogram[distinct].card <= high);
    // Finally encode the multiplicity
    if (high != low)
      buf.append (histogram[distinct].card - low, log2 (high - low + 1));
    // Encode the value
    buf.append (*histogram[distinct].value);
  }

 none:
  assert (!total);
  delete[] histogram;
  return true;
}

void
PlaceMarking::decode (class BitUnpacker& buf)
{
  assert (!!myPlace);
  if (myPlace->isImplicit () || myPlace->isConstant ())
    return;
  /** Total cardinality */
  card_t total;

  // Decode the total number of tokens
  if (const class Constraint* c = myPlace->getCapacity ()) {
    if (unsigned cap = myPlace->getCapacityBits ()) {
      if (cap > 2 && !myPlace->isNonempty () && !buf.extract (1))
	return;
      total = CardType::convert (buf.extract (cap), *c);
    }
    else
      total = CardType::convert (0, *c);
    if (!total)
      return;
  }
  else {
    if (!buf.extract (1))		// 0: 0
      return;
    else if (!buf.extract (1))		// 10xxx: 1..8
      total = 1 + buf.extract (3);
    else if (!buf.extract (1))		// 110xxxxxxxx: 9..264
      total = (1 + 8) + buf.extract (8);
    else if (!buf.extract (1))		// 1110xxxxxxxxxxxxxxxx: 265..65800
      total = (1 + 8 + 256) + buf.extract (16);
    else {				// 1111...: 65801..
      total = buf.extract (CARD_T_BIT);
      assert (total > 8 + 256 + 65536);
    }
  }

  /** Number of distinct tokens */
  card_t distinct = total > 1 ? buf.extract (log2 (total)) + 1 : 1;

  // Decode each distinct token in descending order of multiplicity
  while (distinct--) {
    // Decode the multiplicity (distinct has been decremented by one)
    assert (total >= distinct + 1);
    /** Lower multiplicity bound, inclusive */
    const card_t low = (total + distinct) / (distinct + 1);
    /** Higher multiplicity bound, inclusive */
    const card_t high = total - distinct;
    assert (low <= high);
    /** Multiplicity */
    const card_t count = low != high
      ? buf.extract (log2 (high - low + 1)) + low
      : low;
    // Update the total cardinality of remaining tokens
    assert (total >= count);
    total -= count;

    // Decode the value
    if (!add (*buf.extract (myPlace->getType ()), count))
      assert (false);
  }

  assert (!total);
}

#include "Printer.h"
void
PlaceMarking::display (const class Printer& printer) const
{
  if (empty ())
    return;
  if (myPlace) {
    printer.print (myPlace->getName ());
    printer.delimiter (':')++;
  }
  bool comma = false;
  for (const_iterator i = myTokens.begin (); i != myTokens.end (); i++) {
    if (!i->second)
      continue;

    if (!comma) {
      if (myPlace)
	printer.linebreak ();
      comma = true;
    }
    else
      printer.delimiter (',');

    if (i->second > 1) {
      printer.print (i->second);
      printer.delimiter ('#');
    }
    i->first->display (printer);
  }
  if (myPlace)
    printer--;
}

card_t
PlaceMarking::sort (class PlaceMarking::card_value* histogram) const
{
  assert (histogram && !empty ());
  card_t total = 0;
  unsigned num = 0, pos = 0;
  for (const_iterator i = myTokens.begin ();
       i != myTokens.end ();
       i++, num++) {
    card_t card = i->second;
    if (!card) continue;
    if (total > CARD_T_MAX - card)
      return CARD_T_MAX;
    total += card;
    if (num) {
      for (unsigned low = 0, high = num; low != high; ) {
	pos = (low + high) >> 1;
	assert (pos < num && pos < high);
	if (histogram[pos].card > card)
	  high = pos;
	else if (++pos == high)
	  break;
	else {
	  assert (high > pos);
	  low = pos;
	}
      }
      memmove (histogram + pos + 1, histogram + pos,
	       (num - pos) * sizeof *histogram);
    }
    histogram[pos] = card_value (card, i->first);
  }
  assert (num == size ());
  return total;
}