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

/** @file StateSetReporter.C
 * 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. */

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "StateSetReporter.h"
#include "FullSet.h"
#include "SyncStates.h"
#include "Net.h"
#include "Transition.h"
#include "Valuation.h"
#include "GlobalMarking.h"
#include "Property.h"
#include "Printer.h"
#include "Dotty.h"

StateSetReporter::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) :
  StateReporter (
#ifdef EXPR_COMPILE
		 compilation,
#endif // EXPR_COMPILE
		 net_, printer_, maxerrors, compress, local, flattened),
  myThreshold (threshold),
  myDotty (dotty), myMerge (merge), myUpdate (true),
  myDest (0), myDestSize (0),
  myStates (states),
  myProp (prop), myPropBits (prop ? log2 (prop->getNumStates ()) : 0),
  myPropSucc (0), myPropReject (false)
{
}

StateSetReporter::StateSetReporter (const class StateSetReporter& old,
				    bool update,
				    class StateSet& states,
				    const word_t* dest,
				    unsigned destsize) :
  StateReporter (
#ifdef EXPR_COMPILE
		 old.myCompilation,
#endif // EXPR_COMPILE
		 old.net, old.printer, 1, false, false, old.isFlattened ()),
  myThreshold (0),
  myDotty (old.myDotty), myMerge (old.myMerge), myUpdate (update),
  myDest (dest), myDestSize (destsize),
  myStates (states), myProp (old.myProp), myPropBits (old.myPropBits),
  myPropSucc (0), myPropReject (false)
{
}

StateSetReporter::StateSetReporter (const class StateSetReporter& old,
				    class StateSet& states) :
  StateReporter (old),
  myThreshold (0),
  myDotty (old.myDotty), myMerge (old.myMerge), myUpdate (true),
  myDest (0), myDestSize (0), myStates (states),
  myProp (old.myProp), myPropBits (old.myPropBits),
  myPropSucc (0), myPropReject (false)
{
}

StateSetReporter::~StateSetReporter ()
{
  delete[] myPropSucc;
}

void
StateSetReporter::displayPrologue () const
{
  if (myDotty)
    myDotty->displayPrologue (myMerge);
}

void
StateSetReporter::displayEpilogue () const
{
  if (myDotty)
    myDotty->displayEpilogue ();
}

void
StateSetReporter::displayMarking (const class GlobalMarking& m) const
{
  if (myDotty)
    myDotty->displayMarking (m);
  else
    m.display (printer), printer.finish ();
}

void
StateSetReporter::displayState (const word_t* s) const
{
  class GlobalMarking m (net);
  m.decode (*net.getInitMarking (), s, myPropBits);
  displayMarking (m);
}

void
StateSetReporter::displayPath (const word_t* src,
			       const word_t* dest,
			       unsigned destsize) const
{
  class StateSetReporter reporter (*this, false, myStates, dest, destsize);
  reporter.displayPath (src);
}

bool
StateSetReporter::do_addState (const void* state,
			       size_t size)
{
  return myStates.add (state, size);
}

word_t*
StateSetReporter::do_popState (bool tail,
			       size_t& size)
{
  return myStates.pop (tail, size);
}

class GlobalMarking*
StateSetReporter::pop (bool breadth)
{
  delete[] myPropSucc;
  myPropSucc = 0;
  while (popState (breadth)) {
    inflate ();
    class GlobalMarking* m = new class GlobalMarking (net);
    const unsigned ps = m->decode (*net.getInitMarking (), mySrc, myPropBits);
    if (myProp) {
      class Valuation valuation;
      valuation.setGlobalMarking (m);
      myPropReject = !(*myProp)[ps].eval (valuation, myPropSucc,
					  myProp->getFinalState ());
      if (myPropReject && !valuation.isOK ()) {
	printer.printRaw ("property ");
	printer.print (ps);
	printer.printRaw (" evaluation error");
	printer.finish ();
	flagFatal ();
	if (!myDest)
	  myStates.reject (mySrc, mySrcSize, *this,
			   StateSet::propertyError, isReduced ());
	delete[] myPropSucc;
	myPropSucc = 0;
	delete m;
	return 0;
      }
      else if (!*myPropSucc) {
	delete[] myPropSucc;
	myPropSucc = 0;
	delete m;
	continue;
      }
    }
    return m;
  }
  return 0;
}

