// Persistent reachability graph storage -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__

#include "Graph.h"
#include "LSTS.h"
#include "BTree.h"
#include "Net.h"
#include "Place.h"
#include "GlobalMarking.h"
#include "BitVector.h"
#include "util.h"

#include <stdlib.h> // abort(3)
#ifndef __WIN32
# include <sys/errno.h>
#endif // !__WIN32
#include <errno.h>

#include <list>

#ifdef USE_MMAP
# include <fcntl.h>
# ifdef __DECCXX
/** A qualifier for pointers to unaligned data */
#  define UNALIGNED __unaligned
# else // __DECCXX
/** A qualifier for pointers to unaligned data */
#  define UNALIGNED /*nothing*/
# endif // __DECCXX
# if defined __digital__
#  define fileno(f) ((f)->_file)
# endif // __digital__
# ifdef NO_MMAP
/** an empty file structure */
#  define NULL_F { 0, 0, 0 }
# else // NO_MMAP
/** an empty file structure */
#  define NULL_F { -1, 0, 0, 0 }
# endif // NO_MMAP
/** an empty file pointer */
static const file_t nofile = NULL_F;
/** empty file pointers */
static const struct Graph::files nofiles = { NULL_F, NULL_F, 0, NULL_F };
#else // USE_MMAP
# define UNALIGNED /*nothing*/
/** an empty file pointer */
static const file_t nofile = 0;
/** empty file pointers */
static const struct Graph::files nofiles = { 0, 0, 0, 0 };
#endif // USE_MMAP

/** @file Graph.C
 * Persistent, lossless reachability graph storage
 */

/* Copyright  1999-2003,2005 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. */

/** file offset to state directory slot
 * @param s	number of the state
 * @return	file offset of the corresponding directory slot
 */
#ifdef USE_MMAP
# define DIRSLOT1(s)				\
(reinterpret_cast<UNALIGNED Graph::fpos_t*>	\
 (static_cast<char*>(myFiles.directory.addr) +	\
  myDirectoryOffset) + 3 * (s))
#else // USE_MMAP
# define DIRSLOT1(s) (myDirectoryOffset + (s) * (3 * sizeof (Graph::fpos_t)))
#endif // USE_MMAP
/** file offset to the second component of a state directory slot
 * @param s	number of the state
 * @return	file offset to the second component of the slot
 */
#ifdef USE_MMAP
# define DIRSLOT2(s) (&DIRSLOT1 (s)[1])
#else // USE_MMAP
# define DIRSLOT2(s) (DIRSLOT1 (s) + sizeof (Graph::fpos_t))
#endif // USE_MMAP
/** file offset to the third component of a state directory slot
 * @param s	number of the state
 * @return	file offset to the second component of the slot
 */
#ifdef USE_MMAP
# define DIRSLOT3(s) (&DIRSLOT1 (s)[2])
#else // USE_MMAP
# define DIRSLOT3(s) (DIRSLOT1 (s) + 2 * sizeof (Graph::fpos_t))
#endif // USE_MMAP

#ifdef USE_MMAP
/** number of states */
# define myNumStates							\
(reinterpret_cast<UNALIGNED unsigned*>					\
 (static_cast<char*>(myFiles.directory.addr) + myDirectoryOffset)[-2])
/** number of arcs */
# define myNumArcs							\
(reinterpret_cast<UNALIGNED unsigned*>					\
 (static_cast<char*>(myFiles.directory.addr) + myDirectoryOffset)[-1])
#endif // USE_MMAP

/** File offset flag */
#define OFFSET_FLAG LONG_MIN
/** Determine whether an offset has been flagged
 * @param offset	offset to be checked
 * @return		whether the offset has the error bit set
 */
inline static bool
isFlagged (Graph::fpos_t offset)
{
  return offset & OFFSET_FLAG && true;
}

/** Flag an offset
 * @param state		offset to be flagged
 */
inline static void
flag (UNALIGNED Graph::fpos_t& offset)
{
  assert (!::isFlagged (offset));
  offset |= OFFSET_FLAG;
}

inline static Graph::fpos_t
getOffset (Graph::fpos_t offset)
{
  return offset & ~OFFSET_FLAG;
}
#undef OFFSET_FLAG


#ifdef NO_MMAP
/** pretend that mmapped files are always open */
# define isOpen(file) true
/** pretend to open a file */
# define openFile(name, cr) nofile
#else
/** Check if a file is open
 * @param file	the file
 * @return	true if the file has been opened
 */
static bool
isOpen (const file_t& file)
{
# ifdef USE_MMAP
  return file.fd >= 0;
# else // USE_MMAP
  return bool (file);
# endif // USE_MMAP
}

/** Open a file
 * @param name	the file name (optional)
 * @param cr	flag: create or truncate the file
 * @return	an opened file, or something on which isOpen() does not hold
 */
static file_t
openFile (const char* name, bool cr)
{
# ifdef USE_MMAP
  file_t f = nofile;
  if (name)
    f.fd = open (name, cr ? O_RDWR | O_CREAT | O_TRUNC : O_RDWR, 0666);
  else {
    FILE* file = tmpfile ();
    if (!file) {
      perror ("tmpfile");
      return nofile;
    }
    f.fd = dup (fileno (file));
    fclose (file);
    name = "(temporary)";
  }
  if (f.fd >= 0) {
    f.len = lseek (f.fd, 0, SEEK_END);
    for (f.alloc = 4096; f.alloc < f.len; ) {
      if (!(f.alloc *= 2)) {
	fputs (name, stderr), fputs (": file size overflow\n", stderr);
	abort ();
      }
    }
    if (ftruncate (f.fd, f.alloc)) {
      fputs (name, stderr), perror (": ftruncate");
      abort ();
    }
    f.addr =
#  ifdef __sun
      (caddr_t)
#  endif // __sun
      mmap (0, f.alloc, PROT_READ | PROT_WRITE, MAP_SHARED, f.fd, 0);
    if (f.addr == reinterpret_cast<void*>(MAP_FAILED)) {
      fputs (name, stderr), perror (": mmap");
      close (f.fd);
      return nofile;
    }
  }
  return f;
# else // USE_MMAP
  return name ? fopen (name, cr ? "wb+" : "rb+") : tmpfile ();
# endif // USE_MMAP
}
#endif // NO_MMAP

