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

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

#ifdef __GNUC__
# pragma implementation "StateReporter.h"
#endif // __GNUC__

#include "StateSetReporter.h"
#include "States.h"
#include "Net.h"
#include "Transition.h"
#include "Valuation.h"
#include "GlobalMarking.h"
#include "FullSet.h"
#include "SyncStates.h"
#ifdef EXPR_COMPILE
# include "Compilation.h"
# include "Printer.h"
#endif // EXPR_COMPILE

/** Flag: has the analysis been interrupted? */
volatile bool interrupted = false;

StateReporter::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) :
#ifdef EXPR_COMPILE
  myCompilation (compilation),
#endif // EXPR_COMPILE
  net (net_), printer (printer_),
  myMaxErrors (maxerrors), myNumErrors (0), myNumLocal (0),
  myEnabled (net.getNumEnabled ()
	     ? new char[net.getNumEnabled ()]
	     : 0),
  mySync (0),
  myFatal (false), mySrcDeadlock (true),
  myPriority (0), myStateBuf (), mySrc (0), mySrcSize (0),
  myFlattened (flattened),
  myLocal (local ? new class FullSet () : 0),
  mySuppressed (compress ? new class States () : 0),
  mySuccessors (None), myMinSize (size_t (-1L)), myMaxSize (0)
{
  if (net.getNumEnabled ())
    memset (myEnabled, 0, net.getNumEnabled ());
  if (myLocal && !myLocal->init (true)) {
    delete myLocal;
    *const_cast<class FullSet**>(&myLocal) = 0;
  }
}

StateReporter::StateReporter (const class StateReporter& old) :
#ifdef EXPR_COMPILE
  myCompilation (old.myCompilation),
#endif // EXPR_COMPILE
  net (old.net), printer (old.printer),
  myMaxErrors (old.myMaxErrors), myNumErrors (0), myNumLocal (0),
  myEnabled (net.getNumEnabled ()
	     ? new char[net.getNumEnabled ()]
	     : 0),
  mySync (0),
  myFatal (false), mySrcDeadlock (true),
  myPriority (0), myStateBuf (), mySrc (0), mySrcSize (0),
  myFlattened (old.myFlattened),
  myLocal (old.myLocal ? new class FullSet () : 0),
  mySuppressed (old.mySuppressed ? new class States () : 0),
  mySuccessors (None), myMinSize (size_t (-1L)), myMaxSize (0)
{
  if (net.getNumEnabled ())
    memset (myEnabled, 0, net.getNumEnabled ());
  if (myLocal && !myLocal->init (true)) {
    delete myLocal;
    *const_cast<class FullSet**>(&myLocal) = 0;
  }
}

StateReporter::~StateReporter ()
{
  delete[] myEnabled;
  delete[] mySrc;
  delete mySuppressed;
  delete myLocal;
}

void
StateReporter::enabled (const class Transition& transition)
{
  assert (!myPriority || transition.getPriority () == myPriority);
  mySrcDeadlock = false;
  myPriority = transition.getPriority ();
}

#ifdef EXPR_COMPILE
/** Report an encoded state
 * @param buf	the encoded state
 * @param size	length of the encoded state, in bytes
 * @param err	errNone if the state is not rejected
 * @param tr	the number of the transition that fired
 * @param ftr	the number of the transition in the flattened net
 * @param hide	flag: is the transition hidden?
 * @param ctx	the call-back context
 */
static void
addState (const void* buf, size_t size, enum Error err,
	  unsigned tr, unsigned ftr, int hide, void* ctx)
{
  class StateReporter& reporter = *static_cast<class StateReporter*>(ctx);
  if (err && err != errComp)
    reporter.flagFatal ();
  reporter.addState (buf, size, err != errNone, hide,
		     reporter.isFlattened () ? ftr : tr);
}

/** Report a potential synchronisation state
 * @param tr	the number of the transition that fired
 * @param ctx	the call-back context
 */
static void
syncState (unsigned tr, void* ctx)
{
  class StateReporter& reporter = *static_cast<class StateReporter*>(ctx);
  reporter.reportSync (reporter.net.getTransition (tr));
}

void
StateReporter::analyze (const class Transition& transition)
{
  if (unsigned errors =
      myCompilation->eventAnalyze (transition.getRootIndex (),
				   this, myEnabled)) {
    enabled (transition);
    reject ();
    printer.printQuoted (transition.getName ());
    printer.delimiter (':');
    printer.print (errors);
    printer.printRaw (errors == 1 ? " error" : " errors");
    printer.finish ();
  }
}

