// Property automaton -*- c++ -*-

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
# ifdef __sgi
#  define _POSIX_C_SOURCE 199309L
# endif
#endif // __GNUC__
#include "Property.h"

// #define DEBUG_AUTOMATON // to display the automaton on stdout

#ifdef BUILTIN_LTL
# include "LtlGraph.h"
# include <stdio.h>
#else // BUILTIN_LTL
# ifdef __WIN32
#  undef __STRICT_ANSI__
#  include <windows.h>
#  include <process.h>
#  include <fcntl.h>
#  undef pipe
#  define pipe(fds) _pipe (fds, 0, _O_TEXT | _O_NOINHERIT)
# endif // __WIN32
# ifdef __CYGWIN__
#  undef __STRICT_ANSI__
# endif // __CYGWIN__
# include <ctype.h>
# ifdef __DECCXX
#  include <sys/signal.h>
# else // __DECCXX
#  include <signal.h>
# endif // __DECCXX
#endif // BUILTIN_LTL
#include <stdlib.h>
#include <sys/types.h>
#include <unistd.h>

#ifndef unix
# if defined __unix||defined __unix__
#  define unix
# elif defined _AIX||defined __NetBSD__||defined __APPLE__
#  define unix
# endif
#endif

#if !defined BUILTIN_LTL && defined unix
#include <sys/wait.h>
/** Handle a child termination
 * @param pid		process number of the terminated child
 */
extern "C" void childterm (pid_t pid);
/** Handle a signal
 * @param num		number of the signal
 */
extern "C" void sig (int num);
#endif // !BUILTIN_LTL && unix

#include "PropertyState.h"
#include "Constant.h"
#include "BooleanBinop.h"
#include "NotExpression.h"
#include "LeafValue.h"
#include "BoolType.h"
#include "Net.h"

/** @file Property.C
 * Automaton representing the negation of a property being verified
 */

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

Property::Property () :
#ifdef BUILTIN_LTL
  myNegated (true),
#else // BUILTIN_LTL
  myFD (0),
#endif // BUILTIN_LTL
  myNumExprs (0), myExprs (0), myNumStates (0),
  myStates (0), myStatesAccept (0),
  myInitialState (UINT_MAX), myFinalState (UINT_MAX), myNumSets (0)
{
}

Property::~Property ()
{
  delete[] myExprs;
  delete[] myStates;
  delete myStatesAccept;
}

typedef std::map<unsigned,unsigned> NumberMap;

#ifdef BUILTIN_LTL
/** Translate a gate condition for a transition
 * @param gba		the generalized Bchi automaton
 * @param state		the state whose successor arcs are to be displayed
 * @param numProps	number of atomic propositions
 * @param props		atomic propositions
 * @param stateMap	map for state numbers
 * @param s		(output) the property state in the automaton
 */
static void
translateGates (const class LtlGraph& gba,
		unsigned state,
		unsigned numProps,
		class Expression** props,
		NumberMap& stateMap,
		class PropertyState& s)
{
  for (LtlGraph::const_iterator n = gba.begin (); n != gba.end (); n++) {
    if (n->second.m_incoming.find (state) ==
	const_cast<std::set<unsigned>&>(n->second.m_incoming).end ())
      continue;
    const class LtlBitVector& propositions = n->second.m_atomic;
    /** The gate expression */
    class Expression* gate = 0;
    std::pair<NumberMap::iterator, bool> p =
      stateMap.insert (NumberMap::value_type (n->first, stateMap.size ()));
# ifdef DEBUG_AUTOMATON
    fprintf (stdout, "%u ", p.first->second);
# endif // DEBUG_AUTOMATON

    for (unsigned i = propositions.nonzero (); i; ) {
      const class LtlAtom& atom =
	static_cast<const class LtlAtom&>(Ltl::fetch (i - 1));
      if (i) i = propositions.findNext (i);
      assert (atom.getValue () < numProps);
      class Expression* prop = props[atom.getValue ()]->copy ();
      if (atom.isNegated ())
	prop = NotExpression::construct (*prop);
# ifdef DEBUG_AUTOMATON
      if (i) fputs ("& ", stdout);
      fprintf (stdout, atom.isNegated () ? "! p%u " : "p%u ",
	       atom.getValue ());
# endif // DEBUG_AUTOMATON
      gate = gate
	? BooleanBinop::construct (true, *gate, *prop)
	: prop;
    }
# ifdef DEBUG_AUTOMATON
    if (!gate)
      putc ('t', stdout);
    putc ('\n', stdout);
# endif // DEBUG_AUTOMATON
    if (!gate)
      gate = (new class Constant
	      (*new class LeafValue (Net::getBoolType (), true)))->cse ();
    s.addSuccessor (p.first->second, *gate);
  }
# ifdef DEBUG_AUTOMATON
  fputs ("-1\n", stdout);
# endif // DEBUG_AUTOMATON
}

