// Global marking (PlaceMarking for each place) -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "GlobalMarking.h"
#include "Net.h"
#include "Place.h"
#include "Valuation.h"
#include "Marking.h"
#include "LeafValue.h"

#include <assert.h>

/** @file GlobalMarking.C
 * Assignment of markings for each place
 */

/* 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. */

GlobalMarking::GlobalMarking (const class Net& net) :
#ifndef NDEBUG
  myNet (net),
#endif // NDEBUG
  myErroneous (false),
  mySize (net.getNumPlaces ()),
  myPlaceMarkings (mySize ? new class PlaceMarking[mySize] : 0)
{
  for (unsigned i = mySize; i--; )
    myPlaceMarkings[i].setPlace (net.getPlace (i));
}

GlobalMarking::GlobalMarking (const class GlobalMarking& old) :
#ifndef NDEBUG
  myNet (old.myNet),
#endif // NDEBUG
  myErroneous (old.myErroneous),
  mySize (old.mySize),
  myPlaceMarkings (mySize ? new class PlaceMarking[mySize] : 0)
{
  for (unsigned i = 0; i < mySize; i++)
    myPlaceMarkings[i] = old.myPlaceMarkings[i];
}

class GlobalMarking&
GlobalMarking::operator= (const class GlobalMarking& old)
{
  assert (&myNet == &old.myNet);
  assert (mySize == old.mySize);
  myErroneous = old.myErroneous;
  for (unsigned i = 0; i < mySize; i++)
    myPlaceMarkings[i] = old.myPlaceMarkings[i];
  return *this;
}

GlobalMarking::~GlobalMarking ()
{
  delete[] myPlaceMarkings;
}

class PlaceMarking&
GlobalMarking::operator[] (const class Place& place)
{
  assert (place.getIndex () < mySize);
  return myPlaceMarkings[place.getIndex ()];
}

bool
GlobalMarking::encode (class BitPacker& buf,
		       const class GlobalMarking& m0,
		       card_t* errorplace) const
{
  // Clear the encoding buffer
  buf.clear ();
  /** Valuation for checking the consistency of implicit places */
  class Valuation valuation;
  valuation.setGlobalMarking (this);
  // Encode each place marking in the global marking
  for (card_t i = mySize; i--; ) {
    /** Current place marking */
    const class PlaceMarking& place = (*this)[i];
    if (!place.getPlace ())
      continue;
    if (place.getPlace ()->isConstant ()
	? m0[i] == place
	: place.encode (buf, &valuation))
      continue;
    if (errorplace) *errorplace = i;
    return false;
  }

  // the buffer must not be empty
  if (!buf.getNumBytes ())
    buf.append (0, 1);

  return true;
}

void
GlobalMarking::encode (class BitPacker& buf,
		       const class Net& net) const
{
  assert (net.getParent () == &myNet);
  assert (net.getNumPlaces () <= mySize);

  // Clear the encoding buffer
  buf.clear ();

  for (card_t i = net.getNumPlaces (); i--; ) {
    if (const class Place* place = net.getPlace (i)) {
      if (!place->isConstant () &&
	  !(*this)[i].encode (buf, 0))
	assert (false); // this GlobalMarking should have been valid
    }
  }

  // the buffer must not be empty
  if (!buf.getNumBytes ())
    buf.append (0, 1);
}

unsigned
GlobalMarking::decode (const class GlobalMarking& m0,
		       const word_t* data,
		       unsigned propBits)
{
  card_t i;
  class BitUnpacker buf (data);
  // Decode each place marking in the global marking
  for (i = mySize; i--; ) {
    class PlaceMarking& p = (*this)[i];
    if (p.getPlace ())
      p.decode (buf);
  }
  computeImplicit (m0);
  return propBits ? buf.extract (propBits) : 0;
}

void
GlobalMarking::decode (const class Net& net,
		       const word_t* data)
{
  assert (net.getParent () == &myNet);
  assert (net.getNumPlaces () <= mySize);
  class BitUnpacker buf (data);
  for (card_t i = net.getNumPlaces (); i--; ) {
    class PlaceMarking& p = (*this)[i];
    if (net.getPlace (i)) {
      p.clear ();
      p.decode (buf);
    }
  }
  computeImplicit (*net.getParent ()->getInitMarking ());
}

void
GlobalMarking::computeImplicit (const class GlobalMarking& m0)
{
  class Valuation valuation;
  valuation.setGlobalMarking (this);
  for (card_t i = 0; i < mySize; i++) {
    class PlaceMarking& p = (*this)[i];
    if (const class Place* place = p.getPlace ()) {
      if (place->isConstant ())
	p = m0[i];
      else if (place->isImplicit ()) {
	const class Marking* expr = place->getInitMarking ();
	assert (!!expr);
	p.clear ();
	if (!expr->add (p, 1, valuation))
	  assert (false);
      }
    }
  }
}

bool
GlobalMarking::eval (const class Expression& cond) const
{
  class Valuation valuation;
  valuation.setGlobalMarking (this);
  bool holds = false;
  if (class Value* value = cond.eval (valuation)) {
    assert (value->getKind () == Value::vLeaf);
    assert (valuation.isOK ());
    holds = bool (static_cast<class LeafValue&>(*value));
    delete value;
  }
  return holds;
}

#include "Printer.h"
void
GlobalMarking::display (const class Printer& printer) const
{
  printer.printRaw (isErroneous () ? "erroneous state " : "state ");
  printer.delimiter ('(')++;

  for (unsigned i = 0; i < mySize; i++) {
    assert (myPlaceMarkings[i].getPlace () ||
	    myPlaceMarkings[i].empty ());
    if (!myPlaceMarkings[i].empty () &&
	!myPlaceMarkings[i].getPlace ()->isSuppressed ()) {
      printer.linebreak ();
      myPlaceMarkings[i].display (printer);
    }
  }

  printer--.linebreak ();
  printer.delimiter (')');
}