#ifdef USE_MMAP
size_t
Graph::getNumStates () const
{
  return myNumStates;
}

unsigned
Graph::getNumArcs () const
{
  return myNumArcs;
}
#endif // USE_MMAP

/** Close a file
 * @param file	the file
 */
static void
closeFile (file_t& file)
{
  assert (isOpen (file));
#ifdef USE_MMAP
# ifdef NO_MMAP
  if (file.addr)
    free (file.addr);
# else // NO_MMAP
  if (file.addr)
    munmap (file.addr, file.alloc);
  ftruncate (file.fd, file.len);
  close (file.fd);
# endif // NO_MMAP
#else // USE_MMAP
  fclose (file);
#endif // USE_MMAP
}

#ifdef USE_MMAP
/** Extend a file
 * @param file	the file
 */
static void
extend (file_t& file)
{
  assert (isOpen (file) && file.addr);
  if (file.len < file.alloc)
    return;
# ifndef NO_MMAP
  if (file.addr)
    munmap (file.addr, file.alloc);
# endif // !NO_MMAP
  while (file.alloc < file.len) {
    if (!(file.alloc *= 2)) {
      fputs ("extend: file size overflow\n", stderr);
      abort ();
    }
  }
# ifdef NO_MMAP
  if (!(file.addr = realloc (file.addr, file.alloc))) {
    perror ("extend: realloc");
    abort ();
  }
# else // NO_MMAP
  if (ftruncate (file.fd, file.alloc)) {
    perror ("extend: ftruncate");
    abort ();
  }
  file.addr =
#  ifdef __sun
    (caddr_t)
#  endif // __sun
    mmap (0, file.alloc, PROT_READ | PROT_WRITE, MAP_SHARED, file.fd, 0);
  if (file.addr == reinterpret_cast<void*>(MAP_FAILED)) {
    perror ("extend: mmap");
    abort ();
  }
# endif // NO_MMAP
}
#endif // USE_MMAP

/** Find and update an encoded state in the graph
 * @param myFiles		the graph files
 * @param myDirectoryOffset	offset to the state directory
 * @param buf			the encoded state to find or update
 * @param tmp			work storage for encoded states
 * @param bytes			length of the encoded state in bytes
 * @param number		number of the state to be searched
 * @return			whether the state was found
 */
static bool
update (const struct Graph::files& myFiles,
	Graph::fpos_t myDirectoryOffset,
	const void* buf,
#ifndef USE_MMAP
	void* tmp,
#endif // !USE_MMAP
	size_t bytes, card_t number)
{
  Graph::fpos_t num;
#ifdef USE_MMAP
  num = *DIRSLOT1 (number);
  assert (!bytes || getOffset (num) < myFiles.states.len);
  return !bytes ||
    (getOffset (num) + Graph::fpos_t (bytes) <= myFiles.states.len &&
     !memcmp (static_cast<char*>(myFiles.states.addr) + getOffset (num),
	      buf, bytes));
#else // USE_MMAP
  fseek (myFiles.directory, DIRSLOT1 (number), SEEK_SET);
  if (fread (&num, sizeof num, 1, myFiles.directory) != 1)
    assert (false);

  if (fseek (myFiles.states, getOffset (num), SEEK_SET)) {
    perror ("update (): fseek");
    abort ();
  }

  return
    fread (tmp, 1, bytes, myFiles.states) == bytes &&
    !memcmp (tmp, buf, bytes);
#endif // USE_MMAP
}

Graph::Graph (const class Net& net) :
  myNet (net),
  mySucc (new card_t[1]),
#ifndef USE_MMAP
  myNumArcs (0), myNumStates (0),
#endif // !USE_MMAP
  myStates (0), myFiles (nofiles),
  myDirectoryOffset (0), myFilename (0), myFilebase (0), myLSTS (0)
{
  *mySucc = 0;
}

Graph::Graph (const class Net& net,
	      const char* filename,
	      const char* filebase) :
  myNet (net),
  mySucc (new card_t[1]),
#ifndef USE_MMAP
  myNumArcs (0), myNumStates (0),
#endif // !USE_MMAP
  myStates (0),
  myFiles (nofiles),
  myDirectoryOffset (0), myFilename (0), myFilebase (0), myLSTS (0)
{
  *mySucc = 0;
  unsigned i;
  assert (filename || filebase);
  if (filename)
    myFilename = newString (filename);
  if (filebase)
    myFilebase = newString (filebase);
  else {
    // remove directory component
    for (i = 0; filename[i]; i++);
    while (i > 0 && filename[i - 1] != '/') i--;
    filebase = filename + i;

    // remove the last suffix starting with '.'
    for (i = 0; filebase[i]; i++);
    while (i > 0 && filebase[i] != '.') i--;
    if (!i) // no suffix
      for (i = 0; filebase[i]; i++);
    char* name = new char[i + 1];
    memcpy (name, filebase, i);
    name[i] = 0;
    myFilebase = name;
  }
}

