// Graph of strongly connected components -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
# ifdef __sgi
#  define _XOPEN_SOURCE 1
#  define _XOPEN_SOURCE_EXTENDED 1
# endif // __sgi
#endif // __GNUC__
#include "ComponentGraph.h"
#include "Graph.h"
#include "BitVector.h"
#include <list>
#include <stdlib.h>
#include <errno.h>
#include <set>

#if defined __digital__
# define fileno(f) ((f)->_file)
#endif // __digital__

#if defined __CYGWIN__
# define fileno(f) __sfileno(f)
#endif // __CYGWIN__

/** @file ComponentGraph.C
 * Graph of strongly connected components
 */

/* Copyright  2000-2002,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. */

/** Tarjan state */
struct tarjan
{
  /** reachability graph state */
  card_t state;
  /** number of unprocessed successors */
  unsigned numSucc;
};

/** Stack for Tarjan's algorithm */
typedef std::list<struct tarjan> TarjanStack;

/** Component directory entry */
struct compdirent
{
  /** Number of states in the component */
  card_t numStates;
  /** Offset to the state numbers of the component (or FPOS_NONE) */
  Graph::fpos_t statePos;
  /** Offset to the successor arcs of the component (or FPOS_NONE) */
  Graph::fpos_t succPos;
  /** Offset to the first predecessor arc record (or FPOS_NONE) */
  Graph::fpos_t predPos;
};

/** Predecessor arc entry */
struct predent
{
  /** Offset to the next predecessor position (or FPOS_NONE) */
  Graph::fpos_t nextPos;
  /** Number of the predecessor component */
  card_t comp;
};

#ifdef NO_MMAP
/** an empty file structure */
# define NULL_F { 0, 0, 0 }
/** pretend that mmapped files are always open */
# define isOpen(file) true
#else // NO_MMAP
# ifdef USE_MMAP
/** an empty file structure */
#  define NULL_F { -1, 0, 0, 0 }
# else // USE_MMAP
/** an empty file structure */
#  define NULL_F 0
# endif // USE_MMAP
/** 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
}
#endif // NO_MMAP

/** an empty file pointer */
static const file_t nofile = NULL_F;

#ifdef USE_MMAP
# ifndef NO_MMAP
/** Open a temporary file
 * @param size	desired length of the file in bytes
 * @return	an opened file, or something on which isOpen() does not hold
 */
static file_t
tempFile (size_t size)
{
  FILE* file = tmpfile ();
  if (!file) {
    perror ("tmpfile");
    return nofile;
  }

  file_t f;
  f.fd = dup (fileno (file));
  fclose (file);
  if (f.fd < 0) {
    perror ("tempFile: dup");
    return nofile;
  }
  f.len = 0;
  f.alloc = size;
  if (ftruncate (f.fd, f.alloc)) {
    perror ("tempFile: ftruncate");
    close (f.fd);
    return nofile;
  }
  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)) {
    close (f.fd);
    perror ("tempFile: mmap");
    return nofile;
  }
  return f;
}
# endif // !NO_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

/** Close a temporary file
 * @param f	the file to be closed
 */
static void
closeFile (file_t& f)
{
#ifdef USE_MMAP
# ifdef NO_MMAP
  if (f.addr)
    free (f.addr);
# else // NO_MMAP
  munmap (f.addr, f.alloc);
  close (f.fd);
# endif // NO_MMAP
#else // USE_MMAP
  fclose (f);
#endif // USE_MMAP
}

ComponentGraph::ComponentGraph (const class Graph& graph) :
  myGraph (graph),
  myNumComponents (0), myNumTerminals (0),
  myStateComponents (nofile),
  myComponentDirectory (nofile), myComponentStates (0),
  mySuccComponents (0), myPredComponents (0)
{
}