bool
Property::create (class Expression& expr)
{
  assert (myNegated && !myNumExprs && !myNumStates && !myNumSets);
  class Ltl* ltl = expr.toFormula (*this);
  assert (ltl);
  /** The generalized Bchi automaton */
  class LtlGraph gba (*ltl);
  /** acceptance set number and proposition */
  typedef std::pair<unsigned, const class Ltl*> acceptance_set_t;
  typedef std::map<const class Ltl*, acceptance_set_t> acceptance_map_t;
  acceptance_map_t acceptance_sets;

  /** iterator to states */
  LtlGraph::const_iterator s;

  // construct the acceptance sets
  for (s = gba.begin (); s != gba.end (); s++) {
    myNumStates++;
    const class LtlBitVector& temporal = s->second.m_old;
    for (unsigned i = temporal.nonzero (); i; ) {
      const class Ltl& f = Ltl::fetch (i - 1);
      switch (f.getKind ()) {
      case Ltl::Until:
	if (!static_cast<const class LtlUntil&>(f).isRelease ())
	  acceptance_sets.insert (std::pair<const class Ltl*,acceptance_set_t>
				  (&f, acceptance_set_t
				   (acceptance_sets.size (),
				    &static_cast<const class LtlUntil&>
				    (f).getRight ())));
	break;
      case Ltl::Future:
	if (static_cast<const class LtlFuture&>(f).getOp () ==
	    LtlFuture::finally)
	  acceptance_sets.insert (std::pair<const class Ltl*,acceptance_set_t>
				  (&f, acceptance_set_t
				   (acceptance_sets.size (),
				    &static_cast<const class LtlFuture&>
				    (f).getFormula ())));
	break;
      default:
	break;
      }
      if (i) i = temporal.findNext (i);
    }
  }

  if (!myNumStates++) {
    fputs ("the property automaton is empty: tautology?\n", stderr);
  semanticError:
    Ltl::clear ();
    delete[] myExprs;
    myNumExprs = 0, myExprs = 0;
    delete[] myStates;
    delete myStatesAccept;
    myNumStates = 0, myStates = 0, myStatesAccept = 0;
    myNegated = true, myInitialState = UINT_MAX, myNumSets = 0;
    return false;
  }

  myNumSets = acceptance_sets.size ();
  if (myNumSets && myNumStates >= UINT_MAX / myNumSets) {
    fprintf (stderr, "too many states and acceptance sets: %u,%u\n",
	     myNumStates, myNumSets);
    goto semanticError;
  }

  if (!(myStates = new class PropertyState[myNumStates])) {
    fprintf (stderr, "cannot allocate %u property automaton states\n",
	     myNumStates);
    goto semanticError;
  }

  if (myNumSets &&
      !(myStatesAccept = new class BitVector (myNumStates * myNumSets))) {
    fprintf (stderr, "cannot allocate %u*%u acceptance sets\n",
	     myNumStates, myNumSets);
    goto semanticError;
  }

# ifdef DEBUG_AUTOMATON
  fprintf (stdout, "%u %u\n0 1 -1\n", myNumStates, myNumSets);
# endif // DEBUG_AUTOMATON

  /** map from state numbers to a continuous sequence */
  NumberMap stateMap;
  stateMap.insert (NumberMap::value_type (0, 0));
  translateGates (gba, myInitialState = 0, myNumExprs, myExprs, stateMap,
		  myStates[0]);

  for (s = gba.begin (); s != gba.end (); s++) {
    const class LtlBitVector& temporal = s->second.m_old;
    /** mapped state number */
    std::pair<NumberMap::iterator, bool> p =
      stateMap.insert (NumberMap::value_type (s->first, stateMap.size ()));
# ifdef DEBUG_AUTOMATON
    printf ("%u 0", p.first->second);
# endif // DEBUG_AUTOMATON

    // determine the acceptance sets the state belongs to
    for (acceptance_map_t::iterator a = acceptance_sets.begin ();
	 a != acceptance_sets.end (); a++) {
      /** flag: does the state belong to the acceptance set? */
      bool accepting = true;

      for (unsigned i = temporal.nonzero (); i; ) {
	const class Ltl* f = &Ltl::fetch (i - 1);
	if (f == a->second.second) {
	  accepting = true;
	  break;
	}
	else if (f == a->first)
	  accepting = false;
	if (i) i = temporal.findNext (i);
      }

      if (accepting) {
# ifdef DEBUG_AUTOMATON
	fprintf (stdout, " %u", a->second.first);
# endif // DEBUG_AUTOMATON
	myStatesAccept->assign (p.first->second * myNumSets + a->second.first,
				true);
      }
    }

# ifdef DEBUG_AUTOMATON
    fputs (" -1\n", stdout);
# endif // DEBUG_AUTOMATON
    translateGates (gba, s->first, myNumExprs, myExprs, stateMap,
		    myStates[p.first->second]);
  }

  if (!myNumSets) {
    // no final state and 0 acceptance sets:
    // this is an infinite-word automaton whose all states accept
    if (!(myStatesAccept = new class BitVector (myNumStates))) {
      fprintf (stderr, "cannot allocate %u acceptance sets\n", myNumStates);
      goto semanticError;
    }
    myNumSets = 1;
    for (unsigned i = myNumStates; i--; )
      myStatesAccept->assign (i, true);
  }

  Ltl::clear ();
  return true;
}
#else // BUILTIN_LTL
/** Parse a gate condition for a transition
 * @param file		the input stream
 * @param numProps	number of atomic propositions
 * @param props		atomic propositions
 * @return		the parsed condition
 */
