Logo Search packages:      
Sourcecode: maria version File versions

Graph.h

Go to the documentation of this file.
// Persistent reachability graph storage -*- c++ -*-

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

# include "BitBuffer.h"

# include <map>
# include <assert.h>
# include "file.h"

/** @file Graph.h
 * Persistent, lossless reachability graph storage
 */

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

/** Persistent reachability graph storage */
00040 class Graph
{
public:
  /** File offset */
00044   typedef long fpos_t;
  /** nonexistent file offset */
00046 # define FPOS_NONE (Graph::fpos_t (-1))
  /** special offset indicating a deadlock state */
00048 # define FPOS_DEAD (Graph::fpos_t (-2))
  /** Graph files */
00050   struct files {
    /** Directory */
00052     file_t directory;
    /** State storage */
00054     file_t states;
    /** Arc storage */
00056     FILE* arcs;
    /** Predecessor state storage */
00058     file_t preds;
  };

  /** Addition status */
00062   class AddStatus
  {
  public:
    /** Constructor
     * @param isNew_    flag: was the state just added to the graph?
     * @param number_   the state number
     */
00069     AddStatus (bool isNew_, card_t number_) :
      isNew (isNew_), number (number_) {
    }
    /** Copy constructor */
00073     AddStatus (const class AddStatus& old) :
      isNew (old.isNew), number (old.number) {
    }
    /** Assignment operator */
00077     class AddStatus& operator= (const class AddStatus& old) {
      isNew = old.isNew, number = old.number;
      return *this;
    }
    /** Destructor */
00082     ~AddStatus () {}
    /** flag: was the state just added to the graph? */
00084     bool isNew;
    /** the state number */
00086     card_t number;
  };

  /** Constructor
   * @param net         the net whose reachability graph this is
   */
  explicit Graph (const class Net& net);
  /** Constructor
   * @param net         the net whose reachability graph this is
   * @param filename    name of the Petri Net file (NULL=read from graph file)
   * @param filebase    base name for the graph files (generated if NULL)
   */
  explicit Graph (const class Net& net,
              const char* filename, const char* filebase);
private:
  /** Copy constructor */
  explicit Graph (const class Graph& old);
  /** Assignment operator */
  class Graph& operator= (const class Graph& old);
public:
  /** Destructor */
  ~Graph ();

  /** Determine the net whose reachability graph this is */
00110   const class Net& getNet () const { return myNet; }
  /** Determine the number of arcs generated */
00112   unsigned getNumArcs () const
# ifdef USE_MMAP
    ;
# else // USE_MMAP
  { return myNumArcs; }
# endif // USE_MMAP

  /** Determine the name of the Petri Net */
00120   const char* getFilename () const { return myFilename; }
  /** Determine the base name for the graph files */
00122   const char* getFilebase () const { return myFilebase; }

  /** Open the reachability graph files
   * @param regenerate  flag: true=ignore existing graph files
   * @return            true if the files could be opened; false on error
   */
  bool openFiles (bool regenerate);

  /** Set the LSTS output handler
   * @param lsts  the output handler (NULL=none)
   */
  void setLSTS (class LSTS* lsts);
  /** Get the LSTS output handler */
00135   class LSTS* getLSTS () const { return myLSTS; }

  /** Add an encoded state to the graph
   * @param buf         the encoded state
   * @param bytes size of the encoded state in bytes
   * @return            {false,number} if the state already exists
   *              {true,number} if the state was added
   */
  const class AddStatus add (const void* buf,
                       size_t bytes);

  /** Look up a state in the graph
   * @param buf         the encoded state
   * @param bytes size of the encoded state in bytes
   * @return            the state number, or CARD_T_MAX if not found
   */
  card_t lookup (const void* buf, size_t bytes) const;

  /** Add an event to the graph
   * @param source      the source state number
   * @param target      the target state number
   */
  void add (card_t source, card_t target);

  /** Update added events to the arc file and flag the source state processed
   * @param source      the source state number
   * @param buf         the encoded events
   * @param bytes size of the encoded events in bytes
   */
  void addEvents (card_t source,
              const void* buf,
              size_t bytes);

  /** Get the number of states in the reachability graph */
00169   size_t getNumStates () const
# ifdef USE_MMAP
    ;
# else // USE_MMAP
  { return myNumStates; }
# endif // USE_MMAP

public:
  /** Fetch an encoded state from the reachability graph
   * @param number      number of the state
   * @param length      (output) length of the encoded state in bytes
   * @param erroneous   (output) flag: erroneous state
   * @return            the encoded state, or NULL
   */
  word_t* fetchState (card_t number, size_t& length, bool* erroneous) const;

  /** Get a state by number
   * @param number      number of the state
   * @return            the decoded state
   */
  class GlobalMarking* fetchState (card_t number) const;
  
  /** Get the number of predecessor states of a state
   * @param state number of the state
   * @return            number of directly preceding states
   */
  card_t getNumPredecessors (card_t state) const;

  /** Fetch an offset to the predecessor records for a state
   * @param state number of the state
   * @return            offset to the event storage (FPOS_NONE if none)
   */
  fpos_t getPredecessors (card_t state) const;

  /** Fetch predecessor state numbers for a state
   * @param pos         (in/out) offset to the event storage
   * @return            number of the source state (pos==FPOS_NONE at end)
   */
  card_t getPredecessor (fpos_t& pos) const;

  /** Fetch the successor arcs for a state
   * @param state number of the state
   * @param data  (output) the encoded successors
   * @return            amount and numbers of successor states
   */
  card_t* getSuccessors (card_t state, word_t** data = 0) const;

  /** Evaluate a condition in a state
   * @param state the state
   * @param cond  the condition (NULL=true)
   * @return            whether the condition holds
   */
  bool eval (card_t state,
           const class Expression* cond) const;

  /** Tree of paths */
00225   typedef std::map<card_t,card_t> PathMap;

  /** Extract a path from a leaf to the root of a tree
   * @param tree  the tree
   * @param dest  the leaf of the tree
   * @return            the path
   */
  static card_t* toPath (const PathMap& tree,
                   card_t dest);

  /** Determine the shortest path from a state to a state
   * @param state the source state
   * @param target      the target state
   * @param pathc condition that must hold in every state on the path
   * @return            the amount and numbers of the states on the path
   */
  card_t* path (card_t state, card_t target,
            const class Expression* pathc) const;

  /** Determine the shortest path to a state fulfilling a condition
   * @param state the source state
   * @param cond  the condition
   * @param pathc condition that must hold in every state on the path
   * @return            the amount and numbers of the states on the path
   */
  card_t* path (card_t state, const class Expression& cond,
            const class Expression* pathc) const;

  /** Determine the shortest path from a state fulfilling a condition
   * @param state the target state
   * @param cond  the condition
   * @param pathc condition that must hold in every state on the path
   * @return            the amount and numbers of the states on the path
   */
  card_t* rpath (card_t state, const class Expression& cond,
             const class Expression* pathc) const;

  /** Determine the shortest path to a loop state
   * @param state the source state
   * @param loop  the amount and numbers of the states forming the loop
   * @param pathc condition that must hold in every state on the path
   * @return            the amount and numbers of the states on the path
   */
  card_t* path (card_t state,
            const card_t* loop,
            const class Expression* pathc) const;

  /** Flag a state erroneous
   * @param number      the state number
   * @return            whether the state already was flagged erroneous
   */
  bool flagErroneous (card_t number);

  /** Determine whether a state is erroneous
   * @param number      the state number
   */
  bool isErroneous (card_t number) const;

  /** Determine whether a state has been processed
   * @param number      the state number
   */
  bool isProcessed (card_t number) const;

private:
  /** Add a reverse arc to the graph
   * @param source      source state number
   * @param target      target state number
   */
  void addReverse (card_t source, card_t target);

private:
  /** The net whose reachability graph this is */
00297   const class Net& myNet;
  /** Buffer for successor state numbers of events */
00299   card_t* mySucc;
# ifndef USE_MMAP
  /** Number of arcs */
00302   unsigned myNumArcs;
  /** Number of states */
00304   unsigned myNumStates;
# endif // !USE_MMAP
  /** The state hash */
00307   class BTree* myStates;
# if defined __sgi || defined __DECCXX
public:
# endif // __sgi || __DECCXX
  /** The graph files */
00312   struct files myFiles;
# if defined __sgi || defined __DECCXX
private:
# endif // __sgi || __DECCXX
  /** Offset of the state directory in myDirectory */
00317   fpos_t myDirectoryOffset;
  /** Name of the Petri Net */
00319   const char* myFilename;
  /** Base name for the graph files */
00321   const char* myFilebase;
  /** Labelled state transition system output for newly generated states */
00323   class LSTS* myLSTS;
};

#endif // GRAPH_H_

Generated by  Doxygen 1.6.0   Back to index