void
StateReporter::addState (const void* buf, size_t size,
			 bool rejected, bool hidden, unsigned tr)
{
  const class Transition& t = net.getTransition (tr);
  enabled (t);
  report (buf, size, rejected, hidden);
}
#endif // EXPR_COMPILE

void
StateReporter::analyze (enum SearchKind kind)
{
#ifdef EXPR_COMPILE
  if (myCompilation) {
    myCompilation->linkAddState (&::addState);
    myCompilation->linkReporter (&::syncState, isGraph (), myFlattened);
    myCompilation->getFatal () = &myFatal;
    myCompilation->getFlattened () = myFlattened;
  }
#endif // EXPR_COMPILE
  if (myFlattened)
    analyzeFlattened (kind);
  else
    analyzeModular (kind);
}

void
StateReporter::analyzeFlattened (enum SearchKind kind)
{
  assert (myFlattened);
  const unsigned numTr = net.getNumAllTransitions ();
#ifdef EXPR_COMPILE
  if (myCompilation) {
    while (!interrupted && !myFatal) {
      if (!popCompiled (kind == Breadth))
	break;
      mySrcDeadlock = true, myPriority = 0;
      for (unsigned i = 0; !interrupted && !myFatal && i < numTr; i++) {
	const class Transition& t = net.getTransition (i);
	if (!myPriority || t.getPriority () == myPriority)
	  analyze (t);
      }
      if (mySrcDeadlock && !interrupted && !myFatal) {
	switch (myCompilation->stateDeadlock (net.getIndex ())) {
	case errNone:
	  break;
	default:
	  myFatal = true;
	  // fall through
	case errComp:
	  reportError (true);
	}
      }
      if (suppress ())
	continue;
      addEvents ();
      if (kind >= Single)
	break;
    }
    return;
  }
#endif // EXPR_COMPILE
  while (!interrupted && !myFatal) {
    class GlobalMarking* m = pop (kind == Breadth);
    if (!m)
      break;
    mySrcDeadlock = true, myPriority = 0;
    for (unsigned i = 0; !interrupted && !myFatal && i < numTr; i++) {
      const class Transition& t = net.getTransition (i);
      if (!t.getNumParents () &&
	  (!myPriority || t.getPriority () == myPriority))
	t.analyze (*m, *this);
    }
    if (mySrcDeadlock && !interrupted && !myFatal) {
      switch (net.isDeadlock (*m, true)) {
      case Net::OK:
	break;
      case Net::Fatal:
	myFatal = true;
	// fall through
      case Net::Error:
	reportError (true);
      }
    }
    delete m;
    if (suppress ())
      continue;
    addEvents ();
    if (kind >= Single)
      break;
  }
}

void
StateReporter::analyzeModular (enum SearchKind kind)
{
  assert (!myFlattened);
  /** state spaces of the child nets */
  class FullSet* childset = initModules ();
  /** the synchronising state space */
  class SyncStates* sync = childset ? new class SyncStates (net) : 0;
  unsigned i;
  const unsigned numTr = net.getNumTransitions ();
  while (!interrupted && !myFatal) {
    class GlobalMarking* m =
#ifdef EXPR_COMPILE
      myCompilation ? 0 :
#endif // EXPR_COMPILE
      pop (kind == Breadth);
    if (
#ifdef EXPR_COMPILE
	myCompilation ? !popCompiled (kind == Breadth) :
#endif // EXPR_COMPILE
	!m)
      break;
    mySrcDeadlock = true, myPriority = 0;
    for (i = 0; !interrupted && !myFatal && i < numTr; i++) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
	  !t.getNumChildren ()) {
#ifdef EXPR_COMPILE
	if (myCompilation)
	  analyze (t);
	else
#endif // EXPR_COMPILE
	  t.analyze (*m, *this);
      }
      // synchronisation transitions (which have children) are analysed
      // by SyncStates::sync (), called via analyzeModules () below
    }
    if (childset) {
#ifdef EXPR_COMPILE
      if (myCompilation)
	analyzeModules (*sync, childset);
      else
#endif // EXPR_COMPILE
	analyzeModules (*m, *sync, childset);
    }

    if (mySrcDeadlock && !interrupted && !myFatal) {
#ifdef EXPR_COMPILE
      if (myCompilation) {
	switch (myCompilation->stateDeadlock (net.getIndex ())) {
	case errNone:
	  break;
	default:
	  myFatal = true;
	  // fall through
	case errComp:
	  reportError (true);
	}
      } else
#endif // EXPR_COMPILE
      switch (net.isDeadlock (*m, false)) {
      case Net::OK:
	break;
      case Net::Fatal:
	myFatal = true;
	// fall through
      case Net::Error:
	reportError (true);
      }
    }

    delete m;
    if (suppress ())
      continue;
    addEvents ();
    if (kind >= Single)
      break;
  }
  for (i = net.getNumChildren(); i--; )
    myNumLocal += childset[i].getNumStates ();

  delete[] childset;
  delete sync;
}