static class Expression*
parseGate (FILE* file, unsigned numProps, class Expression** props)
{
  int ch;
# ifdef DEBUG_AUTOMATON
  do
    ch = fgetc (file), fputc (ch, stdout);
  while (isspace (ch));
# else // DEBUG_AUTOMATON
  while (isspace (ch = fgetc (file)));
# endif // DEBUG_AUTOMATON
  switch (ch) {
  case 't':
  case 'f':
    return (new class Constant (*new class LeafValue (Net::getBoolType (),
						      ch == 't')))->cse ();
  case '!':
    if (class Expression* expr = parseGate (file, numProps, props))
      return NotExpression::construct (*expr);
    return 0;
  case '|':
  case '&':
  case 'i':
  case 'e':
    if (class Expression* l = parseGate (file, numProps, props)) {
      if (class Expression* r = parseGate (file, numProps, props)) {
	switch (ch) {
	case '|':
	  return BooleanBinop::construct (false, *l, *r);
	case '&':
	  return BooleanBinop::construct (true, *l, *r);
	case 'i':
	  return BooleanBinop::construct (false,
					 *NotExpression::construct (*l), *r);
	case 'e':
	  return BooleanBinop::construct
	    (false,
	     *BooleanBinop::construct (true, *l, *r),
	     *NotExpression::construct
	     (*BooleanBinop::construct (false, *l->copy (), *r->copy ())));
	}
      }
      l->destroy ();
    }
    return 0;
  case 'p':
    {
      unsigned num;
      if (1 != fscanf (file, "%u", &num))
	fputs ("error in proposition number\n", stderr);
      else if (num > numProps)
	fprintf (stderr, "unknown proposition p%u\n", num);
      else
	return
# ifdef DEBUG_AUTOMATON
	  fprintf (stdout, "%u", num),
# endif // DEBUG_AUTOMATON
	  props[num]->copy ();
    }
    return 0;
  case EOF:
    fputs ("unexpected end of file while parsing formula\n", stderr);
    return 0;
  default:
    fprintf (stderr, "unknown character 0x%02x", ch);
    return 0;
  }
}