Graph::~Graph ()
{
  if (isOpen (myFiles.directory)) {
    closeFile (myFiles.directory);
    closeFile (myFiles.states);
    fclose (myFiles.arcs);
    closeFile (myFiles.preds);
  }

  delete myStates;
  delete[] mySucc;
  delete[] myFilename;
  delete[] myFilebase;
  delete myLSTS;
}

bool
Graph::openFiles (bool regenerate)
{
  assert (!isOpen (myFiles.directory) && !isOpen (myFiles.states) &&
	  !myFiles.arcs && !isOpen (myFiles.preds));
  unsigned i = 0;
  if (myFilebase) while (myFilebase[i]) i++;

  /** flag: create or truncate the graph files */
  bool cr = !myFilebase || regenerate;

  {
    char* base = i ? new char[i + 5] : 0;
    memcpy (base, myFilebase, i);
    if (i) memcpy (base + i, ".rgh", 5);
    file_t f = openFile (base, cr);
#ifndef NO_MMAP
    if (isOpen (f))
      myStates = new class BTree (f);
    else if (!cr && myFilename && errno == ENOENT) {
      f = openFile (base, cr = true);
      if (isOpen (f))
	goto failRGH;
      myStates = new class BTree (f);
    }
    else {
    failRGH:
      perror (base);
      delete[] base;
      return false;
    }
#endif // !NO_MMAP

    if (i) memcpy (base + i, ".rgd", 5);
    myFiles.directory = openFile (base, cr);
    if (!isOpen (myFiles.directory)) {
      perror (base);
      delete myStates; myStates = 0;
      delete[] base;
      return false;
    }
    if (i) memcpy (base + i, ".rgs", 5);
    myFiles.states = openFile (base, cr);
    if (!isOpen (myFiles.states)) {
      perror (base);
      delete myStates; myStates = 0;
      closeFile (myFiles.directory); myFiles.directory = nofile;
      delete[] base;
      return false;
    }
    if (i) memcpy (base + i, ".rga", 5);
    if (!(myFiles.arcs = i ? fopen (base, cr ? "wb+" : "rb+") : tmpfile ())) {
      perror (base);
      delete myStates; myStates = 0;
      closeFile (myFiles.directory); myFiles.directory = nofile;
      closeFile (myFiles.states); myFiles.states = nofile;
      delete[] base;
      return false;
    }
    if (i) memcpy (base + i, ".rgp", 5);
    myFiles.preds = openFile (base, cr);
    if (!isOpen (myFiles.preds)) {
      perror (base);
      delete myStates; myStates = 0;
      closeFile (myFiles.directory); myFiles.directory = nofile;
      closeFile (myFiles.states); myFiles.states = nofile;
      fclose (myFiles.arcs); myFiles.arcs = 0;
      delete[] base;
      return false;
    }
    delete[] base;
  }

  static const char magic[] = "Maria-generated Reachability Graph of ";
  const size_t magiclen = (sizeof magic) - 1;

  if (!cr) {
    // check the magic cookie
#ifdef USE_MMAP
    if (myFiles.directory.len < fpos_t (magiclen)) {
    wrongFormatEOF:
      fprintf (stderr, "%s: premature EOF of graph directory\n",
	       myFilebase);
      goto wrongFormatNoEOF;
    }
    if (memcmp (myFiles.directory.addr, magic, magiclen)) {
    wrongFormatNoEOF:
      delete myStates; myStates = 0;
      closeFile (myFiles.directory); myFiles.directory = nofile;
      closeFile (myFiles.states); myFiles.states = nofile;
      fclose (myFiles.arcs); myFiles.arcs = 0;
      closeFile (myFiles.preds); myFiles.preds = nofile;
      return false;
    }
#else // USE_MMAP
    const size_t capacity = 4096;
    char* buf = new char[capacity];
    assert (capacity >= magiclen);

    if ((fread (buf, 1, magiclen, myFiles.directory) != magiclen) ||
	memcmp (buf, magic, magiclen)) {
      fprintf (stderr, "%s: graph: wrong magic cookie\n",
	       myFilebase);
    wrongFormat:
      if (feof (myFiles.directory))
	fprintf (stderr, "%s: premature EOF of graph directory\n",
		 myFilebase);
    wrongFormatNoEOF:
      delete myStates; myStates = 0;
      closeFile (myFiles.directory); myFiles.directory = nofile;
      closeFile (myFiles.states); myFiles.states = nofile;
      fclose (myFiles.arcs); myFiles.arcs = 0;
      closeFile (myFiles.preds); myFiles.preds = nofile;
      delete[] buf;
      return false;
    }
#endif // USE_MMAP

#ifdef USE_MMAP
    size_t got = myFiles.directory.len - magiclen;
    const char* buf = static_cast<char*>(myFiles.directory.addr) + magiclen;
#else // USE_MMAP
    size_t got = fread (buf, 1, capacity, myFiles.directory);
#endif // USE_MMAP
    size_t len;
    for (len = 0; len < got && buf[len]; len++);
    if (!len) {
      fprintf (stderr, "%s: graph: empty model name\n", myFilebase);
    argError:
      goto wrongFormatNoEOF;
    }
    else if (len == got) {
      fprintf (stderr, "%s: graph: model name is too long\n", myFilebase);
      goto argError;
    }

#ifndef USE_MMAP
    if (fseek (myFiles.directory, fpos_t (len) - got + 1, SEEK_CUR)) {
      fprintf (stderr, "%s: ", myFilebase);
      perror ("fseek");
      goto wrongFormatNoEOF;
    }
#endif // !USE_MMAP

    if (myFilename) {
      if (strcmp (buf, myFilename)) {
	fprintf (stderr, "%s: model names differ: \"%s\" \"%s\"\n",
		 myFilebase, buf, myFilename);
	goto argError;
      }
    }
    else
      myFilename = newString (buf);

#ifndef USE_MMAP
    delete[] buf; buf = 0;
#endif // !USE_MMAP

#ifdef USE_MMAP
    myDirectoryOffset = len + (magiclen + sizeof (fpos_t));
#else // USE_MMAP
    myDirectoryOffset = ftell (myFiles.directory) + (sizeof (fpos_t) - 1);
#endif // USE_MMAP
    myDirectoryOffset /= sizeof (fpos_t);
    myDirectoryOffset *= sizeof (fpos_t);

#ifdef USE_MMAP
    myDirectoryOffset += (sizeof myNumStates) + (sizeof myNumArcs);
    if (myDirectoryOffset >= myFiles.directory.len)
      goto wrongFormatEOF;
    fpos_t endpos = myFiles.directory.len;
#else // USE_MMAP
    fseek (myFiles.directory, myDirectoryOffset, SEEK_SET);
    myDirectoryOffset += (sizeof myNumStates) + (sizeof myNumArcs);

    if (fread (&myNumStates, sizeof myNumStates, 1, myFiles.directory) != 1 ||
	fread (&myNumArcs, sizeof myNumArcs, 1, myFiles.directory) != 1)
      goto wrongFormat;

    fseek (myFiles.directory, 0, SEEK_END);
    fpos_t endpos = ftell (myFiles.directory);
#endif // USE_MMAP

    if ((endpos - myDirectoryOffset) % (3 * sizeof (fpos_t)) ||
	(endpos - myDirectoryOffset) / (3 * sizeof (fpos_t)) != myNumStates) {
      fprintf (stderr, "%s.rgd: trying to ignore extra bytes at end of file\n",
	       myFilebase);
#ifdef USE_MMAP
      myFiles.directory.len = myDirectoryOffset +
	3 * sizeof (fpos_t) * myNumStates;
#endif // USE_MMAP
    }

    if (!myNumStates) {
      fprintf (stderr, "%s.rgd: no states\n", myFilebase);
      goto wrongFormatNoEOF;
    }
  }
  else { // create the directory afresh
#ifdef USE_MMAP
    assert (myFiles.directory.len == 0);
    const size_t len = i ? strlen (myFilename) + 1 : 0;
    myDirectoryOffset = len + (magiclen + sizeof (fpos_t) - 1 +
			       (sizeof myNumStates) + (sizeof myNumArcs));
    myDirectoryOffset /= sizeof (fpos_t);
    myDirectoryOffset *= sizeof (fpos_t);
    myFiles.directory.len = myDirectoryOffset;
    extend (myFiles.directory);
    memcpy (myFiles.directory.addr, magic, magiclen);
    memcpy (static_cast<char*>(myFiles.directory.addr) + magiclen,
	    myFilename, len);
    myNumStates = 0;
    myNumArcs = 0;
#else // USE_MMAP
    // magic cookie
    fwrite (magic, magiclen, 1, myFiles.directory);
    fwrite (myFilename, 1, i ? 1 + strlen (myFilename) : 0, myFiles.directory);
    myDirectoryOffset = ftell (myFiles.directory) + (sizeof (fpos_t) - 1);
    myDirectoryOffset /= sizeof (fpos_t);
    myDirectoryOffset *= sizeof (fpos_t);
    fseek (myFiles.directory, myDirectoryOffset, SEEK_SET);
    myDirectoryOffset += sizeof myNumStates;
    fwrite (&myNumStates, sizeof myNumStates, 1, myFiles.directory);
    myDirectoryOffset += sizeof myNumArcs;
    fwrite (&myNumArcs, sizeof myNumArcs, 1, myFiles.directory);
    assert (myDirectoryOffset == ftell (myFiles.directory));
    fflush (myFiles.directory);
#endif // USE_MMAP
  }

  return true;
}