ComponentGraph::~ComponentGraph ()
{
  if (isOpen (myStateComponents)) {
    assert (isOpen (myComponentDirectory));
    assert (myComponentStates && mySuccComponents && myPredComponents);
    closeFile (myStateComponents);
    closeFile (myComponentDirectory);
    fclose (myComponentStates);
    fclose (mySuccComponents);
    fclose (myPredComponents);
  }
}

inline bool
ComponentGraph::openFiles ()
{
  assert (!myNumComponents);
  assert (!isOpen (myStateComponents));
  assert (!isOpen (myComponentDirectory));
  assert (!myComponentStates);
  assert (!mySuccComponents);
  assert (!myPredComponents);
#ifdef USE_MMAP
  if (!isOpen (myStateComponents =
	       tempFile (myGraph.getNumStates () * sizeof (card_t))));
  else if (!isOpen (myComponentDirectory = tempFile (getpagesize ())))
    closeFile (myStateComponents), myStateComponents = nofile;
#else // USE_MMAP
  if (!(myStateComponents = tmpfile ()))
    perror ("tmpfile");
  else if (!(myComponentDirectory = tmpfile ()))
    perror ("tmpfile"),
      closeFile (myStateComponents), myStateComponents = nofile;
#endif // USE_MMAP
  else if (!(myComponentStates = tmpfile ()))
    perror ("tmpfile"),
      closeFile (myStateComponents), closeFile (myComponentDirectory),
      myStateComponents = myComponentDirectory = nofile;
  else if (!(mySuccComponents = tmpfile ()))
    perror ("tmpfile"),
      closeFile (myStateComponents), closeFile (myComponentDirectory),
      fclose (myComponentStates),
      myStateComponents = myComponentDirectory = nofile,
      myComponentStates = 0;
  else if (!(myPredComponents = tmpfile ()))
    perror ("tmpfile"),
      closeFile (myStateComponents), closeFile (myComponentDirectory),
      fclose (myComponentStates), fclose (mySuccComponents),
      myStateComponents = myComponentDirectory = nofile,
      myComponentStates = mySuccComponents = 0;
  else
    return true;
  return false;
}

inline void
ComponentGraph::setComponent (card_t state, card_t comp)
{
#ifdef USE_MMAP
  assert (size_t (myStateComponents.alloc) >= (state + 1) * sizeof state);
  reinterpret_cast<card_t*>(myStateComponents.addr)[state] = ++comp;
#else // USE_MMAP
  fseek (myStateComponents, state * sizeof state, SEEK_SET);
  fwrite (&++comp, sizeof comp, 1, myStateComponents);
#endif // USE_MMAP
}

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

inline void
ComponentGraph::computeArcs ()
{
  assert (myNumComponents);
  assert (!ftell (mySuccComponents) && !ftell (myPredComponents));
  /** successor and predecessor components */
  std::set<card_t> succComp, predComp;
  for (unsigned comp = 0; comp < myNumComponents; comp++) {
    card_t* states = getStates (comp);
    assert (states && *states);
    for (; *states; (*states)--) {
      card_t s;
      for (Graph::fpos_t pos = myGraph.getPredecessors (states[*states]);
	   pos != FPOS_NONE;) {
	s = getComponent (myGraph.getPredecessor (pos));
	if (s != CARD_T_MAX && s != comp)
	  predComp.insert (s);
      }
      if (card_t* succ = myGraph.getSuccessors (states[*states])) {
	for (assert (*succ > 0); *succ; (*succ)--) {
	  s = getComponent (succ[*succ]);
	  if (s != CARD_T_MAX && s != comp)
	    succComp.insert (s);
	}
	delete[] succ;
      }
    }
    delete[] states;
    if (succComp.empty ())
      myNumTerminals++;
#ifdef USE_MMAP
    struct compdirent& ent =
      reinterpret_cast<struct compdirent*>(myComponentDirectory.addr)[comp];
    assert (size_t (myComponentDirectory.len) >= (comp + 1) * sizeof ent);
#else // USE_MMAP
    struct compdirent ent;
    fseek (myComponentDirectory, comp * sizeof ent, SEEK_SET);
    if (1 != fread (&ent, sizeof ent, 1, myComponentDirectory))
      return;
#endif // USE_MMAP
    assert (ent.numStates &&
	    ent.statePos != FPOS_NONE &&
	    ent.succPos == FPOS_NONE &&
	    ent.predPos == FPOS_NONE);
    std::set<card_t>::const_iterator i;
    ent.succPos = ftell (mySuccComponents);
    for (i = succComp.begin (); i != succComp.end (); i++)
      fwrite (&*i, sizeof *i, 1, mySuccComponents);
    ent.predPos = ftell (myPredComponents);
    for (i = predComp.begin (); i != predComp.end (); i++)
      fwrite (&*i, sizeof *i, 1, myPredComponents);
#ifndef USE_MMAP
    fseek (myComponentDirectory, -sizeof ent, SEEK_CUR);
    fwrite (&ent, sizeof ent, 1, myComponentDirectory);
#endif // !USE_MMAP
    succComp.clear ();
    predComp.clear ();
  }
}

