// Low-level net class -*- c++ -*-

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

# include <string.h>
# include <stdio.h>
# include <limits.h>
# include <map>
# include "BitBuffer.h"

/** @file LNet.h
 * Low-level (unfolded) net
 */

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

/** Low-level net class */
class LNet
{
public:
  /** Low-level arc */
  class LArc
  {
  public:
    /** Constructor */
    LArc () : myNumPlaces (0), myPlaces (0), myWeights (0) {}
    /** Copy constructor */
    LArc (const class LArc& old) :
      myNumPlaces (old.myNumPlaces), myPlaces (0), myWeights (0)
    {
      myPlaces = new unsigned[myNumPlaces];
      memcpy (myPlaces, old.myPlaces, myNumPlaces * sizeof *myPlaces);
      myWeights = new unsigned[myNumPlaces];
      memcpy (myWeights, old.myWeights, myNumPlaces * sizeof *myWeights);
    }
  private:
    /** Assignment operator */
    class LArc& operator= (const class LArc& old);
  public:
    /** Destructor */
    ~LArc () { delete[] myPlaces; delete[] myWeights; }
    /** Add a place to the arc
     * @param place	number of the place
     * @param weight	weight of the place
     * @return		true if the addition succeeded
     */
    bool add (unsigned place, unsigned weight) {
      for (unsigned i = myNumPlaces; i--; ) {
	if (myPlaces[i] == place) {
	  if (myWeights[i] >= UINT_MAX - weight)
	    return false;
	  myWeights[i] += weight;
	  return true;
	}
      }
      unsigned* p = new unsigned[myNumPlaces + 1];
      if (!p) return false;
      memcpy (p, myPlaces, myNumPlaces * sizeof *p);
      delete[] myPlaces; myPlaces = p;
      p = new unsigned[myNumPlaces + 1];
      if (!p) return false;
      memcpy (p, myWeights, myNumPlaces * sizeof *p);
      delete[] myWeights; myWeights = p;
      myPlaces[myNumPlaces] = place;
      myWeights[myNumPlaces++] = weight;
      return true;
    }
    /** Unfold a high-level arc
     * @param lnet	the low-level net
     * @param m		the high-level arc
     * @return		true if the operation succeeded
     */
    bool unfold (class LNet& lnet,
		 const class GlobalMarking& m);
    /** Read the arc from a file
     * @param f		the input stream
     * @return		true if the operation succeeded
     */
    bool read (FILE *f);
    /** Write the arc to a file
     * @param f		the output stream
     * @return		true if the operation succeeded
     */
    bool write (FILE *f) const;
    /** Get the number of places on the arc */
    unsigned getNumPlaces () const { return myNumPlaces; }
    /** Get the number of a place on the arc */
    unsigned getPlace (unsigned i) const { return myPlaces[i]; }
    /** Get the weight of a place on the arc */
    unsigned getWeight (unsigned i) const { return myWeights[i]; }
  private:
    /** number of places */
    unsigned myNumPlaces;
    /** index numbers of places */
    unsigned* myPlaces;
    /** weights of places */
    unsigned* myWeights;
  };

  /** Low-level transition */
  struct ltrans
  {
    /** number of the high level transition */
    unsigned t;
    /** input and output arcs */
    class LArc in, out;
    /** length of the encoded valuation in words */
    size_t datalen;
    /** the encoded valuation */
    word_t* data;
  };

  /** Low-level place name */
  struct lplace
  {
    /** default constructor */
    lplace () : length (0), name (0) {}
    /** length of the name in bits */
    unsigned length;
    /** the name */
    word_t* name;
  };
  /** Less-than comparison for low-level place names */
  struct lplacecmp
  {
    /** Compare two low-level place names
     * @param p1	the first place name
     * @param p2	the second place name
     * @return		true if p1 is less than p2
     */
    bool operator() (const struct lplace& p1,
		     const struct lplace& p2) const {
      if (p1.length < p2.length) return true;
      if (p2.length < p1.length) return false;
      return 0 > memcmp (p1.name, p2.name,
			 (p1.length + (sizeof (word_t) * CHAR_BIT) - 1)
			 / (sizeof (word_t) * CHAR_BIT) * sizeof (word_t));
    }
  };

  /** Map from low-level place names to low-level place numbers */
  typedef std::map<struct lplace,unsigned,struct lplacecmp> PlaceMap;
  /** Iterator to the low-level place name map */
  typedef PlaceMap::iterator iterator;
  /** Constant iterator to the low-level place name map */
  typedef PlaceMap::const_iterator const_iterator;
  /** Constructor
   * @param net		the corresponding high-level net
   */
  explicit LNet (const class Net& net);
private:
  /** Copy constructor */
  explicit LNet (const class LNet& old);
  /** Assignment operator */
  class LNet& operator= (const class LNet& old);
public:
  /** Destructor */
  ~LNet ();

  /** Get the corresponding high-level net */
  const class Net& getNet () const { return myNet; }
  /** Get the number of generated low-level places */
  unsigned getNumPlaces () const { return myNumPlaces; }