bool
Property::create (const char* translator,
		  class Expression& expr)
{
  assert (translator && !myFD && !myNumExprs && !myNumStates);
  /** pipes for the formula and for the automaton */
  int pipe_formula[2], pipe_automaton[2];
  if (pipe (pipe_formula)) {
    perror ("pipe");
    return false;
  }
  if (pipe (pipe_automaton)) {
    perror ("pipe");
    close (pipe_formula[0]), close (pipe_formula[1]);
    return false;
  }
# if defined __WIN32
  /*
   * Since Windows does fork(2)/exec(2) in single pass, we have to
   * duplicate the file descriptors before executing the child process.
   */
  int old_in = _dup (STDIN_FILENO), old_out = _dup (STDOUT_FILENO);
  dup2 (pipe_formula[0], STDIN_FILENO);
  dup2 (pipe_automaton[1], STDOUT_FILENO);

  /* Create the child process */
  HANDLE pid = reinterpret_cast<HANDLE>
    (_spawnlp (_P_NOWAIT, translator, translator, 0));

  _dup2 (old_in, STDIN_FILENO), _dup2 (old_out, STDOUT_FILENO);
  close (old_in), close (old_out);

  if (!pid || pid == INVALID_HANDLE_VALUE) {
    perror (translator);
    close (pipe_formula[0]), close (pipe_formula[1]);
    close (pipe_automaton[0]), close (pipe_automaton[1]);
    return false;
  }
# elif defined unix
  signal (SIGCHLD, SIG_DFL);
  pid_t pid = fork ();
  if (!pid) {
    /* child process */
    dup2 (pipe_formula[0], STDIN_FILENO);
    dup2 (pipe_automaton[1], STDOUT_FILENO);
    close (pipe_formula[0]), close (pipe_formula[1]);
    close (pipe_automaton[0]), close (pipe_automaton[1]);
    setsid ();
    execlp (translator, translator, 0);
    perror (translator);
    exit (0);
  }
  else if (pid < 0) {
    perror ("fork");
    close (pipe_automaton[0]), close (pipe_automaton[1]);
    close (pipe_formula[0]), close (pipe_formula[1]);
    return false;
  }
# else
#  error "unsupported operating system"
# endif

  myFD = pipe_formula[1];
  close (pipe_formula[0]), close (pipe_automaton[1]);
  write (myFD, "!", 1);
  expr.toFormula (*this);
  close (myFD);
  myFD = 0;

  /** file handle for parsing the automaton */
  FILE* f = fdopen (pipe_automaton[0], "r");
  if (!f) {
    perror ("fdopen");
    close (pipe_automaton[0]);
    goto semanticError;
  }

  /** character read from the file */
  int ch;

# ifdef unix
  for (;;) {
    int status = 0;
    pid_t child = wait (&status);
    if (child == pid) {
      if (!status)
	break;
      fprintf (stderr, "%s returned %d\n", translator, status);
      goto statusError;
    }
    else if (child < 0) {
      perror ("wait");
    statusError:
      signal (SIGCHLD, sig);
      goto semanticError;
    }
    else
      childterm (pid);
  }

  signal (SIGCHLD, sig);
# endif // unix

  if (2 != fscanf (f, "%u%u", &myNumStates, &myNumSets)) {
  parseError:
    fputs ("error in translated automaton\n", stderr);
  semanticError:
# if defined __WIN32
    TerminateProcess (pid, 0);
# elif defined unix
    kill (pid, SIGKILL);
# endif // unix
    delete[] myExprs;
    myNumExprs = 0, myExprs = 0;
    delete[] myStates;
    delete myStatesAccept;
    myNumStates = 0, myStates = 0, myStatesAccept = 0;
    myInitialState = UINT_MAX, myNumSets = 0;
    if (f) fclose (f);
    return false;
  }

  if (!myNumStates) {
    fputs ("the property automaton is empty: tautology?\n", stderr);
    goto semanticError;
  }

  if (myNumSets && myNumStates >= UINT_MAX / myNumSets) {
    fprintf (stderr, "too many states and acceptance sets: %u,%u\n",
	     myNumStates, myNumSets);
    goto semanticError;
  }