#ifndef USE_MMAP
/** Write a strongly connected component
 * @param compDirectory	stronly connected component directory
 * @param compStates	file containing the component state numbers
 * @param stateComps	map from state numbers to component numbers
 * @param visited	states that have been visited
 * @param processed	states that have been processed
 * @param st		the search stack
 * @param stsize	size of the search stack
 * @param root		number of the root state of the component
 * @param num		number of the component
 * @return		new size of the search stack
 */
inline unsigned
writeComponent (FILE* compDirectory,
		FILE* compStates,
		FILE* stateComps,
		class BitVector& visited,
		class BitVector& processed,
		const card_t* st,
		unsigned stsize,
		card_t root,
		unsigned num)
{
  struct compdirent c = {
    0,			// number of states
    ftell (compStates),	// offset to state numbers
    FPOS_NONE,		// offset to successor component numbers
    FPOS_NONE		// offset to predecessor component numbers
  };

  assert (stsize > 0);
  assert (card_t (ftell (compDirectory)) == num * sizeof c);
  assert (!processed[root] || !visited[root]);
  num++;
  unsigned i = stsize;
  while (i--) {
    card_t state = st[i];
    assert (!processed[state] || !visited[state]);
    fseek (stateComps, state * sizeof state, SEEK_SET);
    fwrite (&num, sizeof num, 1, stateComps);
    processed.assign (state, true);
    visited.assign (state, true);
    c.numStates++;
    if (state == root) break;
    assert (i > 0);
  }
  fwrite (st + i, sizeof *st, stsize - i, compStates);
  fwrite (&c, sizeof c, 1, compDirectory);
  return i;
}
#endif // !USE_MMAP

/** Write a strongly connected component
 * @param compDirectory	stronly connected component directory
 * @param compStates	file containing the component state numbers
 * @param stateComps	memory-based map from state to component numbers
 * @param visited	states that have been visited
 * @param processed	states that have been processed
 * @param st		the search stack
 * @param stsize	size of the search stack
 * @param root		number of the root state of the component
 * @param num		number of the component
 * @return		new size of the search stack
 */
inline unsigned
writeComponent (file_t& compDirectory,
		FILE* compStates,
		card_t* stateComps,
		class BitVector& visited,
		class BitVector& processed,
		const card_t* st,
		unsigned stsize,
		card_t root,
		unsigned num)
{
#ifdef USE_MMAP
  assert (card_t (compDirectory.len) == num * sizeof (struct compdirent));
  compDirectory.len += sizeof (struct compdirent);
  extend (compDirectory);
  struct compdirent& c =
    reinterpret_cast<struct compdirent*>(compDirectory.addr)[num];
#else // USE_MMAP
  struct compdirent c;
  assert (card_t (ftell (compDirectory)) == num * sizeof c);
#endif // USE_MMAP
  c.numStates = 0;
  c.statePos = ftell (compStates);
  c.succPos = c.predPos = FPOS_NONE;

  assert (stsize > 0);
  assert (!processed[root] || !visited[root]);
  num++;
  unsigned i = stsize;
  while (i--) {
    card_t state = st[i];
    assert (!processed[state] || !visited[state]);
    stateComps[state] = num;
    processed.assign (state, true);
    visited.assign (state, true);
    c.numStates++;
    if (state == root) break;
    assert (i > 0);
  }
  fwrite (st + i, sizeof *st, stsize - i, compStates);
#ifndef USE_MMAP
  fwrite (&c, sizeof c, 1, compDirectory);
#endif // !USE_MMAP
  return i;
}