void
Graph::setLSTS (class LSTS* lsts)
{
  delete myLSTS;
  myLSTS = lsts;
}

/** Compute a hash value for a sequence of bytes
 * @param buf		the sequence
 * @param bytes		number of bytes in the sequence
 */
inline static size_t
getHashValue (const unsigned char* buf, size_t bytes)
{
  size_t h = 0;
  while (bytes--)
    h ^= (h << 3 | h >> (CHAR_BIT - 3)) ^ buf[bytes];
  return h;
}

const class Graph::AddStatus
Graph::add (const void* buf,
	    size_t bytes)
{
  size_t h = getHashValue (reinterpret_cast<const unsigned char*>(buf), bytes);
  if (card_t* states = myStates->search (h)) {
#ifndef USE_MMAP
    word_t* tmp =
      new word_t[(bytes + (sizeof (word_t) - 1)) / sizeof (word_t)];
#endif // !USE_MMAP

    for (card_t s = *states; s; s--) {
      if (::update (myFiles, myDirectoryOffset, buf,
#ifndef USE_MMAP
		    tmp,
#endif // !USE_MMAP
		    bytes, states[s])) {
	s = states[s];
#ifndef USE_MMAP
	delete[] tmp;
#endif // !USE_MMAP
	delete[] states;
	return AddStatus (false, s);
      }
    }

#ifndef USE_MMAP
    delete[] tmp;
#endif // !USE_MMAP
    delete[] states;
  }

  // a new state: add it to disk
#ifdef USE_MMAP
  myFiles.directory.len += 3 * sizeof (fpos_t);
  extend (myFiles.directory);
  UNALIGNED fpos_t* const num = DIRSLOT1 (myNumStates);
  const fpos_t len = myFiles.states.len;
  num[0] = len;
  num[1] = num[2] = FPOS_NONE;

  myFiles.states.len += bytes;
  extend (myFiles.states);
  memcpy (static_cast<char*>(myFiles.states.addr) + len, buf, bytes);
  myStates->insert (h, myNumStates);
  return AddStatus (true, myNumStates++);
#else // USE_MMAP
  {
    fseek (myFiles.directory, DIRSLOT1 (myNumStates), SEEK_SET);
    if (fseek (myFiles.states, 0, SEEK_END))
      assert (false);
    fpos_t num[3];
    num[0] = ftell (myFiles.states);
    num[1] = num[2] = FPOS_NONE;
    if ((fwrite (num, sizeof num, 1, myFiles.directory) != 1) ||
	(fwrite (buf, 1, bytes, myFiles.states) != bytes)) {
    error:
      perror ("Graph::add (state): fwrite");
      abort ();
    }

    myStates->insert (h, myNumStates++);
    fseek (myFiles.directory, myDirectoryOffset -
	   (sizeof (myNumStates) + sizeof (myNumArcs)), SEEK_SET);
    if (1 != fwrite (&myNumStates, sizeof myNumStates, 1, myFiles.directory))
      goto error;

    return AddStatus (true, myNumStates - 1);
  }
#endif // USE_MMAP
}