#ifdef EXPR_COMPILE
# include "Compilation.h"

bool
StateSetReporter::popCompiled (bool breadth)
{
  assert (!!myCompilation);
  delete[] myPropSucc;
  myPropSucc = 0;
  while (popState (breadth)) {
    myCompilation->stateDecode (net.getIndex (), mySrc, mySrcSize);
    if (myProp) {
      const unsigned ps = *myCompilation->getPropSucc ();
      enum Error err = myCompilation->propEval (ps);
      myPropReject = err == errComp;
      if (err && err != errComp) {
	printer.printRaw ("property ");
	printer.print (ps);
	printer.printRaw (" evaluation error");
	printer.finish ();
	flagFatal ();
	if (!myDest)
	  myStates.reject (mySrc, mySrcSize, *this,
			   StateSet::propertyError, isReduced ());
	delete[] myPropSucc;
	myPropSucc = 0;
	return false;
      }
      else if (!*myCompilation->getPropSucc ()) {
	continue;
      }
    }
    return true;
  }
  return false;
}
#endif // EXPR_COMPILE

void
StateSetReporter::addEvents ()
{
  delete[] myPropSucc;
  myPropSucc = 0;
}

bool
StateSetReporter::report (const class Transition& transition,
			  const class Valuation& valuation,
			  const class GlobalMarking& marking,
			  bool rejected)
{
  /** flag: is the state new? */
  bool isNew = false;
  if (myPropReject)
    rejected = true;
  const unsigned* p = myPropBits ? (myPropSucc + *myPropSucc) : 0;
  do {
    if (myPropBits)
      myStateBuf.append (*p, myPropBits);
    if (myDest) {
      if (myDestSize == myStateBuf.getNumWords () &&
	  !memcmp (myDest, myStateBuf.getBuf (),
		   sizeof (word_t) * myDestSize)) {
	if (myDotty)
	  myDotty->displayEdge (transition, valuation, marking);
	else
	  transition.displayEdge (valuation, marking, printer);
	flagFatal ();
	return true;
      }
    }
    if (!myDest || myUpdate) {
      myStateBuf.deflate ();
      if (report (myStateBuf.getBuf (), myStateBuf.getNumBytes (),
		  rejected, transition.isHidden (valuation), 0))
	isNew = true;
      myStateBuf.inflate ();
    }
    if (!myPropBits)
      break;
    myStateBuf.remove (myPropBits);
  }
  while (--p > myPropSucc);

  return isNew;
}

void
StateSetReporter::reportError (bool deadlock)
{
  if (myDest)
    return; // reproducing a counterexample, not reporting an error
  deflate ();
  myStates.reject (mySrc, mySrcSize, *this, myFatal
		   ? (deadlock
		      ? StateSet::deadlockFatal
		      : StateSet::rejectFatal)
		   : (deadlock
		      ? StateSet::deadlockState
		      : StateSet::rejectState),
		   isReduced ());
  inflate ();
  if (error ())
    flagFatal ();
}

#ifdef EXPR_COMPILE
bool
StateSetReporter::report (const void* state,
			  size_t size,
			  bool rejected,
			  bool hidden)
{
  return report (state, size, rejected, hidden, 0);
}
#endif // EXPR_COMPILE