unsigned
ComponentGraph::compute (card_t state,
			 const class Expression* cond)
{
  assert (!myNumComponents);
  if (!myGraph.eval (state, cond) || !openFiles ())
    return 0;
  /** Current and allocated length of the component stack */
  unsigned cstsize = 0, cstalloc = 128;
  /** Component stack */
  card_t* cst = new card_t[cstalloc];

  TarjanStack st;
  /** Visited states */
  class BitVector visited (myGraph.getNumStates ());
  /** States belonging to a component */
  class BitVector processed (myGraph.getNumStates ());
  // Combinations for	visited[state]	and	processed[state]:
  // initially			0			0
  // visited in the search	1			0
  // visited; depth adjusted	0			1
  // processed component	1			1

#ifdef USE_MMAP
  /** Search depth numbers or component numbers */
  card_t* const depths = reinterpret_cast<card_t*>(myStateComponents.addr);
#else // USE_MMAP
  /** Search depth numbers (if insufficient memory, use get/setComponent) */
  card_t* depths =
    reinterpret_cast<card_t*>(calloc (myGraph.getNumStates (),
				      sizeof *depths));
#endif // USE_MMAP

  /** Search depth */
  card_t depth = 1;
  /** Successor state numbers */
  card_t* succ;

  while (!interrupted) {
    // compute a strongly connected component
    while (!interrupted) {
      assert (!processed[state] || !visited[state]);
      if (processed[state] || visited.tset (state))
	break;
      // push the state on the component stack
      if (cstsize == cstalloc) {
	if (card_t* ncst = new card_t[cstalloc <<= 1]) {
	  memcpy (ncst, cst, cstsize * sizeof *cst);
	  delete[] cst; cst = ncst;
	}
	else {
	  delete[] cst;
#ifndef USE_MMAP
	  free (depths);
#endif // !USE_MMAP
	  interrupted = true;
	  return myNumComponents;
	}
      }
      cst[cstsize++] = state;

      // determine the successors of the state
      succ = myGraph.getSuccessors (state);
#ifndef USE_MMAP
      if (depths)
#endif // !USE_MMAP
	depths[state] = ++depth;
#ifndef USE_MMAP
      else
	setComponent (state, depth++);
#endif // !USE_MMAP
      struct tarjan t = { state, succ ? *succ : 0 };
      for (; t.numSucc; t.numSucc--) {
	card_t s = succ[t.numSucc];
	if (!(processed[s] && visited[s]) && myGraph.eval (s, cond)) {
	  state = s;
	  break;
	}
      }
      delete[] succ;
      st.push_front (t);
    }

    // backtrack
    while (!interrupted) {
      if (st.empty ()) {
#ifndef USE_MMAP
	if (depths) {
#endif // !USE_MMAP
	  if (cstsize &&
	      ::writeComponent (myComponentDirectory,
				myComponentStates,
				depths,
				visited, processed,
				cst, cstsize, *cst,
				myNumComponents++))
	    assert (false);
#ifndef USE_MMAP
	  fseek (myStateComponents, 0, SEEK_SET);
	  fwrite (depths, sizeof depths, myGraph.getNumStates (),
		  myStateComponents);
	  free (depths);
	}
	else
	  if (cstsize &&
	      ::writeComponent (myComponentDirectory,
				myComponentStates,
				myStateComponents,
				visited, processed,
				cst, cstsize, *cst,
				myNumComponents++))
	    assert (false);
#endif // !USE_MMAP
	delete[] cst;
	computeArcs ();
	return myNumComponents;
      }
      /** Minimum search depth in the state */
      const card_t minDepth = processed[state] && visited[state]
	? CARD_T_MAX
#ifdef USE_MMAP
	: depths[state] - 1;
#else // USE_MMAP
	: (depths ? (depths[state] - 1) : getComponent (state));
#endif // USE_MMAP
      struct tarjan& t = *st.begin ();
      state = t.state;
#ifndef USE_MMAP
      if (depths) {
#endif // !USE_MMAP
	if ((depths[state] - 1) > minDepth) {
	  depths[state] = minDepth + 1;
	  if (processed.tset (state))
	    assert (!visited[state]);
	  else
	    assert (visited[state]), visited.assign (state, false);
	}
#ifndef USE_MMAP
      }
      else {
	if (getComponent (state) > minDepth) {
	  setComponent (state, minDepth);
	  if (processed.tset (state))
	    assert (!visited[state]);
	  else
	    assert (visited[state]), visited.assign (state, false);
	}
      }
#endif // !USE_MMAP

      if (t.numSucc-- > 1) {
	succ = myGraph.getSuccessors (state);
	assert (succ && *succ > t.numSucc);
	for (; t.numSucc; t.numSucc--) {
	  card_t s = succ[t.numSucc];
	  if (!(processed[s] && visited[s]) && myGraph.eval (s, cond)) {
	    state = s;
	    break;
	  }
	}
	delete[] succ;
	if (t.numSucc)
	  break;
      }

      st.pop_front ();

      if (processed[state])
	continue;

#ifdef USE_MMAP
      cstsize = ::writeComponent (myComponentDirectory,
				  myComponentStates,
				  depths,
				  visited, processed,
				  cst, cstsize, state,
				  myNumComponents++);
#else // USE_MMAP
      cstsize = depths
	? ::writeComponent (myComponentDirectory,
			    myComponentStates,
			    depths,
			    visited, processed,
			    cst, cstsize, state,
			    myNumComponents++)
	: ::writeComponent (myComponentDirectory,
			    myComponentStates,
			    myStateComponents,
			    visited, processed,
			    cst, cstsize, state,
			    myNumComponents++);
#endif // USE_MMAP
    }
  }

  delete[] cst;
#ifndef USE_MMAP
  free (depths);
#endif // !USE_MMAP
  return myNumComponents;
}