card_t
Graph::lookup (const void* buf,
	       size_t bytes) const
{
  size_t h = getHashValue (reinterpret_cast<const unsigned char*>(buf),
			   bytes);
  if (card_t* states = myStates->search (h)) {
#ifndef USE_MMAP
    word_t* tmp =
      new word_t[(bytes + (sizeof (word_t) - 1)) / sizeof (word_t)];
#endif // !USE_MMAP

    for (card_t s = *states; s; s--) {
      if (::update (myFiles, myDirectoryOffset, buf,
#ifndef USE_MMAP
		    tmp,
#endif // !USE_MMAP
		    bytes, states[s])) {
	s = states[s];
#ifndef USE_MMAP
	delete[] tmp;
#endif // !USE_MMAP
	delete[] states;
	return s;
      }
    }

#ifndef USE_MMAP
    delete[] tmp;
#endif // !USE_MMAP
    delete[] states;
  }

  return CARD_T_MAX;
}

void
Graph::add (card_t source, card_t target)
{
  assert (!!mySucc);
  assert (source != CARD_T_MAX);
  assert (target != CARD_T_MAX);
  if (!(*mySucc & (*mySucc + 1))) {
    card_t* succ = new card_t[(*mySucc + 1) << 1];
    memcpy (succ, mySucc, (*mySucc + 1) * sizeof *succ);
    delete[] mySucc;
    mySucc = succ;
  }
  mySucc[++(*mySucc)] = target;
  addReverse (source, target);
}

/** Encode a number to a file using a variable-length code
 * @param file	the output file
 * @param num	the number to be encoded
 * @return	true if the operation succeeded
 */
static bool
encodeNumber (FILE* file, card_t num)
{
  char buf[4];
  unsigned len;
  // variable-length code:
  // 0..127		0xxxxxxx
  // 128..16511		10xxxxxxxxxxxxxx
  // 16512..1073758335	11xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
  if (num < 128)
    buf[0] = num, len = 1;
  else if ((num -= 128) < (1 << 14))
    buf[0] = 0x80 | (num >> 8), buf[1] = num, len = 2;
  else if ((num -= (1 << 14)) < (1 << 30)) {
    buf[3] = num;
    buf[2] = num >>= 8;
    buf[1] = num >>= 8;
    buf[0] = (num >> 8) | 0xc0;
    len = 4;
  }
  else
    return false;

  return len == fwrite (buf, 1, len, file);
}

/** Decode a number from a file using a variable-length code
 * @param file	the output file
 * @return	the decoded number
 */
static card_t
decodeNumber (FILE* file)
{
  unsigned char buf[4];
  if (1 != fread (buf, 1, 1, file)) {
  err:
    perror ("decodeNumber: fread");
    assert (false);
    return 0;
  }

  switch (*buf & 0xc0) {
  default:
    // 0..127
    return *buf;
  case 0x80:
    // 128..16511
    if (1 != fread (buf + 1, 1, 1, file))
      goto err;
    return 128 + ((static_cast<unsigned>(*buf & 0x3f) << 8) | buf[1]);
  case 0xc0:
    // 16512..1073758335
    if (3 != fread (buf + 1, 1, 3, file))
      goto err;
    return 16512 + ((static_cast<unsigned>(*buf & 0x3f) << 24) |
		    (static_cast<unsigned>(buf[1]) << 16) |
		    (static_cast<unsigned>(buf[2]) << 8) |
		    buf[3]);
  }
}

