// Reporting successor states -*- c++ -*-

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

# include "BitBuffer.h"

/** @file StateReporter.h
 * Interface for reporting successor states
 */

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

/** Reporting successor states */
class StateReporter
{
public:
  /** Search kinds */
  enum SearchKind {
    Breadth,	///< exhaustive breadth-first search
    Depth,	///< exhaustive depth-first search
    Single	///< process a single state
  };

  /** Constructor
   * @param compilation	the compiled model (optional)
   * @param net_	the net that is being analysed
   * @param printer_	printer object for diagnostic output
   * @param maxerrors	maximum number of allowed errors (0=infinity)
   * @param compress	flag: collapse deterministic sequences?
   * @param local	flag: suppress transient (invisible) states?
   * @param flattened	flag: consider the flattened net?
   */
  StateReporter (
# ifdef EXPR_COMPILE
		 const class Compilation* compilation,
# endif // EXPR_COMPILE
		 const class Net& net_,
		 const class Printer& printer_,
		 unsigned maxerrors,
		 bool compress,
		 bool local,
		 bool flattened);
  /** Copy constructor */
  StateReporter (const class StateReporter& old);
private:
  /** Assignment operator */
  class StateReporter& operator= (const class StateReportert& other);
public:
  /** Destructor */
  virtual ~StateReporter ();

  /** Get the number of errors that have been reported */
  unsigned getNumErrors () const { return myNumErrors; }
  /** Get the number of local states generated in modular analysis */
  unsigned getNumLocal () const { return myNumLocal; }

  /** Get the minimum length of state vectors */
  size_t getMinSize () const { return myMinSize; }
  /** Get the maximum length of state vectors */
  size_t getMaxSize () const { return myMaxSize; }
  /** Get the transition enabledness sets */
  const char* getEnabled () const { return myEnabled; }
  /** Determine if the flattened net is being considered */
  bool isFlattened () const { return myFlattened; }

  /** Determine whether this is a reduced state space */
  bool isReduced () const { return !!myLocal; }

  /** Note an enabled transition
   * @param transition	the transition
   */
  void enabled (const class Transition& transition);

# ifdef EXPR_COMPILE
protected:
  /** Analyze the successors of a transition
   * @param transition	the transition
   */
  void analyze (const class Transition& transition);
public:
  /** Report a successor state
   * @param buf		the encoded state
   * @param size	length of the encoded state, in bytes
   * @param rejected	flag: is the state rejected?
   * @param hidden	flag: is the transition to the state hidden?
   * @param tr		the index of the transition that fired
   */
  void addState (const void* buf, size_t size,
		 bool rejected, bool hidden, unsigned tr);
# endif // EXPR_COMPILE

  /** Search the state space
   * @param kind	Type of search
   */
  void analyze (enum SearchKind kind);

private:
  /** Search the state space of the flattened net
   * @param kind	Type of search
   */
  void analyzeFlattened (enum SearchKind kind);

  /** Search the state space in a modular way
   * @param kind	Type of search
   */
  virtual void analyzeModular (enum SearchKind kind);

protected:
  /** Initialize the state spaces of the modules
   * @return		the state spaces of the modules, or 0 if not modular
   */
  class FullSet* initModules () const;
  /** Search the state spaces of the modules
   * @param m		the source marking
   * @param sync	the synchronisation states
   * @param childset	the state spaces of the modules
   */
  void analyzeModules (const class GlobalMarking& m,
		       class SyncStates& sync,
		       class FullSet* childset);
# ifdef EXPR_COMPILE
  /** Search the state spaces of the modules
   * @param sync	the synchronisation states
   * @param childset	the state spaces of the modules
   */
  void analyzeModules (class SyncStates& sync,
		       class FullSet* childset);

public:
  /** Generate the successors of a synchronisation transition
   * @param transition	the transition
   */
  void sync (const class Transition& transition);
protected:
# endif // EXPR_COMPILE
  /** Determine if a state can be suppressed */
  bool suppress ();

public:
  /** Report a successor state
   * @param transition	the transition fired
   * @param valuation	the binding of the transition
   * @param marking	the resulting marking
   * @return		true if analysis should proceed; false on fatal error
   */
  bool report (const class Transition& transition,
	       const class Valuation& valuation,
	       const class GlobalMarking& marking);

  /** Report a synchronisation state
   * @param transition	the synchronisation transition
   */
  void reportSync (const class Transition& transition);

  /** Set the synchronisation source state (called by SyncStates)
   * @param src		the encoded source state
   * @param size	length of the encoded state in bytes
   */
  void setSyncSource (word_t* src, size_t size) {
    delete[] mySrc; mySrc = src; mySrcSize = size;
  }

protected:
  /** Report an error
   * @return		true when the maximum amount of errors has been reached
   */
  bool error () { return ++myNumErrors == myMaxErrors; }

  /** Add an encoded state to the state space (called by report ())
   * @param state	the encoded state
   * @param size	length of the encoded state in bytes
   * @param hidden	flag: is the transition to the state hidden?
   * @return		true if the state was new
   */
  bool addState (const void* state,
		 size_t size,
		 bool hidden);