card_t
ComponentGraph::getComponent (card_t state) const
{
#ifdef USE_MMAP
  assert (size_t (myStateComponents.alloc) >= (state + 1) * sizeof state);
  return reinterpret_cast<card_t*>(myStateComponents.addr)[state] - 1;
#else // USE_MMAP
  fseek (myStateComponents, state * sizeof state, SEEK_SET);
  return 1 == fread (&state, sizeof state, 1, myStateComponents)
    ? --state
    : CARD_T_MAX;
#endif // USE_MMAP
}

card_t*
ComponentGraph::getStates (card_t comp) const
{
  assert (comp < myNumComponents);
#ifdef USE_MMAP
  struct compdirent& c =
    reinterpret_cast<struct compdirent*>(myComponentDirectory.addr)[comp];
  if (size_t (myComponentDirectory.len) < (comp + 1) * sizeof c ||
      c.statePos == FPOS_NONE)
    return 0;
#else // USE_MMAP
  struct compdirent c;
  fseek (myComponentDirectory, comp * sizeof c, SEEK_SET);
  if (1 != fread (&c, sizeof c, 1, myComponentDirectory) ||
      c.statePos == FPOS_NONE)
    return 0;
#endif // USE_MMAP
  assert (c.numStates && c.numStates <= myGraph.getNumStates ());
  card_t* states = new card_t[c.numStates + 1];
  fseek (myComponentStates, c.statePos, SEEK_SET);
  if (c.numStates !=
      fread (states + 1, sizeof *states, c.numStates, myComponentStates)) {
    delete[] states;
    return 0;
  }
  *states = c.numStates;
  return states;
}

