Logo Search packages:      
Sourcecode: maria version File versions

LNet.h

Go to the documentation of this file.
// 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 Mäkelä (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 */
00040 class LNet
{
public:
  /** Low-level arc */
00044   class LArc
  {
  public:
    /** Constructor */
00048     LArc () : myNumPlaces (0), myPlaces (0), myWeights (0) {}
    /** Copy constructor */
00050     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 */
00063     ~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
     */
00069     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 */
00108     unsigned getNumPlaces () const { return myNumPlaces; }
    /** Get the number of a place on the arc */
00110     unsigned getPlace (unsigned i) const { return myPlaces[i]; }
    /** Get the weight of a place on the arc */
00112     unsigned getWeight (unsigned i) const { return myWeights[i]; }
  private:
    /** number of places */
00115     unsigned myNumPlaces;
    /** index numbers of places */
00117     unsigned* myPlaces;
    /** weights of places */
00119     unsigned* myWeights;
  };

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

  /** Low-level place name */
00136   struct lplace
  {
    /** default constructor */
00139     lplace () : length (0), name (0) {}
    /** length of the name in bits */
00141     unsigned length;
    /** the name */
00143     word_t* name;
  };
  /** Less-than comparison for low-level place names */
00146   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
     */
00153     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 */
00164   typedef std::map<struct lplace,unsigned,struct lplacecmp> PlaceMap;
  /** Iterator to the low-level place name map */
00166   typedef PlaceMap::iterator iterator;
  /** Constant iterator to the low-level place name map */
00168   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 */
00183   const class Net& getNet () const { return myNet; }
  /** Get the number of generated low-level places */
00185   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
   */
00208   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)
   */
00238   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 */
00332   const class Net& myNet;
  /** Number of bits required for representing high-level places */
00334   const unsigned myPlaceBits;
  /** Number of low-level places */
00336   unsigned myNumPlaces;
  /** Map from low-level places to encoded high-level places and values */
00338   word_t** myPlaces;
  /** Map from encoded high-level places and values to low-level places */
00340   PlaceMap myPlaceMap;
  /** Buffer for converting place names */
00342   mutable class BitPacker myBuf;
  /** Low-level transition files */
00344   FILE** myTransitions;
};

#endif // LNET_H_

Generated by  Doxygen 1.6.0   Back to index