  /** Fetch an encoded state
   * @param tail	flag: retrieve from tail of list instead of head
   * @return		the encoded state (mySrc), or NULL if none available
   */
  word_t* popState (bool tail);

  /** Inflate the source state buffer */
  void inflate () {
    BitPacker::inflate (mySrc[(mySrcSize - 1) / sizeof (word_t)],
			(-mySrcSize) % sizeof (word_t));
  }
  /** Deflate the source state buffer */
  void deflate () {
    BitPacker::deflate (mySrc[(mySrcSize - 1) / sizeof (word_t)],
			(-mySrcSize) % sizeof (word_t));
  }

private:
  /** Add an encoded state to the state space
   * @param state	the encoded state
   * @param size	length of the encoded state in bytes
   * @return		true if the state was new
   */
  virtual bool do_addState (const void* state,
			    size_t size) = 0;

  /** Fetch an encoded state
   * @param tail	flag: retrieve from tail of list instead of head
   * @param size	(output) length of the encoded stream
   * @return		the encoded state, or NULL if none available
   */
  virtual word_t* do_popState (bool tail, size_t& size) = 0;

  /** Dequeue an unprocessed state
   * @param breadth	true=dequeue (FIFO, queue), false=pop (LIFO, stack)
   * @return		an unprocessed state, or NULL if all processed
   */
  virtual class GlobalMarking* pop (bool breadth) = 0;

# ifdef EXPR_COMPILE
  /** Dequeue an unprocessed state
   * @param breadth	true=dequeue (FIFO, queue), false=pop (LIFO, stack)
   * @return		true if a state was found, or false if all processed
   */
  virtual bool popCompiled (bool breadth) = 0;

  /** Determine whether arcs should be generated */
  virtual bool isGraph () const { return false; }
# endif // EXPR_COMPILE

  /** Add all events from the current source state to the graph */
  virtual void addEvents ();

  /** Report a successor state
   * @param transition	the transition fired
   * @param valuation	the binding of the transition
   * @param marking	the resulting marking
   * @param rejected	flag: is the state rejected?
   * @return		true if the state was new
   */
  virtual bool report (const class Transition& transition,
		       const class Valuation& valuation,
		       const class GlobalMarking& marking,
		       bool rejected) = 0;

  /** Report a deadlock or an error in the current state
   * @param deadlock	flag: is this a deadlock?
   */
  virtual void reportError (bool deadlock) = 0;

public:
# ifdef EXPR_COMPILE
  /** Report a successor state
   * @param state	the resulting encoded deflated state (mandatory)
   * @param size	length of the encoded state, in bytes
   * @param rejected	flag: is the state rejected?
   * @param hidden	flag: is the transition to the state hidden?
   * @return		true if the state was new
   */
  virtual bool report (const void* state,
		       size_t size,
		       bool rejected,
		       bool hidden) = 0;
# endif // EXPR_COMPILE

  /** Report an inconsistent successor state
   * @param transition	the transition fired
   * @param valuation	the binding of the transition
   * @param marking	the resulting marking
   * @param reason	reason for failure (optional)
   * @param place	the place whose marking could not be encoded (optional)
   */
  void reject (const class Transition& transition,
	       const class Valuation& valuation,
	       const class GlobalMarking& marking,
	       const char* reason,
	       const class Place* place);

  /** Determine whether a fatal condition has occurred */
  bool isFatal () const { return myFatal; }
  /** Flag a fatal condition */
  void flagFatal () { myFatal = true; }

private:
  /** Report an inconsistent successor state */
  virtual void reject () = 0;

public:
# ifdef EXPR_COMPILE
  /** The compiled model */
  const class Compilation* const myCompilation;
# endif // EXPR_COMPILE
  /** The net being analyzed */
  const class Net& net;
  /** Printer object for diagnostics */
  const class Printer& printer;
private:
  /** Maximum allowed number of errors (0=infinite) */
  const unsigned myMaxErrors;
  /** Number of errors that have occurred */
  unsigned myNumErrors;
  /** Number of local states generated in modular analysis */
  unsigned myNumLocal;
  /** Log of enabledness set occurrences (optional) */
  char* const myEnabled;
protected:
  /** Synchronisation states for modular analysis (optional) */
  class SyncStates* mySync;
  /** Flag: has a fatal condition occurred? */
  bool myFatal;
  /** Flag: is the source state a deadlock? */
  bool mySrcDeadlock;
  /** Priority level of the last fired transition */
  unsigned myPriority;
  /** Encoder for states */
  class BitPacker myStateBuf;
  /** The encoded state that is being analyzed */
  word_t* mySrc;
  /** Length of mySrc, in bytes */ 
  size_t mySrcSize;
private:
  /** Flag: apply search on flattened state space? */
  const bool myFlattened;
  /** Set of local (transient, invisible) states */
  class FullSet* const myLocal;
  /** Suppressed states (when applying path compression) */
  class States* const mySuppressed;
  /** Flag: how many successors does the state have (in path compression) */
  enum { None = 0, One, Many } mySuccessors;
  /** Minimum length of encoded state vectors */
  size_t myMinSize;
  /** Maximum length of encoded state vectors */
  size_t myMaxSize;
};

#endif // STATEREPORTER_H_