card_t
ComponentGraph::getNumSucc (card_t comp) const
{
  assert (comp < myNumComponents);
#ifdef USE_MMAP
  const struct compdirent* c =
    reinterpret_cast<struct compdirent*>(myComponentDirectory.addr) + comp;
  if (size_t (myComponentDirectory.len) < (comp + 1) * sizeof *c)
    return 0;
  if (c[0].succPos == FPOS_NONE)
    return CARD_T_MAX;
  if (size_t (myComponentDirectory.len) < (comp + 2) * sizeof *c) {
    fseek (mySuccComponents, 0, SEEK_END);
    return (ftell (mySuccComponents) - c[0].succPos) / sizeof (card_t);
  }
#else // USE_MMAP
  struct compdirent c[2];
  fseek (myComponentDirectory, comp * sizeof *c, SEEK_SET);
  switch (fread (c, sizeof *c, 2, myComponentDirectory)) {
  case 0:
    return 0;
  case 1:
    fseek (mySuccComponents, 0, SEEK_END);
    c[1].succPos = ftell (mySuccComponents);
    // fall through
  case 2:
    if (c[0].succPos == FPOS_NONE)
      return CARD_T_MAX;
  }
#endif // USE_MMAP
  assert (c[0].succPos <= c[1].succPos);
  return (c[1].succPos - c[0].succPos) / sizeof (card_t);
}

card_t
ComponentGraph::getNumPred (card_t comp) const
{
  assert (comp < myNumComponents);
#ifdef USE_MMAP
  const struct compdirent* c =
    reinterpret_cast<struct compdirent*>(myComponentDirectory.addr) + comp;
  if (size_t (myComponentDirectory.len) < (comp + 1) * sizeof *c)
    return 0;
  if (c[0].predPos == FPOS_NONE)
    return CARD_T_MAX;
  if (size_t (myComponentDirectory.len) < (comp + 2) * sizeof *c) {
    fseek (myPredComponents, 0, SEEK_END);
    return (ftell (myPredComponents) - c[0].predPos) / sizeof (card_t);
  }
#else // USE_MMAP
  struct compdirent c[2];
  fseek (myComponentDirectory, comp * sizeof *c, SEEK_SET);
  switch (fread (c, sizeof *c, 2, myComponentDirectory)) {
  case 0:
    return 0;
  case 1:
    fseek (myPredComponents, 0, SEEK_END);
    c[1].predPos = ftell (myPredComponents);
    // fall through
  case 2:
    if (c[0].predPos == FPOS_NONE)
      return CARD_T_MAX;
  }
#endif // USE_MMAP
  assert (c[0].predPos <= c[1].predPos);
  return (c[1].predPos - c[0].predPos) / sizeof (card_t);
}

card_t*
ComponentGraph::getSucc (card_t comp) const
{
  assert (comp < myNumComponents);
  Graph::fpos_t pos;
#ifdef USE_MMAP
  const struct compdirent* c =
    reinterpret_cast<struct compdirent*>(myComponentDirectory.addr) + comp;
  if (size_t (myComponentDirectory.len) < (comp + 1) * sizeof *c ||
      c[0].succPos == FPOS_NONE)
    return 0;
  if (size_t (myComponentDirectory.len) < (comp + 2) * sizeof *c) {
    fseek (mySuccComponents, 0, SEEK_END);
    pos = ftell (mySuccComponents);
  }
  else
    pos = c[1].succPos;
#else // USE_MMAP
  struct compdirent c[2];
  fseek (myComponentDirectory, comp * sizeof *c, SEEK_SET);
  switch (fread (c, sizeof *c, 2, myComponentDirectory)) {
  case 0:
    return 0;
  case 1:
    fseek (mySuccComponents, 0, SEEK_END);
    c[1].succPos = ftell (mySuccComponents);
    // fall through
  case 2:
    if (c[0].succPos == FPOS_NONE)
      return 0;
  }
  pos = c[1].succPos;
#endif // USE_MMAP
  assert (c[0].succPos <= pos);
  if (card_t numSucc = (pos - c[0].succPos) / sizeof (card_t)) {
    card_t* comps = new card_t[numSucc + 1];
    fseek (mySuccComponents, c[0].succPos, SEEK_SET);
    if (numSucc != fread (comps + 1, sizeof *comps,
			  numSucc, mySuccComponents)) {
      delete[] comps;
      return 0;
    }
    *comps = numSucc;
    return comps;
  }
  return 0;
}