void
Graph::addEvents (card_t source,
		  const void* buf,
		  size_t bytes)
{
  assert (!isProcessed (source) && mySucc);
#ifdef USE_MMAP
  /** offset to the arc file */
  UNALIGNED fpos_t& arcoffset = *DIRSLOT2 (source);
  assert (arcoffset == FPOS_NONE);
#else // USE_MMAP
  /** offset to the arc file */
  fpos_t arcoffset;
#endif // USE_MMAP

  if (*mySucc) {
    if (myLSTS) {
      word_t* data = const_cast<word_t*>(static_cast<const word_t*>(buf));
      BitPacker::inflate (data[(bytes - 1) / sizeof (word_t)],
			  (-bytes) % sizeof (word_t));
      myLSTS->outputArcs (*this, source, mySucc, data);
      BitPacker::deflate (data[(bytes - 1) / sizeof (word_t)],
			  (-bytes) % sizeof (word_t));
    }
    fseek (myFiles.arcs, 0, SEEK_END);
    arcoffset = ftell (myFiles.arcs);

    if (!encodeNumber (myFiles.arcs, bytes) ||
	!encodeNumber (myFiles.arcs, *mySucc) ||
	(*mySucc != fwrite (mySucc + 1, sizeof *mySucc,
			    *mySucc, myFiles.arcs)) ||
	(bytes != fwrite (buf, 1, bytes, myFiles.arcs))) {
      perror ("Graph::add (event): fwrite");
      abort ();
    }
    *mySucc = 0;
  }
  else
    arcoffset = FPOS_DEAD;

  // update the directory file

#ifndef USE_MMAP
  fseek (myFiles.directory, DIRSLOT2 (source), SEEK_SET);
# ifndef NDEBUG
  {
    fpos_t arcpos;
    assert (1 == fread (&arcpos, sizeof arcpos, 1, myFiles.directory) &&
	    arcpos == FPOS_NONE);
    fseek (myFiles.directory, DIRSLOT2 (source), SEEK_SET);
  }
# endif // !NDEBUG
  fwrite (&arcoffset, sizeof arcoffset, 1, myFiles.directory);
  fseek (myFiles.directory, myDirectoryOffset - sizeof myNumArcs, SEEK_SET);
  fwrite (&myNumArcs, sizeof myNumArcs, 1, myFiles.directory);
#endif // !USE_MMAP
}

word_t*
Graph::fetchState (card_t number, size_t& length, bool* erroneous) const
{
  assert (number < myNumStates);
#ifdef USE_MMAP
  fpos_t num = *DIRSLOT1 (number);
#else // USE_MMAP
  fseek (myFiles.directory, DIRSLOT1 (number), SEEK_SET);
  fpos_t num;
  if (fread (&num, sizeof num, 1, myFiles.directory) != 1) {
  readError:
    perror ("Graph::fetchState (): fread");
    return 0;
  }
#endif // USE_MMAP
  if (erroneous)
    *erroneous = ::isFlagged (num);
  num = ::getOffset (num);
#ifdef USE_MMAP
  length = (number == myNumStates - 1
	    ? myFiles.states.len
	    : ::getOffset (*DIRSLOT1 (number + 1))) - num;
#else // USE_MMAP
  if (number == myNumStates - 1) {
    fseek (myFiles.states, 0, SEEK_END);
    length = ftell (myFiles.states) - num;
  }
  else {
    fpos_t pos;
    fseek (myFiles.directory, DIRSLOT1 (number + 1), SEEK_SET);
    if (fread (&pos, sizeof pos, 1, myFiles.directory) != 1)
      goto readError;
    length = ::getOffset (pos) - num;
  }

  if (fseek (myFiles.states, num, SEEK_SET)) {
    perror ("Graph::fetchState (): fseek");
    return 0;
  }
#endif // USE_MMAP

  unsigned numWords = (length + sizeof (word_t) - 1) / sizeof (word_t);
  word_t* buf = new word_t[numWords];
#ifdef USE_MMAP
  memcpy (buf, static_cast<char*>(myFiles.states.addr) + num, length);
#else // USE_MMAP
  if (fread (buf, 1, length, myFiles.states) != length) {
    delete[] buf;
    goto readError;
  }
#endif // USE_MMAP
  return buf;
}

class GlobalMarking*
Graph::fetchState (card_t number) const
{
  size_t length;
  bool erroneous;
  word_t* buf = fetchState (number, length, &erroneous);
  if (!buf)
    return 0;

  BitPacker::inflate (buf[(length - 1) / sizeof (word_t)],
		      (-length) % sizeof (word_t));
  // Decode the marking
  class GlobalMarking* marking = new class GlobalMarking (myNet);
  marking->decode (*myNet.getInitMarking (), buf);
  // Set the error bit
  if (erroneous)
    marking->flagErroneous ();
  delete[] buf;
  return marking;
}

card_t
Graph::getNumPredecessors (card_t state) const
{
  card_t num = 0;
  for (fpos_t pos = getPredecessors (state); pos != FPOS_NONE;
       getPredecessor (pos))
    num++;
  return num;
}

Graph::fpos_t
Graph::getPredecessors (card_t state) const
{
  assert (state < myNumStates);
#ifdef USE_MMAP
  return *DIRSLOT3 (state);
#else // USE_MMAP
  fseek (myFiles.directory, DIRSLOT3 (state), SEEK_SET);
  fpos_t pos;
  if (fread (&pos, sizeof pos, 1, myFiles.directory) != 1) {
    assert (false);
    return FPOS_NONE;
  }
  return pos;
#endif // USE_MMAP
}

card_t
Graph::getPredecessor (Graph::fpos_t& pos) const
{
  card_t state;
  assert (pos != FPOS_NONE);
#ifdef USE_MMAP
  assert (pos >= 0);
  assert (pos + fpos_t ((sizeof state) + (sizeof pos)) <= myFiles.preds.len);
  const char* buf = static_cast<char*>(myFiles.preds.addr);
  state = *reinterpret_cast<UNALIGNED const card_t*>(buf + pos);
  pos = *reinterpret_cast<UNALIGNED const fpos_t*>(buf + pos + sizeof state);
#else // USE_MMAP
  fseek (myFiles.preds, pos, SEEK_SET);
  if (fread (&state, sizeof state, 1, myFiles.preds) != 1 ||
      fread (&pos, sizeof pos, 1, myFiles.preds) != 1) {
    assert (false);
    pos = FPOS_NONE;
    return CARD_T_MAX;
  }
#endif // USE_MMAP
  assert (state < myNumStates);
  return state;
}

