// Storage of encoded states -*- c++ -*-

/** @file StateSet.C
 * Set of reached states, represented with bit vectors
 */

/* 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 "StateSet.h"
#endif // __GNUC__
#include "FullSet.h"
#include "Printer.h"
#include "Net.h"
#include "Dotty.h"
#include "ByteBuffer.h"
#include "StateSetReporter.h"

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

bool
StateSet::openFile ()
{
  if (!(myPathFile = tmpfile ()))
    perror ("tmpfile");
  return !!myPathFile;
}

/** Display the reason for rejecting a state
 * @param reason	the reason for rejecting the state
 * @param printer	the output stream
 */
static void
printReason (enum StateSet::Code reason,
	     const class Printer& printer)
{
  switch (reason) {
  case StateSet::initialState:
  case StateSet::addStates:
    assert (false);
    break;
  case StateSet::deadlockState:
    printer.printRaw ("deadlock");
    break;
  case StateSet::deadlockFatal:
    printer.printRaw ("fatal deadlock");
    break;
  case StateSet::rejectState:
    printer.printRaw ("rejected state");
    break;
  case StateSet::rejectFatal:
    printer.printRaw ("fatally rejected state");
    break;
  case StateSet::propertyError:
    printer.printRaw ("property evaluation error");
    break;
  case StateSet::inconsistent:
    printer.printRaw ("inconsistent successor");
    break;
  }

  printer.finish ();
}

/** Read the file offsets to the counterexample trace
 * @param numOffset	(output) the length of the offset sequence
 * @param off		the offset to the path file
 * @param end		the end offset to the path file
 * @param f		the path file
 */
static unsigned*
readOffsets (unsigned& numOffsets,
	     long off,
	     long end,
	     FILE* f)
{
#ifndef NDEBUG
  assert (off < end);
  fseek (f, 0, SEEK_END);
  assert (end <= ftell (f));
#endif // NDEBUG
  numOffsets = 1;
  unsigned* offsets = new unsigned[1];
  if ((*offsets = off)) {
    unsigned char rbuf[8];
    class ByteUnpacker u (rbuf);
    do {
      fseek (f, offsets[numOffsets - 1], SEEK_SET);
      if (!(numOffsets & (numOffsets + 1))) {
	unsigned* o = new unsigned[(numOffsets + 1) << 1];
	memcpy (o, offsets, numOffsets * sizeof *offsets);
	delete[] offsets;
	offsets = o;
      }
      fread (rbuf, sizeof rbuf, 1, f);
      offsets[numOffsets] = u.extract (); u.buf = rbuf;
      assert (offsets[numOffsets] < offsets[numOffsets - 1]);
    }
    while (offsets[numOffsets++]);
  }
  return offsets;
}

void
StateSet::reject (const void* dstate,
		  size_t dlen,
		  const class StateSetReporter& reporter,
		  enum Code reason,
		  bool reduced) const
{
  assert (!!dstate);

  if (!myPathFile)
    return;

  reporter.displayPrologue ();
  ::printReason (reason, reporter.printer);

  if (reduced) {
    class FullSet states;
    if (!states.init (false)) {
      assert (false);
      return;
    }

    unsigned numOffsets;
    unsigned* offsets = ::readOffsets (numOffsets, myOffset,
				       myPathFileLength, myPathFile);
    const unsigned* o = offsets + numOffsets;
    size_t size = 0;
    word_t* state = 0;

    if (!reporter.net.getParent ())
      reporter.displayMarking (*reporter.net.getInitMarking ());
    else {
      // the first state on the path is the "initial" one: display it
      assert (numOffsets > 0); assert (!o[-1]);
      state = getState (*--o, &size);
      BitPacker::inflate (state[(size - 1) / sizeof (word_t)],
			  (-size) % sizeof (word_t));
      reporter.displayState (state);
    }

    for (const unsigned* o = offsets + numOffsets;
	 o-- > offsets && !interrupted; ) {
      delete[] state;
      state = getState (*o, &size);
      if (states.getNumStates ()) {
	BitPacker::inflate (state[(size - 1) / sizeof (word_t)],
			    (-size) % sizeof (word_t));
	class StateSetReporter recoverer (reporter, true, states, state,
					  1 + (size - 1) / sizeof (word_t));
	recoverer.analyze (StateReporter::Breadth);
	assert (recoverer.isFatal ());
	BitPacker::deflate (state[(size - 1) / sizeof (word_t)],
			    (-size) % sizeof (word_t));
	states.clear ();
      }
      if (!states.add (state, size))
	assert (false);
    }

    if (!interrupted && (dlen != size || memcmp (state, dstate, size))) {
      word_t* d1 = new word_t[(dlen + (sizeof (word_t) - 1)) /
			      sizeof (word_t)];
      memcpy (d1, dstate, dlen);
      BitPacker::inflate (d1[(dlen - 1) / sizeof (word_t)],
			  (-dlen) % sizeof (word_t));
      class StateSetReporter recoverer (reporter, true, states, d1,
					1 + (dlen - 1) / sizeof (word_t));
      recoverer.analyze (StateReporter::Breadth);
      assert (recoverer.isFatal ());
      delete[] d1;
    }

    delete[] state;
    delete[] offsets;
    fseek (myPathFile, myPathFileLength, SEEK_SET);
  }
  else
    displayPath (dstate, dlen, reporter);

  reporter.displayEpilogue ();
}

void
StateSet::displayPath (const void* dstate, size_t dlen,
		       const class StateSetReporter& reporter) const
{
  assert (!!dstate);
  if (!myPathFile)
    return;

  unsigned numOffsets;
  unsigned* offsets = ::readOffsets (numOffsets, myOffset,
				     myPathFileLength, myPathFile);
  const unsigned* o = offsets + numOffsets;
  word_t* s1 = 0;
  size_t size = 0;

  if (!reporter.net.getParent ())
    reporter.displayMarking (*reporter.net.getInitMarking ());
  else {
    // the first state on the path is the "initial" one: display it
    assert (numOffsets > 0); assert (!o[-1]);
    s1 = getState (*--o, &size);
    BitPacker::inflate (s1[(size - 1) / sizeof (word_t)],
			(-size) % sizeof (word_t));
    reporter.displayState (s1);
  }

  while (o-- > offsets && !interrupted) {
    word_t* state = getState (*o, &size);
    BitPacker::inflate (state[(size - 1) / sizeof (word_t)],
			(-size) % sizeof (word_t));
    if (s1) {
      reporter.displayPath (s1, state, 1 + (size - 1) / sizeof (word_t));
      delete[] s1;
    }
    s1 = state;
  }

  if (!interrupted) {
    word_t* d1 = new word_t[(dlen + (sizeof (word_t) - 1)) / sizeof (word_t)];
    memcpy (d1, dstate, dlen);
    const unsigned dwords = 1 + (dlen - 1) / sizeof (word_t);
    BitPacker::inflate (d1[dwords - 1], (-dlen) % sizeof (word_t));
    if (dlen != size || memcmp (s1, d1, dwords * sizeof (word_t)))
      reporter.displayPath (s1, d1, dwords);
    delete[] d1;
  }

  delete[] s1;
  delete[] offsets;
  fseek (myPathFile, myPathFileLength, SEEK_SET);
}

word_t*
StateSet::getState (long, size_t*) const
{
  assert (false);
  return 0;
}