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

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

  /** Addition status */
  class AddStatus
  {
  public:
    /** Constructor
     * @param isNew_	flag: was the state just added to the graph?
     * @param number_	the state number
     */
    AddStatus (bool isNew_, card_t number_) :
      isNew (isNew_), number (number_) {
    }
    /** Copy constructor */
    AddStatus (const class AddStatus& old) :
      isNew (old.isNew), number (old.number) {
    }
    /** Assignment operator */
    class AddStatus& operator= (const class AddStatus& old) {
      isNew = old.isNew, number = old.number;
      return *this;
    }
    /** Destructor */
    ~AddStatus () {}
    /** flag: was the state just added to the graph? */
    bool isNew;
    /** the state number */
    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 */
  const class Net& getNet () const { return myNet; }
  /** Determine the number of arcs generated */
  unsigned getNumArcs () const
# ifdef USE_MMAP
    ;
# else // USE_MMAP
  { return myNumArcs; }
# endif // USE_MMAP

  /** Determine the name of the Petri Net */
  const char* getFilename () const { return myFilename; }
  /** Determine the base name for the graph files */
  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 */
  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 */
  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 */
  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 */
  const class Net& myNet;
  /** Buffer for successor state numbers of events */
  card_t* mySucc;
# ifndef USE_MMAP
  /** Number of arcs */
  unsigned myNumArcs;
  /** Number of states */
  unsigned myNumStates;
# endif // !USE_MMAP
  /** The state hash */
  class BTree* myStates;
# if defined __sgi || defined __DECCXX
public:
# endif // __sgi || __DECCXX
  /** The graph files */
  struct files myFiles;
# if defined __sgi || defined __DECCXX
private:
# endif // __sgi || __DECCXX
  /** Offset of the state directory in myDirectory */
  fpos_t myDirectoryOffset;
  /** Name of the Petri Net */
  const char* myFilename;
  /** Base name for the graph files */
  const char* myFilebase;
  /** Labelled state transition system output for newly generated states */
  class LSTS* myLSTS;
};

#endif // GRAPH_H_