card_t*
ComponentGraph::getPred (card_t comp) const
{
  assert (comp < myNumComponents);
  Graph::fpos_t pos;
#ifdef USE_MMAP
  const struct compdirent* c =
    reinterpret_cast<struct compdirent*>(myComponentDirectory.addr) + comp;
  if (size_t (myComponentDirectory.len) < (comp + 1) * sizeof *c ||
      c[0].predPos == FPOS_NONE)
    return 0;
  if (size_t (myComponentDirectory.len) < (comp + 2) * sizeof *c) {
    fseek (myPredComponents, 0, SEEK_END);
    pos = ftell (myPredComponents);
  }
  else
    pos = c[1].predPos;
#else // USE_MMAP
  struct compdirent c[2];
  fseek (myComponentDirectory, comp * sizeof *c, SEEK_SET);
  switch (fread (c, sizeof *c, 2, myComponentDirectory)) {
  case 0:
    return 0;
  case 1:
    fseek (myPredComponents, 0, SEEK_END);
    c[1].predPos = ftell (myPredComponents);
    // fall through
  case 2:
    if (c[0].predPos == FPOS_NONE)
      return 0;
  }
  pos = c[1].predPos;
#endif // USE_MMAP
  assert (c[0].predPos <= pos);
  if (card_t numPred = (pos - c[0].predPos) / sizeof (card_t)) {
    card_t* comps = new card_t[numPred + 1];
    fseek (myPredComponents, c[0].predPos, SEEK_SET);
    if (numPred != fread (comps + 1, sizeof *comps,
			  numPred, myPredComponents)) {
      delete[] comps;
      return 0;
    }
    *comps = numPred;
    return comps;
  }
  return 0;
}

card_t*
ComponentGraph::path (card_t state, card_t comp,
		      const class Expression* pathc) const
{
  if (!myGraph.eval (state, pathc))
    return 0;
  /** Visited states */
  class BitVector visited (myGraph.getNumStates ());
  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) */
  Graph::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 (getComponent (state) == comp)
      return Graph::toPath (p, state);
    if (card_t* succ = myGraph.getSuccessors (state)) {
      for (assert (*succ > 0); *succ; (*succ)--) {
	card_t s = succ[*succ];
	if (!visited.tset (s) && myGraph.eval (s, pathc)) {
	  sq.push_back (s);
	  p.insert (Graph::PathMap::value_type (s, state));
	}
      }
      delete[] succ;
    }
  }
}

card_t*
ComponentGraph::rpath (card_t state, card_t comp,
		       const class Expression* pathc) const
{
  if (!myGraph.eval (state, pathc))
    return 0;
  /** Visited states */
  class BitVector visited (myGraph.getNumStates ());
  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) */
  Graph::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 (getComponent (state) == comp)
      return Graph::toPath (p, state);
    for (Graph::fpos_t pos = myGraph.getPredecessors (state);
	 pos != FPOS_NONE;) {
      card_t s = myGraph.getPredecessor (pos);
      if (!visited.tset (s) && myGraph.eval (s, pathc)) {
	sq.push_back (s);
	p.insert (Graph::PathMap::value_type (s, state));
      }
    }
  }
}