bool
StateSetReporter::report (const void* state,
			  size_t size,
			  bool rejected,
			  bool hidden,
			  unsigned pending)
{
  if (rejected || myPropReject) {
    if (!myDest) {
      myStates.reject (state, size, *this, myFatal
		       ? StateSet::rejectFatal
		       : StateSet::rejectState,
		       isReduced ());
      if (error ())
	flagFatal ();
    }
    return true;
  }
  bool status = addState (state, size, hidden);
  if (myThreshold) {
    const unsigned numArcs = myStates.getNumArcs ();
    if (!(numArcs % myThreshold)) {
      const unsigned numStates = myStates.getNumStates ();
      printer.print (numStates), printer.printRaw (" states, ");
      printer.print (numArcs), printer.printRaw (" arcs, ");
      printer.print (myStates.getNumPending ());
      if (pending)
	printer.delimiter ('+'), printer.print (pending);
      printer.printRaw (" pending");
      printer.finish ();
    }
  }
  return status;
}

void
StateSetReporter::reject (const void* dstate,
			  size_t dlen,
			  long offset,
			  bool reduced,
			  unsigned reason)
{
  myStates.setOffset (offset);
  myStates.reject (dstate, dlen, *this,
		   static_cast<enum StateSet::Code>(reason), reduced);
}

word_t*
StateSetReporter::pop (bool tail, size_t& size, long& offset)
{
  word_t* buf = myStates.pop (tail, size);
  offset = myStates.getOffset ();
  return buf;
}

void
StateSetReporter::setOffset (long offset)
{
  myStates.setOffset (offset);
}

void
StateSetReporter::reject ()
{
  if (!myDest)
    myStates.reject (mySrc, mySrcSize, *this,
		     StateSet::inconsistent, isReduced ());
}

void
StateSetReporter::displayPath (const word_t* src)
{
  assert (src && myDest);
  /** state spaces of the child nets (optional) */
  class FullSet* childset = initModules ();
  /** the synchronising state space */
  class SyncStates* sync = childset ? new class SyncStates (net) : 0;
  /** Flag: has the analysis been interrupted? */
  extern volatile bool interrupted;
  const unsigned numTr = childset
    ? net.getNumTransitions ()
    : net.getNumAllTransitions ();
  unsigned ps, i;
  class GlobalMarking m (net);

  // Initialize the context and fetch the source state
  ps = m.decode (*net.getInitMarking (), src, myPropBits);
 again:
  myFatal = false;
  if (myProp) {
    class Valuation valuation;
    valuation.setGlobalMarking (&m);
    myPropReject =
      !(*myProp)[ps].eval (valuation, myPropSucc, myProp->getFinalState ());
    if (myPropReject && !valuation.isOK ()) {
      assert (false);
      delete[] childset; delete sync;
      return;
    }
    assert (*myPropSucc > 0);
  }
  else
    myPropSucc = 0;

#ifndef NDEBUG
  mySrcDeadlock = true;
#endif // NDEBUG
  for (i = 0, myPriority = 0; !interrupted && !myFatal && i < numTr; i++) {
    const class Transition& t = net.getTransition (i);
    if ((!myPriority || t.getPriority () == myPriority) &&
	(!childset || !t.getNumChildren ()))
      t.analyze (m, *this);
    // synchronisation transitions (which have children) are analysed
    // by SyncStates::sync (), called via analyzeModules () below
  }
  if (childset)
    analyzeModules (m, *sync, childset);
  assert (i == numTr || interrupted || myFatal);
  if (!interrupted && !myFatal) {
    // path compression has eliminated the state; reconstruct it
    assert (!myPropSucc || *myPropSucc == 1);
    assert (!mySrcDeadlock);
    ps = myPropSucc ? myPropSucc[1] : 0;
    addEvents ();
    for (i = 0, myPriority = 0; !interrupted && !myFatal && i < numTr; i++) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
	  (!childset || !t.getNumChildren ()))
	t.analyze (m, *this);
    }
    assert (myFatal);
    goto again;
  }

  assert (interrupted || myFatal);
  delete[] childset; delete sync;
}