// Reporting successor states in graph-based analysis -*- c++ -*-

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

# include "StateReporter.h"
# include "Search.h"

/** @file GraphReporter.h
 * Interface for reporting successor states in graph-based analysis
 */

/* 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 in graph-based analysis */
class GraphReporter : public StateReporter
{
public:
  /** 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?
   * @param threshold	threshold for reporting state space statistics
   * @param graph	the reachability graph being generated
   */
  GraphReporter (
#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,
		 unsigned threshold,
		 class Graph& graph);
private:
  /** Copy constructor */
  GraphReporter (const class GraphReporter& old);
  /** Assignment operator */
  class GraphReporter& operator= (const class GraphReporter& other);
public:
  /** Destructor */
  ~GraphReporter ();

  /** Get a reference to the reachability graph */
  const class Graph& getGraph () const { return myGraph; }
  /** Get the graph of strongly connected components */
  const class ComponentGraph* getComponents () const { return myComponents; }
  /** Get a GraphReporter by module
   * @param path	amount and indexes of path components (subnets)
   */
  class GraphReporter& getChild (const unsigned* path);
  /** Get a GraphReporter by module
   * @param path	amount and indexes of path components (subnets)
   */
  const class GraphReporter& getChild (const unsigned* path) const {
    return const_cast<class GraphReporter*>(this)->getChild (path);
  }

  /** Compute the strongly connected components for this graph
   * @param state	start state of the search
   * @param cond	condition for exploring states (NULL=true)
   * @return		number of strongly connected components (0=fail)
   */
  unsigned strong (card_t state,
		   const class Expression* cond);

  /** Initialize the search list
   * @param state	the state to be analyzed
   */
  void init (card_t state) {
    assert (myStates.empty ()); myStates.push (state);
  }
  /** Assign the addOld flag */
  void setAddOld (bool addOld) { myAddOld = addOld; }

  /** Retrieve the successors of a state
   * @param state	the state to be analyzed
   * @return		the successors of the state (must be cleared by caller)
   */
  class SearchList& getSuccessors (card_t state);

  /** Analyze an anonymous transition
   * @param transition	the transition
   * @return		the successor states (must be cleared by caller)
   */
  class SearchList& getSuccessors (const class Transition& transition);

  /** Prepare for computing the enabled fairness sets
   * @param state	the state to be analyzed
   * @param buf		(output) the encoded event labels (deleted by caller)
   * @param u		(output) the bit unpacker object (deleted by caller)
   * @return		the successors of the state (deleted by caller)
   */
  card_t* prepareFair (card_t state,
		       word_t*& buf,
		       class BitUnpacker*& u);

  /** Compute the enabled fairness sets
   * @param state	the state being analyzed (for diagnostics)
   * @param u		the bit unpacker object from prepareFair ()
   * @param strong	(output) the enabled strong fairness sets (optional)
   *			(static allocation; not deleted by caller)
   * @return		amount and numbers of enabled weak fairness sets
   *			(static allocation; not deleted by caller)
   */
  unsigned* computeFair (card_t state,
			 class BitUnpacker* u,
			 unsigned** strong);

  /** Evaluate the gates of a property automaton
   * @param state	the state number of the reachability graph
   * @param prop	the state number of the property automaton
   * @param ps		current state in the property automaton
   * @return		the amount and numbers of enabled successor states
   */
  const unsigned* eval (card_t state,
			unsigned prop,
			const class PropertyState& ps);
  /** Finish evaluating the gates of a property automaton
   * @param enabled	an array of enabled states returned by eval ()
   */
#ifdef EXPR_COMPILE
  void eval_done (const unsigned* enabled) const
#else
  static void eval_done (const unsigned* enabled)
#endif // EXPR_COMPILE
  {
#ifdef EXPR_COMPILE
    if (!myCompilation)
#endif // EXPR_COMPILE
      delete[] enabled;
  }

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

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
   */
  bool do_addState (const void* state,
		    size_t size);

  /** Add an encoded state to the state space, but do not enqueue it
   * @param state	the encoded state
   * @param size	length of the encoded state in bytes
   * @return		true if the state was new
   */
  bool do_addStateOnly (const void* state,
			size_t size);

  /** 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
   */
  word_t* do_popState (bool tail, size_t& size);

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

#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
   */
  bool popCompiled (bool breadth);

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

  /** Add all events from the current source state to the graph */
  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
   */
  bool report (const class Transition& transition,
	       const class Valuation& valuation,
	       const class GlobalMarking& marking,
	       bool rejected);

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

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
   */
  bool report (const void* state,
	       size_t size,
	       bool rejected,
	       bool hidden);
#endif // EXPR_COMPILE

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

public:
  /** Display a state number
   * @param m		the state (to be decomposed into module states)
   * @param state	the state number
   * @param out		the output stream
   */
  void printState (const class GlobalMarking& m,
		   card_t state,
		   const class Printer& out);

private:
  /** Threshold for reporting intermediate statistics */
  const unsigned myThreshold;
  /** The reachability graph being constructed */
  class Graph& myGraph;
  /** Graph of strongly connected components (optional) */
  class ComponentGraph* myComponents;
  /** GraphReporters for modules (only for non-flattened analysis) */
  class GraphReporter** const myChildren;
  /** Table for keeping track of visited states in non-flattened analysis */
  class BitVector* myVisited;
  /** Buffer for encoding events */
  class BitPacker myEventBuf;
  /** List of unprocessed states */
  class SearchList myStates;
  /** Number of the state being analyzed */
  card_t myStateNum;
  /** Number of the state last generated (set by do_addState) */
  card_t myTargetNum;
  /** Flag: is myStateNum being revisited? */
  bool myProcessed;
  /** Work area for computing enabled weak fairness sets */
  unsigned* myWeaklyFair;
  /** Work area for computing enabled strong fairness sets */
  unsigned* myStronglyFair;
  /** Flag: add also existing states to the state list */
  bool myAddOld;
};

#endif // GRAPHREPORTER_H_