  if (!(myStates = new class PropertyState[myNumStates])) {
    fprintf (stderr, "cannot allocate %u property automaton states\n",
	     myNumStates);
    goto semanticError;
  }
  if (myNumSets &&
      !(myStatesAccept = new class BitVector (myNumStates * myNumSets))) {
    fprintf (stderr, "cannot allocate %u*%u acceptance sets\n",
	     myNumStates, myNumSets);
    goto semanticError;
  }

  /** map from state numbers to a continuous sequence */
  NumberMap stateMap;
  /** map from acceptance set numbers to a continuous sequence */
  NumberMap setMap;

# ifdef DEBUG_AUTOMATON
  fprintf (stdout, "%u %u\n", myNumStates, myNumSets);
# endif // DEBUG_AUTOMATON

  for (unsigned i = myNumStates; i--; ) {
    unsigned num, initial;
    // state number and "initial state" flag
    if (2 != fscanf (f, "%u%u", &num, &initial) ||
	initial > unsigned (1 + !myNumSets))
      goto parseError;
    std::pair<NumberMap::iterator, bool> p =
      stateMap.insert (NumberMap::value_type (num, stateMap.size ()));

    // translated number of the state
    const unsigned state = p.first->second;

    if (myStates[state].getNumSuccessors ()) {
      fprintf (stderr, "redefinition of state %u\n", num);
      goto semanticError;
    }
    if (initial == 2) {
      if (myFinalState != UINT_MAX) {
	fprintf (stderr, "redefinition of final state as %u\n", num);
	goto semanticError;
      }
      myFinalState = state;
    }
    else if (initial) {
      if (myInitialState != UINT_MAX) {
	fprintf (stderr, "redefinition of initial state as %u\n", num);
	goto semanticError;
      }
      myInitialState = state;
    }

# ifdef DEBUG_AUTOMATON
    fprintf (stdout, "%u %u ", state, initial);
# endif // DEBUG_AUTOMATON

    // acceptance sets that the state belongs to
    for (;;) {
      while (isspace (ch = fgetc (f)));
      if (ch == '-') {
	if (1 != fscanf (f, "%u", &num) || 1 != num) {
	  fputs ("unexpected data after '-'\n", stderr);
	  goto semanticError;
	}
# ifdef DEBUG_AUTOMATON
	fputs ("-1\n", stdout);
# endif // DEBUG_AUTOMATON
	break;
      }
      ungetc (ch, f);
      if (!isdigit (ch) || 1 != fscanf (f, "%u", &num))
	goto parseError;

      p = setMap.insert (NumberMap::value_type (num, setMap.size ()));
      if (p.second && setMap.size () > myNumSets) {
	fprintf (stderr, "too many acceptance sets: set number %u\n", num);
	goto semanticError;
      }

# ifdef DEBUG_AUTOMATON
      fprintf (stdout, "%u ", p.first->second);
# endif // DEBUG_AUTOMATON
      myStatesAccept->assign (state * myNumSets + p.first->second, true);
    }

    // transitions
    for (;;) {
      while (isspace (ch = fgetc (f)));
      if (ch == '-') {
	if (1 != fscanf (f, "%u", &num) || 1 != num) {
	  fputs ("unexpected data after '-'\n", stderr);
	  goto semanticError;
	}
# ifdef DEBUG_AUTOMATON
	fputs ("-1\n", stdout);
# endif // DEBUG_AUTOMATON
	break;
      }
      ungetc (ch, f);
      if (!isdigit (ch) || 1 != fscanf (f, "%u", &num))
	goto parseError;

      p = stateMap.insert (NumberMap::value_type (num, stateMap.size ()));
      if (p.second && stateMap.size () > myNumStates) {
	fputs ("too many states\n", stderr);
	goto semanticError;
      }

# ifdef DEBUG_AUTOMATON
      fprintf (stdout, "%u", p.first->second);
# endif // DEBUG_AUTOMATON
      if (class Expression* e = ::parseGate (f, myNumExprs, myExprs)) {
	if (p.first->second == myFinalState) {
	  fputs ("ignoring transition from final state\n", stderr);
	  e->destroy ();
	}
	else
	  myStates[state].addSuccessor (p.first->second, *e);
      }
      else
	goto parseError;
# ifdef DEBUG_AUTOMATON
      fputc ('\n', stdout);
# endif // DEBUG_AUTOMATON
    }
  }

  while (isspace (ch = fgetc (f)));