class FullSet*
StateReporter::initModules () const
{
  unsigned i = myFlattened ? 0 : net.getNumChildren ();
  class FullSet* childset = i ? new class FullSet[i] : 0;
  while (i--) {
    if (!childset[i].init (false)) {
      assert (false);
      delete[] childset;
      return 0;
    }
  }
  return childset;
}

void
StateReporter::analyzeModules (const class GlobalMarking& m,
			       class SyncStates& sync,
			       class FullSet* childset)
{
  assert (net.getNumChildren () > 0);
  unsigned i;

  // analyze child state spaces
  for (i = net.getNumChildren (); !interrupted && !myFatal && i--; ) {
    const class Net& child = net.getChild (i);
    childset[i].clear ();
    m.encode (myStateBuf, child);
#ifdef SYNC_CACHE
    if (sync.lookup (i, myStateBuf.getBuf (), myStateBuf.getNumWords ()))
      continue; // the modular state has already been analyzed
#endif // SYNC_CACHE
    myStateBuf.deflate ();
    if (!childset[i].add (myStateBuf.getBuf (), myStateBuf.getNumBytes ()))
      assert (false); // this should be a new state
    // to do: support safety-LTL property checking for the modules
    class StateSetReporter reporter (
#ifdef EXPR_COMPILE
				     myCompilation,
#endif
				     child, printer, 0, false, false, false,
				     0, 0, false, childset[i], 0);
    reporter.mySync = &sync;
    reporter.analyzeModular (Breadth);
    // to do: report the error graphically, show step from mySrc to myStateBuf
    if (reporter.myFatal)
      myFatal = true;
    if (reporter.getNumErrors ())
      reportError (false);
    myNumLocal += reporter.myNumLocal;
  }

  // find out enabled synchronisation transitions and synchronise
  for (i = net.getNumTransitions (); i--; ) {
    const class Transition& t = net.getTransition (i);
    if ((!myPriority || t.getPriority () == myPriority) &&
	t.getNumChildren ())
      sync.sync (m, t, *this);
  }

#ifndef SYNC_CACHE
  sync.cleanup ();
#endif // !SYNC_CACHE
}

#ifdef EXPR_COMPILE
void
StateReporter::analyzeModules (class SyncStates& sync,
			       class FullSet* childset)
{
  assert (net.getNumChildren () > 0);
  assert (!!myCompilation);
  unsigned i = net.getNumChildren ();
  word_t** srcs = new word_t*[i];

  // analyze child state spaces
  for (; !interrupted && !myFatal && i--; ) {
    const class Net& child = net.getChild (i);
    childset[i].clear ();
    unsigned bytes;
    const void* buf =
      myCompilation->stateProject (child.getIndex (), 0, 0, bytes);
    word_t* data = const_cast<word_t*>(static_cast<const word_t*>(buf));
    unsigned numWords = bytes ? (bytes - 1) / sizeof (word_t) + 1 : 0;
    /* back up the source state */
    BitPacker::inflate (data[numWords - 1], (-bytes) % sizeof (word_t));
    srcs[i] = bytes ? new word_t[numWords] : 0;
    memcpy (srcs[i], data, numWords * sizeof (word_t));
#ifdef SYNC_CACHE
    if (sync.lookup (i, data, numWords))
      continue; // the modular state has already been analyzed
#endif // SYNC_CACHE
    BitPacker::deflate (data[numWords - 1], (-bytes) % sizeof (word_t));
    if (!childset[i].add (buf, bytes))
      assert (false); // this should be a new state

    // to do: support safety-LTL property checking for the modules
    class StateSetReporter reporter (myCompilation,
				     child, printer, 0, false, false, false,
				     0, 0, false, childset[i], 0);
    reporter.mySync = &sync;
    reporter.analyzeModular (Breadth);
    /* restore the source state */
    myCompilation->stateDecode (child.getIndex (), srcs[i], 0);
    // to do: report the error graphically, show step from mySrc to myStateBuf
    if (reporter.myFatal)
      myFatal = true;
    if (reporter.getNumErrors ())
      reportError (false);
    myNumLocal += reporter.myNumLocal;
  }