card_t*
Graph::getSuccessors (card_t state, word_t** data) const
{
  fpos_t pos;
  assert (state < myNumStates);
#ifdef USE_MMAP
  pos = *DIRSLOT2 (state);
#else // USE_MMAP
  fseek (myFiles.directory, DIRSLOT2 (state), SEEK_SET);
  if (fread (&pos, sizeof pos, 1, myFiles.directory) != 1) {
    assert (false);
    return 0;
  }
#endif // USE_MMAP
  if (pos == FPOS_DEAD || pos == FPOS_NONE)
    return 0;
  fseek (myFiles.arcs, pos, SEEK_SET);
  /** length of the encoded data */
  const size_t length = decodeNumber (myFiles.arcs);
  /** number of successor states */
  const card_t numSucc = decodeNumber (myFiles.arcs);
  assert (numSucc > 0);
  card_t* succ = new card_t[numSucc + 1];
  *succ = numSucc;
  if (fread (succ + 1, sizeof *succ, *succ, myFiles.arcs) != *succ) {
    assert (false);
    delete[] succ;
    return 0;
  }
  if (data) {
    if (!length)
      *data = 0;
    else {
      const unsigned numWords =
	(length + sizeof (word_t) - 1) / sizeof (word_t);
      word_t* buf = new word_t[numWords];
      if (fread (buf, 1, length, myFiles.arcs) != length) {
	assert (false);
	delete[] succ;
	delete[] buf;
	return 0;
      }
      BitPacker::inflate (buf[numWords - 1], (-length) % sizeof (word_t));
      *data = buf;
    }
  }
  return succ;
}

bool
Graph::eval (card_t state,
	     const class Expression* cond) const
{
  if (!cond)
    return true;
  class GlobalMarking* m = fetchState (state);
  bool accept = m->eval (*cond);
  delete m;
  return accept;
}

card_t*
Graph::toPath (const PathMap& tree,
	       card_t dest)
{
  card_t* p = new card_t[1];
  *p = 0;
  for (;;) {
    card_t* np = new card_t[++(*p) + 1];
    memcpy (np, p, *p * sizeof *p);
    delete[] p; p = np;
    p[*p] = dest;
    PathMap::const_iterator i = tree.find (dest);
    if (i == tree.end ()) break;
    dest = i->second;
  }
  return p;
}

card_t*
Graph::path (card_t state, card_t target,
	     const class Expression* pathc) const
{
  if (!eval (state, pathc) || !eval (target, pathc))
    return 0;
  /** Visited states */
  class BitVector visited (myNumStates);
  visited.assign (state, true);
  /** Search queue */
  std::list<card_t> sq;
  sq.push_front (CARD_T_MAX); /* mark for the next level */
  sq.push_back (state);
  /** Arcs in the explored graph (target, source) */
  PathMap p;

  for (;;) {
    if ((state = *sq.begin ()) == CARD_T_MAX) {
      sq.pop_front ();
      if (sq.empty ())
	return 0;
      sq.push_back (CARD_T_MAX);
      state = *sq.begin ();
    }
    sq.pop_front ();
    assert (!sq.empty ());
    assert (visited[state]);
    if (state == target)
      return toPath (p, target);
    if (card_t* succ = getSuccessors (state)) {
      for (assert (*succ > 0); *succ; (*succ)--) {
	card_t s = succ[*succ];
	if (!visited.tset (s) && eval (s, pathc)) {
	  sq.push_back (s);
	  p.insert (PathMap::value_type (s, state));
	}
      }
      delete[] succ;
    }
  }
}

card_t*
Graph::path (card_t state, const class Expression& cond,
	     const class Expression* pathc) const
{
  if (!eval (state, pathc))
    return 0;
  /** Visited states */
  class BitVector visited (myNumStates);
  visited.assign (state, true);
  /** Search queue */
  std::list<card_t> sq;
  sq.push_front (CARD_T_MAX); /* mark for the next level */
  sq.push_back (state);
  /** Arcs in the explored graph (target, source) */
  PathMap p;

  for (;;) {
    if ((state = *sq.begin ()) == CARD_T_MAX) {
      sq.pop_front ();
      if (sq.empty ())
	return 0;
      sq.push_back (CARD_T_MAX);
      state = *sq.begin ();
    }
    sq.pop_front ();
    assert (!sq.empty ());
    assert (visited[state]);
    if (eval (state, &cond))
      return toPath (p, state);
    if (card_t* succ = getSuccessors (state)) {
      for (assert (*succ > 0); *succ; (*succ)--) {
	card_t s = succ[*succ];
	if (!visited.tset (s) && eval (s, pathc)) {
	  sq.push_back (s);
	  p.insert (PathMap::value_type (s, state));
	}
      }
      delete[] succ;
    }
  }
}