  if (ch != EOF) {
    fputs ("extraneous non-whitespace data at end of input\n", stderr);
    goto semanticError;
  }

  if (!myNumSets && myFinalState == UINT_MAX) {
    // no final state and 0 acceptance sets:
    // this is an infinite-word automaton whose all states accept
    if (!(myStatesAccept = new class BitVector (myNumStates))) {
      fprintf (stderr, "cannot allocate %u acceptance sets\n", myNumStates);
      goto semanticError;
    }
    myNumSets = 1;
    for (unsigned i = myNumStates; i--; )
      myStatesAccept->assign (i, true);
  }

  fclose (f);
  return true;
}
#endif // BUILTIN_LTL

class Ltl*
Property::addConstant (bool b)
{
#ifdef BUILTIN_LTL
  return &LtlConstant::construct (b != myNegated);
#else // BUILTIN_LTL
  assert (myFD);
  write (myFD, b ? " t" : " f", 2);
  return 0;
#endif // BUILTIN_LTL
}

class Ltl*
Property::addUnop (enum Unop op,
		   class Expression& expr)
{
#ifdef BUILTIN_LTL
  if (op == opNot) myNegated = !myNegated;
  class Ltl* ltl = expr.toFormula (*this);
  if (op == opNot) myNegated = !myNegated;

  switch (op) {
  case opNot:
    break;
  case opFinally:
    ltl = &LtlFuture::construct (myNegated
				 ? LtlFuture::globally
				 : LtlFuture::finally, *ltl);
    break;
  case opGlobally:
    ltl = &LtlFuture::construct (myNegated
				 ? LtlFuture::finally
				 : LtlFuture::globally, *ltl);
    break;
  case opNext:
    ltl = &LtlFuture::construct (LtlFuture::next, *ltl);
    break;
  }
  return ltl;
#else // BUILTIN_LTL
  assert (myFD);
  switch (op) {
  case opNot:
    write (myFD, " !", 2);
    break;
  case opFinally:
    write (myFD, " F", 2);
    break;
  case opGlobally:
    write (myFD, " G", 2);
    break;
  case opNext:
    write (myFD, " X", 2);
    break;
  }
  return expr.toFormula (*this);
#endif // BUILTIN_LTL
}

class Ltl*
Property::addBinop (enum Binop op,
		    class Expression& left,
		    class Expression& right)
{
#ifdef BUILTIN_LTL
  class Ltl* l = left.toFormula (*this);
  class Ltl* r = right.toFormula (*this);
  switch (op) {
  case opAnd:
    return &LtlJunct::construct (!myNegated, *l, *r);
  case opOr:
    return &LtlJunct::construct (myNegated, *l, *r);
  case opRelease:
    return &LtlUntil::construct (!myNegated, *l, *r);
  case opUntil:
    return &LtlUntil::construct (myNegated, *l, *r);
  }
  assert (false);
  return 0;
#else // BUILTIN_LTL
  assert (myFD);
  switch (op) {
  case opAnd:
    write (myFD, " &", 2);
    break;
  case opOr:
    write (myFD, " |", 2);
    break;
  case opUntil:
    write (myFD, " U", 2);
    break;
  case opRelease:
    write (myFD, " V", 2);
    break;
  }
  left.toFormula (*this);
  right.toFormula (*this);
  return 0;
#endif // BUILTIN_LTL
}

class Ltl*
Property::addExpression (class Expression& expr)
{
#ifndef BUILTIN_LTL
  assert (myFD);
#endif // !BUILTIN_LTL
  unsigned i;
  for (i = 0; i < myNumExprs; i++)
    if (myExprs[i] == &expr)
      break;
  if (i == myNumExprs) {
    class Expression** exprs = new class Expression*[i + 1];
    assert (myExprs ? i : !i);
    if (myExprs) {
      memcpy (exprs, myExprs, i * sizeof *exprs);
      delete[] myExprs;
    }
    (myExprs = exprs)[myNumExprs++] = &expr;
  }
#ifdef BUILTIN_LTL
  return &LtlAtom::construct (i, myNegated);
#else // BUILTIN_LTL
  char num[23];
  write (myFD, num, snprintf (num, sizeof num, " p%u", i));
  return 0;
#endif // BUILTIN_LTL
}