// Reporting successor states in safety property analysis -*- c++ -*-

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

# include "StateReporter.h"

/** @file StateSetReporter.h
 * Interface for reporting successor states in safety property 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 safety property analysis */
class StateSetReporter : 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 dotty	visualization interface for counterexamples
   * @param merge	flag: merge visual counterexamples to one graph?
   * @param states	the state space being generated
   * @param prop	property being analyzed (optional)
   */
  StateSetReporter (
# 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,
		    const class Dotty* dotty,
		    bool merge,
		    class StateSet& states,
		    const class Property* prop);

  /** Constructor for recovering error traces
   * @param old		the reporter being copied
   * @param update	flag: update the state space?
   * @param states	the state space being generated
   * @param dest	the encoded inflated destination state
   * @param destsize	length of the encoded state being sought, in words
   */
  StateSetReporter (const class StateSetReporter& old,
		    bool update,
		    class StateSet& states,
		    const word_t* dest,
		    unsigned destsize);

  /** Constructor for client-side reporting in distributed search
   * @param old		the reporter being copied
   * @param states	the state space being generated
   */
  StateSetReporter (const class StateSetReporter& old,
		    class StateSet& states);

private:
  /** Copy constructor */
  StateSetReporter (const class StateSetReporter& old);
  /** Assignment operator */
  class StateSetReporter& operator= (const class StateSetReportert& other);
public:
  /** Destructor */
  ~StateSetReporter ();

  /** Start displaying an error trace */
  void displayPrologue () const;
  /** Finish displaying an error trace */
  void displayEpilogue () const;
  /** Display a marking */
  void displayMarking (const class GlobalMarking& m) const;
  /** Display an encoded inflated state
   * @param s		the state to be displayed
   */
  void displayState (const word_t* s) const;
  /** Display a path leading from a state to another
   * @param src		the encoded inflated source state
   * @param dest	the encoded inflated destination state
   * @param destsize	length of the encoded state being sought, in words
   */
  void displayPath (const word_t* src,
		    const word_t* dest,
		    unsigned destsize) const;

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);

  /** 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);
# 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 analysis should proceed; false on fatal error
   */
  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

  /** @name Server-side methods for distributed verification */
  /*@{*/
  /** Report a successor state and a number of pending states
   * @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?
   * @param pending	number of additional pending states
   * @return		true if the state was new
   */
  bool report (const void* state,
	       size_t size,
	       bool rejected,
	       bool hidden,
	       unsigned pending);

  /** Display path to a rejected state
   * @param dstate	the encoded rejected state
   * @param dlen	length of dstate in bytes
   * @param offset	offset to the counterexample path file
   * @param reduced	flag: has the state space been reduced?
   * @param reason	reason for rejecting the state
   */
  void reject (const void* dstate,
	       size_t dlen,
	       long offset,
	       bool reduced,
	       unsigned reason);

  /** Fetch an encoded state
   * @param tail	flag: retrieve from tail of list instead of head
   * @param size	(output) length of the encoded stream
   * @param offset	(output) offset to the counterexample file
   * @return		the encoded state
   */
  word_t* pop (bool tail, size_t& size, long& offset);

  /** Set the offset to the counterexample
   * @param offset	offset to the counterexample path file
   */
  void setOffset (long offset);
  /*@}*/

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

  /** Display a path from src to myDest
   * @param src		the encoded inflated source state
   */
  void displayPath (const word_t* src);

private:
  /** Threshold for reporting intermediate statistics */
  const unsigned myThreshold;
  /** Visualization interface for counterexamples */
  const class Dotty* const myDotty;
  /** Flag: merge visual counterexamples to one graph? */
  const bool myMerge;
  /** Flag: update the state space? */
  const bool myUpdate;
  /** Encoded state being sought (optional) */
  const word_t* const myDest;
  /** Length of the encoded state being sought */
  const unsigned myDestSize;
  /** The state space being generated */
  class StateSet& myStates;
  /** Property being analyzed (optional) */
  const class Property* const myProp;
  /** Number of bits per property state (0 when no property) */
  const unsigned myPropBits;
  /** Amount and numbers of the enabled successor states in myProp */
  unsigned* myPropSucc;
  /** Flag: is the property automaton about to enter a rejecting state? */
  bool myPropReject;
};

#endif // STATESETREPORTER_H_