  // find out enabled synchronisation transitions and synchronise
  for (i = net.getNumTransitions (); i--; ) {
    const class Transition& t = net.getTransition (i);
    if ((myPriority && t.getPriority () != myPriority) ||
	!t.getNumChildren ())
      continue;
    sync.sync (t, *this, srcs);
  }

  for (i = net.getNumChildren (); i--; )
    delete[] srcs[i];
  delete[] srcs;

# ifndef SYNC_CACHE
  sync.cleanup ();
# endif // !SYNC_CACHE
}

void
StateReporter::sync (const class Transition& transition)
{
  assert (transition.getNumChildren () > 0);
  unsigned bytes;
  const void* buf = myCompilation->stateProject
    (transition.getNet ()->getIndex (), 0, 0, bytes);
  unsigned numWords = (bytes - 1) / sizeof (word_t) + 1;
  word_t* s = numWords ? new word_t[numWords] : 0;
  memcpy (s, buf, bytes);
  BitPacker::inflate (s[numWords - 1], (-bytes) % sizeof (word_t));
  setSyncSource (s, bytes);
  analyze (transition);
}
#endif // EXPR_COMPILE

bool
StateReporter::suppress ()
{
  if (myLocal && myLocal->getNumStates ())
    return true;
  if (mySuppressed) {
    switch (mySuccessors) {
    case One:
      return true;
    case Many:
      if (const size_t num = mySuppressed->size ()) {
	const struct States::state& s = (*mySuppressed)[num - 1];
	do_addState (s.buf, s.size);
	mySuccessors = None;
      }
      // fall through
    case None:
      mySuppressed->clear ();
    }
  }
  return false;
}

bool
StateReporter::report (const class Transition& transition,
		       const class Valuation& valuation,
		       const class GlobalMarking& marking)
{
  card_t errorplace;
  assert (valuation.isOK ());
  enabled (transition);
  if (myEnabled) transition.logEnabled (valuation, myEnabled);
  if (marking.encode (myStateBuf, *net.getInitMarking (), &errorplace)) {
    enum Net::Status status = net.isReject (marking, myFlattened);
    switch (status) {
    case Net::OK:
      break;
    case Net::Fatal:
      flagFatal ();
      // fall through
    case Net::Error:
      break;
    }
    return report (transition, valuation, marking, status != Net::OK);
  }

  assert (!!net.getPlace (errorplace));
  reject (transition, valuation, marking, 0, net.getPlace (errorplace));
  return true;
}

void
StateReporter::reportSync (const class Transition& transition)
{
  assert (mySync && transition.getNumParents ());
  assert (!myFlattened);
  enabled (transition);
  mySync->add (transition, mySrc,
	       (mySrcSize + (sizeof (word_t) - 1)) / sizeof (word_t));
}

bool
StateReporter::addState (const void* state,
			 size_t size,
			 bool hidden)
{
  if (size > myMaxSize) myMaxSize = size;
  if (size < myMinSize) myMinSize = size;
  if (hidden && myLocal)
    return myLocal->add (state, size), false; // local state suppressed
  if (!mySuccessors && mySuppressed && mySuppressed->size () &&
      mySuppressed->add (state, size))
    return mySuccessors = One, false; // path compression applied
  mySuccessors = Many;
  return do_addState (state, size);
}

word_t*
StateReporter::popState (bool tail)
{
  delete[] mySrc;
  if (myLocal) {
    if ((mySrc = myLocal->pop (tail, mySrcSize)))
      return mySrc;
    if (myLocal->getNumStates ())
      addEvents ();
    myLocal->clear ();
  }
  if (mySuppressed) {
    if (const size_t num = mySuppressed->size ()) {
      const struct States::state& s = (*mySuppressed)[num - 1];
      switch (mySuccessors) {
      case One:
	mySrc = new word_t[1 + (s.size - 1) / sizeof (word_t)];
	memcpy (mySrc, s.buf, mySrcSize = s.size);
	mySuccessors = None;
	return mySrc;
      case Many:
	do_addState (s.buf, s.size);
	mySuccessors = None;
	// fall through
      case None:
	mySuppressed->clear ();
      }
    }
  }
  if ((mySrc = do_popState (tail, mySrcSize)) && mySuppressed)
    if (!mySuppressed->add (mySrc, mySrcSize))
      assert (false);
  return mySrc;
}

void
StateReporter::addEvents ()
{
}

void
StateReporter::reject (const class Transition& transition,
		       const class Valuation& valuation,
		       const class GlobalMarking& marking,
		       const char* reason,
		       const class Place* place)
{
  if (valuation.getError () == errFatal)
    flagFatal ();
  reject ();
  transition.report (valuation, marking, reason, place, printer);
  enabled (transition);
}