card_t*
Graph::rpath (card_t state, const class Expression& cond,
	      const class Expression* pathc) const
{
  if (!eval (state, pathc))
    return 0;
  /** Visited states */
  class BitVector visited (myNumStates);
  visited.assign (state, true);
  /** Search queue */
  std::list<card_t> sq;
  sq.push_front (CARD_T_MAX); /* mark for the next level */
  sq.push_back (state);
  /** Arcs in the explored graph (target, source) */
  PathMap p;

  for (;;) {
    if ((state = *sq.begin ()) == CARD_T_MAX) {
      sq.pop_front ();
      if (sq.empty ())
	return 0;
      sq.push_back (CARD_T_MAX);
      state = *sq.begin ();
    }
    sq.pop_front ();
    assert (!sq.empty ());
    assert (visited[state]);
    if (eval (state, &cond))
      return toPath (p, state);
    for (fpos_t pos = getPredecessors (state); pos != FPOS_NONE;) {
      card_t s = getPredecessor (pos);
      if (!visited.tset (s) && eval (s, pathc)) {
	sq.push_back (s);
	p.insert (PathMap::value_type (s, state));
      }
    }
  }
}

card_t*
Graph::path (card_t state,
	     const card_t* loop,
	     const class Expression* pathc) const
{
  if (!eval (state, pathc))
    return 0;
  /** Visited states */
  class BitVector visited (myNumStates);
  visited.assign (state, true);
  /** Search queue */
  std::list<card_t> sq;
  sq.push_front (CARD_T_MAX); /* mark for the next level */
  sq.push_back (state);
  /** Arcs in the explored graph (target, source) */
  PathMap p;

  for (;;) {
    if ((state = *sq.begin ()) == CARD_T_MAX) {
      sq.pop_front ();
      if (sq.empty ())
	return 0;
      sq.push_back (CARD_T_MAX);
      state = *sq.begin ();
    }
    sq.pop_front ();
    assert (!sq.empty ());
    assert (visited[state]);
    for (const card_t* l = loop + *loop; l > loop; l--) {
      if (state == *l) {
	card_t* q = toPath (p, state);
	// append the loop to the p
	card_t* r = new card_t[*q + *loop];
	*r = *q + *loop - 1;
	memcpy (r + *loop, q + 1, *q * sizeof *q);
	delete[] q;
	q = r + *loop;
	const card_t* k = l;
	for (; l++ < loop + *loop; *--q = *l);
	for (l = loop + 1; l++ < k; *--q = *l);
	assert (q == r + 1);
	return r;
      }
    }
    if (card_t* succ = getSuccessors (state)) {
      for (assert (*succ > 0); *succ; (*succ)--) {
	card_t s = succ[*succ];
	if (!visited.tset (s) && eval (s, pathc)) {
	  sq.push_back (s);
	  p.insert (PathMap::value_type (s, state));
	}
      }
      delete[] succ;
    }
  }
}

bool
Graph::flagErroneous (card_t number)
{
  assert (number < myNumStates);
#ifdef USE_MMAP
  UNALIGNED fpos_t& num = *DIRSLOT1 (number);
#else // USE_MMAP
  fseek (myFiles.directory, DIRSLOT1 (number), SEEK_SET);
  fpos_t num;
  if (fread (&num, sizeof num, 1, myFiles.directory) != 1)
    assert (false);
#endif // USE_MMAP
  if (::isFlagged (num))
    return true;
  ::flag (num);
#ifndef USE_MMAP
  fseek (myFiles.directory, -sizeof num, SEEK_CUR);
  if (fwrite (&num, sizeof num, 1, myFiles.directory) != 1)
    assert (false);
#endif // !USE_MMAP
  return false;
}

bool
Graph::isErroneous (card_t number) const
{
  assert (number < myNumStates);
#ifdef USE_MMAP
  return ::isFlagged (*DIRSLOT1 (number));
#else // USE_MMAP
  fseek (myFiles.directory, DIRSLOT1 (number), SEEK_SET);
  fpos_t num;
  if (fread (&num, sizeof num, 1, myFiles.directory) != 1)
    assert (false);
  return ::isFlagged (num);
#endif // USE_MMAP
}

bool
Graph::isProcessed (card_t number) const
{
  fpos_t num;
  assert (number < myNumStates);
#ifdef USE_MMAP
  num = *DIRSLOT2 (number);
#else // USE_MMAP
  fseek (myFiles.directory, DIRSLOT2 (number), SEEK_SET);
  if (fread (&num, sizeof num, 1, myFiles.directory) != 1)
    assert (false);
#endif // USE_MMAP
  return num != FPOS_NONE;
}

void
Graph::addReverse (card_t source, card_t target)
{
  myNumArcs++;
#ifdef USE_MMAP
  UNALIGNED fpos_t& arcend = *DIRSLOT3 (target);
  const fpos_t arcoffset = arcend;
  const fpos_t len = myFiles.preds.len;
  arcend = myFiles.preds.len;
  myFiles.preds.len += (sizeof arcoffset) + (sizeof source);
  extend (myFiles.preds);
  char* buf = static_cast<char*>(myFiles.preds.addr) + len;
  *reinterpret_cast<UNALIGNED card_t*>(buf) = source;
  *reinterpret_cast<UNALIGNED fpos_t*>(buf + sizeof source) = arcoffset;
#else // USE_MMAP
  fpos_t arcoffset;
  fseek (myFiles.directory, DIRSLOT3 (target), SEEK_SET);
  if (1 != fread (&arcoffset, sizeof arcoffset, 1, myFiles.directory)) {
    perror ("Graph::addReverse (): fread");
    abort ();
  }
  fseek (myFiles.directory, -sizeof arcoffset, SEEK_CUR);
  fseek (myFiles.preds, 0, SEEK_END);
  fpos_t arcend = ftell (myFiles.preds);
  fwrite (&arcend, sizeof arcend, 1, myFiles.directory);
  fwrite (&source, sizeof source, 1, myFiles.preds);
  fwrite (&arcoffset, sizeof arcoffset, 1, myFiles.preds);
#endif // USE_MMAP
}