  /** Generate the unfolded net using a "coverable marking" algorithm
   * @param printer	printer object for diagnostic output
   * @param maxerrors	maximum number of allowed errors (0=infinity)
   * @return		true if everything succeeded
   */
  bool generateMinimal (const class Printer& printer,
			unsigned maxerrors);

  /** Generate the unfolded net
   * @param printer	printer object for diagnostic output
   * @param maxerrors	maximum number of allowed errors (0=infinity)
   * @return		true if everything succeeded
   */
  bool generate (const class Printer& printer,
		 unsigned maxerrors);

  /** Add a place to the net
   * @param name	name of the place
   * @param length	length of the name in bits
   * @return		number of the place
   */
  unsigned addPlace (word_t* name, unsigned length) {
    struct lplace lp;
    lp.name = name;
    lp.length = length;
    std::pair<iterator,bool> p =
      myPlaceMap.insert (PlaceMap::value_type (lp, myNumPlaces));
    if (p.second) {
      word_t** places = new word_t*[myNumPlaces + 1];
      memcpy (places, myPlaces, myNumPlaces * sizeof *places);
      places[myNumPlaces] = name;
      delete[] myPlaces;
      myPlaces = places;
      return myNumPlaces++;
    }
    delete[] name;
    return p.first->second;
  }

  /** Add a place to the net
   * @param p		number of the high-level place
   * @param value	value of the high-level place
   * @return		number of the low-level place
   */
  unsigned addPlace (unsigned p, const class Value& value);

  /** Find a place in the net
   * @param name	name of the place
   * @param length	length of the name in bits
   * @return		number of the place (UINT_MAX if not found)
   */
  unsigned getPlace (const word_t* name, unsigned length) const {
    struct lplace lp;
    lp.name = const_cast<word_t*>(name);
    lp.length = length;
    const_iterator i = myPlaceMap.find (lp);
    return i == myPlaceMap.end () ? UINT_MAX : i->second;
  }

  /** Find a place in the net
   * @param p		number of the high-level place
   * @param value	value of the high-level place
   * @return		number of the low-level place (UINT_MAX if not found)
   */
  unsigned getPlace (unsigned p, const class Value& value) const;

  /** Introduce low-level places for each token in a high-level marking
   * @param place	number of the high-level place
   * @param p		the high-level marking (multiplicities set to 1)
   */
  void addPlaces (unsigned place,
		  const class PlaceMarking& p);

  /** Remove transitions generated from a high-level transition
   * @param t		number of the high-level transition
   */
  void removeTransitions (unsigned t);

  /** Add a transition to the net
   * @param tr		the transition
   * @return		true if the operation succeeded
   */
  bool addTransition (const struct ltrans& tr);

  /** Unfold a high-level marking
   * @param m		the high-level marking
   * @return		the low-level marking (number of tokens in each place);
   *			NULL if some low-level places do not exist
   */
  unsigned* unfold (const class GlobalMarking& m) const;

  /** Fold a low-level marking
   * @param marking	the low-level marking
   * @return		the high-level marking
   */
  class GlobalMarking& fold (const unsigned* marking) const;

  /** Get the high-level place corresponding to a low-level place
   * @param p		index number of the low-level place
   * @return		the originating high-level place
   */
  const class Place& getPlace (unsigned p) const;

  /** Display a low-level place name
   * @param out		the output stream
   * @param p		index number of the low-level place
   * @return		the originating high-level place
   */
  const class Place& displayPlace (class StringBuffer& out,
				   unsigned p) const;

  /** Display a low-level transition name
   * @param out		the output stream
   * @param t		the low-level transition
   */
  void displayTransition (class StringBuffer& out,
			  const struct ltrans& t) const;

  /** Display the net
   * @param printer	the output stream
   * @param marking	initial marking (number of tokens in each place)
   */
  void display (const class Printer& printer, const unsigned* marking) const;

  /** Dump the net in LoLA format
   * @param file	file to be dumped to
   * @param marking	initial marking (number of tokens in each place)
   */
  void toLoLA (FILE* file, const unsigned* marking) const;

  /** Dump the net in PEP format
   * @param file	file to be dumped to
   * @param marking	initial marking (number of tokens in each place)
   */
  void toPEP (FILE* file, const unsigned* marking) const;

  /** Fold the net to special PROD format
   * @param file	file to be dumped to
   * @param extfile	file for external declarations (global data)
   * @param marking	initial marking (number of tokens in each place)
   */
  void toPROD (FILE* file, FILE* extfile, const unsigned* marking) const;

private:
  /** The corresponding high-level net */
  const class Net& myNet;
  /** Number of bits required for representing high-level places */
  const unsigned myPlaceBits;
  /** Number of low-level places */
  unsigned myNumPlaces;
  /** Map from low-level places to encoded high-level places and values */
  word_t** myPlaces;
  /** Map from encoded high-level places and values to low-level places */
  PlaceMap myPlaceMap;
  /** Buffer for converting place names */
  mutable class BitPacker myBuf;
  /** Low-level transition files */
  FILE** myTransitions;
};

#endif // LNET_H_