Logo Search packages:      
Sourcecode: maria version File versions

Transition.C

Go to the documentation of this file.
// Transition class -*- c++ -*-

/** @file Transition.C
 * Transition in an algebraic system net
 */

/* Copyright © 1998-2003 Marko Mäkelä (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. */

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "Transition.h"
#include "Place.h"
#include "Arc.h"
#include "Constant.h"
#include "Undefined.h"
#include "VariableDefinition.h"
#include "VariableSet.h"
#include "LeafValue.h"
#include "Token.h"
#include "GlobalMarking.h"
#include "Valuation.h"
#include "Substitution.h"
#include "BooleanBinop.h"
#include "Function.h"
#include "Quantifier.h"
#include "Printer.h"
#include "DummyReporter.h"
#include "Net.h"
#include "Search.h"
#include "LNet.h"
#include "BitVector.h"
#include "Variable.h"
#include "PlaceContents.h"
#include "Property.h"

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

/** Check for unacceptable valuations and clear the errors
 * @param status  default return value
 * @param transition    the transition
 * @param valuation     valuation to be checked
 * @param marking the marking being processed
 * @param reporter      object for reporting found states and errors
 * @param reason  reason for failure (optional)
 * @return        status, or false if there is an error in the valuation
 */
static bool
00070 willDo (bool status,
      const class Transition& transition,
      class Valuation& valuation,
      const class GlobalMarking& marking,
      class StateReporter& reporter,
      const char* reason = 0)
{
  if (!valuation.isOKorVar () || reason) {
    status = false;
    reporter.reject (transition, valuation, marking, reason, 0);
  }

  valuation.clearErrors ();
  return status;
}

/** Augment the valuation with initial assignments to output variables
 * @param transition    the transition
 * @param valuation     the valuation
 * @param marking the marking being processed
 * @param reporter      object for reporting found states and errors
 * @return        true if the operation succeeded
 */
static bool
00094 firstOutput (const class Transition& transition,
           class Valuation& valuation,
           const class GlobalMarking& marking,
           class StateReporter& reporter)
{
  if (const class QuantifierList* vars = transition.getOutputVariables ()) {
    switch (vars->augment (valuation)) {
    case Quantifier::pass:
      return true;
    case Quantifier::fail:
      switch (vars->advance (valuation)) {
      case Quantifier::pass:
      return true;
      case Quantifier::fail:
      willDo (false, transition, valuation, marking, reporter,
            "empty output:");
      vars->clear (valuation);
      return false;
      case Quantifier::undefined:
      break;
      }
      // fall through
    case Quantifier::undefined:
      willDo (false, transition, valuation, marking, reporter,
            "first output:");
      vars->clear (valuation);
      return false;
    }
  }
  return true;
}

/** Iterate to the next assignment to output variables
 * @param transition    the transition
 * @param valuation     the valuation
 * @param marking the marking being processed
 * @param reporter      object for reporting found states and errors
 * @return        true if a new valuation was generated
 */
static bool
00134 nextOutput (const class Transition& transition,
          class Valuation& valuation,
          const class GlobalMarking& marking,
          class StateReporter& reporter)
{
  if (const class QuantifierList* vars = transition.getOutputVariables ()) {
    switch (vars->advance (valuation)) {
    case Quantifier::pass:
      return true;
    case Quantifier::undefined:
      willDo (false, transition, valuation, marking, reporter,
            "iterating output:");
      // fall through
    case Quantifier::fail:
      vars->clear (valuation);
      break;
    }
  }
  return false;
}

/** Fire the output arcs of a transition
 * @param transition    the transition
 * @param valuation     the transition instance
 * @param marking the state (input/output parameter)
 * @param reporter      object for reporting found states and errors
 */
static void
00162 fireOutputs (const class Transition& transition,
           class Valuation& valuation,
           class GlobalMarking& marking,
           class StateReporter& reporter)
{
  assert (valuation.isOK ());

  for (unsigned out = 0; out < transition.getNumOutputs (); out++) {
    const class Arc& arc = transition.getOutput (out);
    class PlaceMarking& place = marking[reporter.isFlattened ()
                              ? arc.getPlace ().getIndex ()
                              : arc.getIndex ()];
    if (!arc.getExpr ().add (place, 1, valuation)) {
      willDo (false, transition, valuation, marking, reporter, "firing:");
      return;
    }
  }

  reporter.report (transition, valuation, marking);
}

00183 Transition::Transition () :
  myNet (0), myLocalIndex (0), myRootIndex (0), myName (0),
  myNumParents (0), myParents (0), myNumChildren (0), myChildren (0),
  myPriority (0), myKind (tNormal),
  myNumInputs (0), myInputs (0), myNumOutputs (0), myOutputs (0),
  myOutputMarking (false), myUnif (0),
  myNumWeaklyFair (0), myNumStronglyFair (0), myNumEnabled (0),
  myWeaklyFairCond (0), myStronglyFairCond (0), myEnabledCond (0),
  myWeaklyFairSet (0), myStronglyFairSet (0), myEnabledSet (0),
  myGates (), myHide (0),
  myOutputVariables (0), myVariables (), myFunctions (),
  myNumConstants (0), myConstantNames (0), myConstants (0)
{
}

00198 Transition::Transition (class Net& net,
                  unsigned i,
                  char* name) :
  myNet (&net), myLocalIndex (i), myRootIndex (i), myName (name),
  myNumParents (0), myParents (0), myNumChildren (0), myChildren (0),
  myPriority (0), myKind (tNormal),
  myNumInputs (0), myInputs (0), myNumOutputs (0), myOutputs (0),
  myOutputMarking (false), myUnif (0),
  myNumWeaklyFair (0), myNumStronglyFair (0), myNumEnabled (0),
  myWeaklyFairCond (0), myStronglyFairCond (0), myEnabledCond (0),
  myWeaklyFairSet (0), myStronglyFairSet (0), myEnabledSet (0),
  myGates (), myHide (0),
  myOutputVariables (0), myVariables (), myFunctions (),
  myNumConstants (0), myConstantNames (0), myConstants (0)
{
}

00215 Transition::~Transition ()
{
  delete[] myName;
  delete[] myChildren;
  delete[] myParents;

  while (myNumInputs)
    delete myInputs[--myNumInputs];
  delete[] myInputs;

  while (myNumOutputs)
    delete myOutputs[--myNumOutputs];
  delete[] myOutputs;

  for (struct unif* u; (u = myUnif); myUnif = u) {
    u = u->next;
    delete myUnif->vars;
    delete myUnif;
  };

  while (myNumWeaklyFair)
    myWeaklyFairCond[--myNumWeaklyFair]->destroy ();
  delete[] myWeaklyFairCond;
  delete[] myWeaklyFairSet;

  while (myNumStronglyFair)
    myStronglyFairCond[--myNumStronglyFair]->destroy ();
  delete[] myStronglyFairCond;
  delete[] myStronglyFairSet;

  while (myNumEnabled)
    myEnabledCond[--myNumEnabled]->destroy ();
  delete[] myEnabledCond;
  delete[] myEnabledSet;

  for (GateList::iterator g = myGates.begin (); g != myGates.end (); g++)
    (*g)->destroy ();

  myHide->destroy ();

  for (FunctionMap::iterator f = myFunctions.begin ();
       f != myFunctions.end (); f++)
    delete f->second;

  if (myOutputVariables) {
    for (QuantifierList::const_iterator q = myOutputVariables->begin ();
       q != myOutputVariables->end (); q++) {
      iterator v = myVariables.find ((*q)->getVariable ().getName ());
      assert (v != end () && v->second == &(*q)->getVariable ());
      v->second = 0;
    }

    delete myOutputVariables;
  }

  for (iterator v = myVariables.begin (); v != myVariables.end (); v++)
    delete v->second;

  while (myNumConstants--) {
    delete[] myConstantNames[myNumConstants];
    myConstants[myNumConstants]->destroy ();
  }
  delete[] myConstantNames;
  delete[] myConstants;
}

#ifndef NDEBUG
bool
00283 Transition::hasParent (const class Transition& parent) const
{
  for (unsigned i = myNumParents; i--; )
    if (myParents[i] == &parent)
      return true;
  return false;
}

bool
00292 Transition::hasChild (const class Transition& child) const
{
  for (unsigned i = myNumChildren; i--; )
    if (myChildren[i] == &child)
      return true;
  return false;
}
#endif // NDEBUG

/** Enlarge an array of transitions
 * @param t the array
 * @param num     size of the array
 */
void
00306 enlarge (const class Transition**& t,
       unsigned num)
{
  if (!(num & (num + 1))) {
    const class Transition** u =
      new const class Transition*[(num + 1) << 1];
    memcpy (u, t, sizeof (*t) * num);
    delete[] t;
    t = u;
  }
}

void
00319 Transition::changeParent (const class Transition& old,
                    const class Transition& fused)
{
  assert (old.hasChild (*this));
  assert (fused.hasChild (*this));
  for (unsigned i = myNumParents; i--; ) {
    if (myParents[i] == &old) {
      myParents[i] = &fused;
      return;
    }
  }
  assert (false);
}

void
00334 Transition::addChild (class Transition& child)
{
  assert (myNet && child.myNet);
  assert (child.myNet->getParent () == myNet ||
        myNet->getParent () == child.myNet);
  assert (!child.hasParent (*this));
  assert (!hasParent (child));

  ::enlarge (myChildren, myNumChildren);
  myChildren[myNumChildren++] = &child;
  ::enlarge (child.myParents, child.myNumParents);
  child.myParents[child.myNumParents++] = this;
}

void
00349 Transition::setAssertion (bool fatal)
{
  delete myOutputVariables;
  myOutputVariables = 0;
  while (myNumOutputs)
    delete myOutputs[--myNumOutputs];
  delete[] myOutputs;
  myOutputs = 0;
  myKind = fatal ? tFatal : tUndefined;
}

bool
00361 Transition::isHidden (const class Valuation& valuation) const
{
  if (!myHide)
    return false;
  if (class Value* v = myHide->eval (valuation)) {
    assert (v->getKind () == Value::vLeaf);
    bool hidden = bool (*static_cast<class LeafValue*>(v));
    delete v;
    return hidden;
  }
  valuation.clearErrors ();
  return false;
}

void
00376 Transition::addGate (class Expression& gate)
{
  assert (gate.getType () && gate.getType ()->getKind () == Type::tBool);

  if (!myGates.empty () &&
      (*myGates.begin ())->getKind () == Expression::eConstant) {
    // there is a constant gate (which should be always disabled):
    // ignore subsequent gate definitions
#ifndef NDEBUG
    {
      const class Expression* g = *myGates.begin ();
      const class Value& v =
      static_cast<const class Constant*>(g)->getValue ();
      assert (v.getKind () == Value::vLeaf);
      assert (!bool (static_cast<const class LeafValue&>(v)));
    }
#endif // NDEBUG
  ignore:
    gate.destroy ();
    return;
  }

  if (!gate.isAtomic () && gate.getKind () == Expression::eBooleanBinop) {
    class BooleanBinop& b = static_cast<class BooleanBinop&>(gate);
    if (b.isConj ()) {
      addGate (*const_cast<class Expression&>(b.getLeft ()).copy ());
      addGate (*const_cast<class Expression&>(b.getRight ()).copy ());
      b.destroy ();
      return;
    }
  }
  else if (gate.getKind () == Expression::eConstant) {
    const class Value& v =
      static_cast<const class Constant&>(gate).getValue ();
    assert (v.getKind () == Value::vLeaf);
    if (bool (static_cast<const class LeafValue&>(v)))
      goto ignore; // the gate is always true; it can be ignored
    else {
      // gate is always false; remove other gates
      for (GateList::iterator g = myGates.begin (); g != myGates.end (); g++)
      (*g)->destroy ();
      myGates.clear ();
      myGates.insert (myGates.end (), &gate);
    }
    return;
  }
  else if (gate.getKind () == Expression::eUndefined) {
    setAssertion (static_cast<const class Undefined&>(gate).isFatal ());
    goto ignore;
  }

  // see if there is such a gate already
  for (GateList::const_iterator g = myGates.begin (); g != myGates.end (); g++)
    if (**g == gate)
      goto ignore;

  // insert the gate
  myGates.insert (myGates.end (), &gate);
}

void
00437 Transition::addHide (class Expression& qualifier)
{
  assert (qualifier.isBasic () && !qualifier.isTemporal ());
  assert (qualifier.getType () &&
        qualifier.getType ()->getKind () == Type::tBool);

  // if the transition has been declared always hidden, ignore the qualifier
  if (myHide && myHide->getKind () == Expression::eConstant) {
#ifndef NDEBUG
    const class Value& v = static_cast<class Constant&>(qualifier).getValue ();
    assert (v.getKind () == Value::vLeaf);
    assert (bool (static_cast<const class LeafValue&>(v)));
#endif // NDEBUG
    qualifier.destroy ();
    return;
  }

  // treat constant qualifiers specially
  if (qualifier.getKind () == Expression::eConstant) {
    const class Value& v = static_cast<class Constant&>(qualifier).getValue ();
    assert (v.getKind () == Value::vLeaf);
    if (!bool (static_cast<const class LeafValue&>(v)))
      qualifier.destroy ();
    else {
      myHide->destroy ();
      myHide = &qualifier;
    }
    return;
  }

  myHide = myHide
    ? BooleanBinop::construct (false, *myHide, qualifier)
    : &qualifier;
}

unsigned
00473 Transition::addFairness (class Expression& qualifier,
                   unsigned number,
                   bool isStrong)
{
  assert (qualifier.isBasic () && !qualifier.isTemporal ());
  assert (qualifier.getType () &&
        qualifier.getType ()->getKind () == Type::tBool);

  unsigned& numFair = isStrong ? myNumStronglyFair : myNumWeaklyFair;

  if (qualifier.getKind () == Expression::eConstant) {
    const class Value& v = static_cast<class Constant&>(qualifier).getValue ();
    assert (v.getKind () == Value::vLeaf);
    if (!bool (static_cast<const class LeafValue&>(v))) {
      qualifier.destroy ();
      return numFair;
    }
  }

  class Expression**& fc = isStrong ? myStronglyFairCond : myWeaklyFairCond;
  unsigned*& fs = isStrong ? myStronglyFairSet : myWeaklyFairSet;

  class Expression** c = new class Expression*[numFair + 1];
  memcpy (c, fc, numFair * sizeof *fc);
  delete[] fc;
  fc = c;
  unsigned* s = new unsigned[numFair + 1];
  memcpy (s, fs, numFair * sizeof *fs);
  delete[] fs;
  fs = s;
  c[numFair] = &qualifier;
  s[numFair] = number;
  return ++numFair;
}

unsigned
00509 Transition::addEnabledness (class Expression& qualifier,
                      unsigned number)
{
  assert (qualifier.isBasic () && !qualifier.isTemporal ());
  assert (qualifier.getType () &&
        qualifier.getType ()->getKind () == Type::tBool);

  if (qualifier.getKind () == Expression::eConstant) {
    const class Value& v = static_cast<class Constant&>(qualifier).getValue ();
    assert (v.getKind () == Value::vLeaf);
    if (!bool (static_cast<const class LeafValue&>(v))) {
      qualifier.destroy ();
      return myNumEnabled;
    }
  }

  class Expression** c = new class Expression*[myNumEnabled + 1];
  memcpy (c, myEnabledCond, myNumEnabled * sizeof *myEnabledCond);
  delete[] myEnabledCond;
  myEnabledCond = c;
  unsigned* s = new unsigned[myNumEnabled + 1];
  memcpy (s, myEnabledSet, myNumEnabled * sizeof *myEnabledSet);
  delete[] myEnabledSet;
  myEnabledSet = s;
  c[myNumEnabled] = &qualifier;
  s[myNumEnabled] = number;
  return ++myNumEnabled;
}

/** Determine whether a variable occurs in an expression
 * @param expr    a variable in the expression
 * @param data    variable to look for
 * @return  false if the variable was found
 */
static bool
00544 findVariable (const class Expression& expr,
            void* data)
{
  return expr.getKind () != Expression::eVariable ||
    &static_cast<const class Variable&>(expr).getVariable () != data;
}

/** Determine which places are referenced from output arcs
 * @param expr    the literal (Variable or PlaceContents)
 * @param data    set of referenced places (or 0)
 * @return  if data==0 and expr is PlaceContents, false; otherwise true
 */
static bool
00557 findOutput (const class Expression& expr,
          void* data)
{
  if (expr.getKind () == Expression::ePlaceContents) {
    if (!data)
      return false;
    const class Place& place =
      static_cast<const class PlaceContents&>(expr).getPlace ();
    static_cast<class BitVector*>(data)->assign (place.getIndex (), true);
  }
  return true;
}

bool
00571 Transition::isInput (const class VariableDefinition* variable) const
{
  for (unsigned i = 0; i < myNumInputs; i++)
    if (!myInputs[i]->getExpr ().forVariables
      (&::findVariable, const_cast<class VariableDefinition*>(variable)))
      return true;
  return false;
}

bool
00581 Transition::isOutput (const class VariableDefinition* variable) const
{
  for (unsigned i = 0; i < myNumOutputs; i++)
    if (!myOutputs[i]->getExpr ().forVariables
      (&::findVariable, const_cast<class VariableDefinition*>(variable)))
      return true;
  return false;
}

bool
00591 Transition::isGate (const class VariableDefinition* variable) const
{
  for (GateList::const_iterator i = myGates.begin (); i != myGates.end (); i++)
    if (!(*i)->forVariables
      (&::findVariable, const_cast<class VariableDefinition*>(variable)))
      return true;
  return false;
}

const class VariableDefinition&
00601 Transition::addOutputVariable (const class Type& type, char* name,
                         class Expression* expr)
{
  if (!myOutputVariables)
    myOutputVariables = new class QuantifierList;

  if (name) {
    class VariableDefinition& d = const_cast<class VariableDefinition&>
      (*getVariable (name));
    assert (&d.getType () == &type && d.isAggregate ());
    myOutputVariables->append (*new class Quantifier (d, expr));
    return d;
  }
  else {
    for (card_t i = myOutputVariables ? myOutputVariables->size () : 0;; i++) {
      name = new char[i ? 2 + log16 (i) : 3];
      sprintf (name, ":%x", i);
      if (myVariables.find (name) == myVariables.end ())
      break;
      delete[] name;
    }
  }

  class Quantifier* q = new class Quantifier (name, type, expr);
  myOutputVariables->append (*q);
  class VariableDefinition& d = const_cast<class VariableDefinition&>
    (q->getVariable ());
  assert (myVariables.find (name) == myVariables.end ());
  myVariables.insert (VariableMap::value_type (d.getName (), &d));
  return d;
}

const class VariableDefinition&
00634 Transition::addVariable (char* name,
                   const class Type& type,
                   bool aggregate,
                   bool hidden)
{
  assert (name && myVariables.find (name) == myVariables.end ());
  class VariableDefinition* d =
    new class VariableDefinition (name, type, aggregate, hidden);
  myVariables.insert (VariableMap::value_type (d->getName (), d));
  return *d;
}

void
00647 Transition::addFunction (class Function& function)
{
  assert (!getFunction (function.getName ()));
  myFunctions.insert (FunctionMap::value_type
                  (function.getName (), &function));
}

bool
00655 Transition::checkGates (const class Valuation& valuation,
                  enum Error err) const
{
  for (GateList::const_iterator i = myGates.begin ();
       i != myGates.end (); i++) {
    class Value* v = (*i)->eval (valuation);
    if (!v) {
      if (valuation.getError () != err)
      return false;
      valuation.clearErrors ();
      continue;
    }
    assert (valuation.isOK () && v->getKind () == Value::vLeaf);
    bool accepted = bool (static_cast<const class LeafValue&>(*v));
    delete v;
    if (!accepted)
      return false;
  }

  return true;
}

void
00678 Transition::addArc (class Arc& arc)
{
  if (arc.isOutput ()) {
    if (myOutputs) {
      class Arc** a = new class Arc*[myNumOutputs + 1];
      memcpy (a, myOutputs, sizeof (*myOutputs) * myNumOutputs);
      delete[] myOutputs;
      myOutputs = a;
    }
    else {
      assert (!myNumOutputs);
      myOutputs = new class Arc*[1];
    }

    myOutputs[myNumOutputs++] = &arc;
    if (!myOutputMarking && !arc.getExpr ().forVariables (&::findOutput, 0))
      myOutputMarking = true;
  }
  else {
    if (myInputs) {
      class Arc** a = new class Arc*[myNumInputs + 1];
      memcpy (a, myInputs, sizeof (*myInputs) * myNumInputs);
      delete[] myInputs;
      myInputs = a;
    }
    else {
      assert (!myNumInputs);
      myInputs = new class Arc*[1];
    }

    myInputs[myNumInputs++] = &arc;
  }
}

class Arc*
00713 Transition::getArc (bool output, const class Place& place)
{
  if (output) {
    for (unsigned i = 0; i < myNumOutputs; i++)
      if (&myOutputs[i]->getPlace () == &place)
      return myOutputs[i];
  }
  else {
    for (unsigned i = 0; i < myNumInputs; i++)
      if (&myInputs[i]->getPlace () == &place)
      return myInputs[i];
  }
  return NULL;
}

/** restore heap order to arrays being sorted
 * @param keys          the keys
 * @param values  values associated with the keys
 * @param size          number of elements in the arrays
 * @param depth         depth below which the heap order is to be restored
 */
static void
00735 heapify (unsigned* keys,
       unsigned* values,
       unsigned size,
       unsigned depth)
{
  unsigned largest = depth, l;
  for (;;) {
    l = largest << 1;
    assert (keys && values && depth < size);
    if (++l >= size)
      return;
    if (keys[l] > keys[depth]) {
      largest = l;
      if (++l < size && keys[l] > keys[depth])
      largest = l;
    }
    else if (++l < size && keys[l] > keys[depth])
      largest = l;
    else
      return;
    l = keys[largest], keys[largest] = keys[depth], keys[depth] = l;
    l = values[largest], values[largest] = values[depth], values[depth] = l;
    depth = largest;
  }
}


bool
00763 Transition::addConstant (char* name, class Constant& constant)
{
  assert (name && constant.getType () && !constant.getType ()->isLeaf ());

  for (unsigned i = myNumConstants; i--; )
    if (!strcmp (name, myConstantNames[i]))
      return false;

  if (!(myNumConstants & (myNumConstants + 1))) {
    char** constantNames = new char*[(myNumConstants + 1) << 1];
    memcpy (constantNames, myConstantNames,
          myNumConstants * sizeof *myConstantNames);
    delete[] myConstantNames;
    myConstantNames = constantNames;

    class Constant** constants =
      new class Constant*[(myNumConstants + 1) << 1];
    memcpy (constants, myConstants, myNumConstants * sizeof *myConstants);
    delete[] myConstants;
    myConstants = constants;
  }

  myConstantNames[myNumConstants] = name;
  myConstants[myNumConstants++] = &constant;
  return true;
}

const class Constant*
00791 Transition::getConstant (const char* name) const
{
  for (unsigned i = myNumConstants; i--; )
    if (!strcmp (name, myConstantNames[i]))
      return myConstants[i];
  return 0;
}

bool
00800 Transition::fuse (const class Transition& callee,
              const class Printer& printer,
              bool warn)
{
  /** the return status */
  bool ok = true;

  assert (myNet && callee.myNet);
  assert (callee.myNet == myNet ||
        callee.myNet == myNet->getParent () ||
        callee.myNet->getParent () == myNet);
  // if the callee is a synchronisation label, register the caller with it
  if (callee.myNet == myNet->getParent ()) {
    for (unsigned i = callee.myNumChildren; i--; ) {
      if (callee.myChildren[i]->myNet == myNet) {
      printer.printRaw ("transition ");
      printer.printQuoted (callee.myChildren[i]->myName);
      printer.printRaw (" already synchronises on ");
      printer.delimiter (':');
      printer.printQuoted (callee.myName);
      printer.finish ();
      ok = false;
      break;
      }
    }
    const_cast<class Transition&>(callee).addChild (*this);
  }

  /** variable substitutions */
  class Substitution substitution;
  // fuse the variables
  for (VariableMap::const_iterator i = callee.myVariables.begin ();
       i != callee.myVariables.end (); i++) {
    const class VariableDefinition& var = *i->second;
    if (class Function* func = getFunction (var.getName ())) {
      if (!func->getArity ()) {
      if (func->getExpr ().getType () != &var.getType ()) {
        printer.printRaw ("type mismatch for variable ");
        printer.printQuoted (var.getName ());
        printer.finish ();
        ok = false;
      }
      else if (var.isAggregate ()) {
        if (warn) {
          printer.printRaw ("Warning:callee output variable ");
          printer.printQuoted (var.getName ());
          printer.printRaw (" shadows a nullary function");
          printer.finish ();
        }
      }
      else
        substitution.setExpr (var, *const_cast<class Expression&>
                        (func->getExpr ()).cse ()->copy ());
      continue;
      }
      if (warn) {
      printer.printRaw ("Warning:callee variable ");
      printer.printQuoted (var.getName ());
      printer.printRaw (" shadows a non-nullary function");
      printer.finish ();
      }
    }
    if (const class Constant* c = getConstant (var.getName ())) {
      substitution.setExpr (var, *const_cast<class Constant*>(c)->copy ());
      continue;
    }
    iterator j = myVariables.find (i->first);
    if (j != myVariables.end ()) {
      const class VariableDefinition& v = *j->second;
      if (v.isAggregate () || var.isAggregate ()) {
      printer.printRaw ("redefinition of output variable ");
      printer.printQuoted (var.getName ());
      printer.finish ();
      ok = false;
      }
      else if (&v.getType () != &var.getType ()) {
      printer.printRaw ("type mismatch for variable ");
      printer.printQuoted (var.getName ());
      printer.finish ();
      ok = false;
      }
      else
      substitution.setExpr (var, *(new class Variable (v))->cse ());
    }
    else if (ok && !var.isAggregate ()) {
      // introduce a new variable
      class VariableDefinition& v =
      *new class VariableDefinition (var);
      myVariables.insert (VariableMap::value_type (v.getName (), &v));
      substitution.setExpr (var, *(new class Variable (v))->cse ());
    }
  }

  // fuse the output variables
  if (callee.myOutputVariables) {
    for (QuantifierList::const_iterator q =
         callee.myOutputVariables->begin ();
       q != callee.myOutputVariables->end (); q++) {
      const class VariableDefinition& var = (*q)->getVariable ();
      class Expression* cond =
      const_cast<class Expression*>((*q)->getCondition ());
      substitution.setExpr
      (var, *(new class Variable (addOutputVariable
                            (var.getType (), 0, cond
                             ? cond->substitute (substitution)
                             : 0)))->cse ());
      if (!warn);
      else if (getConstant (var.getName ())) {
      printer.printRaw ("Warning:callee output variable ");
      printer.printQuoted (var.getName ());
      printer.printRaw (" shadows a constant");
      printer.finish ();
      }
      else if (getFunction (var.getName ())) {
      printer.printRaw ("Warning:callee output variable ");
      printer.printQuoted (var.getName ());
      printer.printRaw (" shadows a function");
      printer.finish ();
      }
    }
  }

  // fuse the gates
  if (ok)
    for (GateList::const_iterator g = callee.myGates.begin ();
       g != callee.myGates.end (); g++)
      addGate (*(*g)->substitute (substitution));

  // fuse the functions
  for (FunctionMap::const_iterator f = callee.myFunctions.begin ();
       f != callee.myFunctions.end (); f++) {
    if (myFunctions.find (f->first) != myFunctions.end ()) {
      if (f->second->isCopy () && callee.myNet->getParent () == myNet) {
      /*
       * We are constructing a fused synchronisation transition here,
       * by fusing together each synchronising transitions
       * (the parameter "callee") in child nets.
       *
       * This function definition has been copied to the callee from
       * a synchronisation label.  Thus, it will be copied to this
       * transition from some other source, and it must not be copied
       * here again.
       *
       * This modification was suggested by Charles Lakos.
       */
       continue;
      }
      printer.printRaw ("redefinition of function ");
      printer.printQuoted (f->first);
      printer.finish ();
      ok = false;
    }
    else if (ok) {
      const class Function& func = *f->second;
      unsigned i = func.getArity ();
      char* name = newString (func.getName ());
      class VariableDefinition** params = i
      ? new class VariableDefinition*[i]
      : 0;
      if (const class VariableDefinition* v = i ? 0 : getVariable (name)) {
      if (v->isAggregate ()) {
        printer.printRaw ("Warning:nullary callee function ");
        printer.printQuoted (name);
        printer.printRaw (" shadows an output variable");
        printer.finish ();
      }
      else if (&v->getType () != func.getExpr ().getType ()) {
        printer.printRaw ("type mismatch for variable and nullary function ");
        printer.printQuoted (name);
        printer.finish ();
        ok = false;
      }
      else {
        substitution.setExpr (*v, *const_cast<class Expression&>
                        (func.getExpr ()).cse ()->copy ());
        iterator v = myVariables.find (name);
        assert (v != myVariables.end ());
        delete v->second;
        myVariables.erase (v);
      }
      }
      if (warn && !i && getConstant (name)) {
      printer.printRaw ("Warning:nullary callee function ");
      printer.printQuoted (name);
      printer.printRaw (" shadows a constant");
      printer.finish ();
      }
      while (i--)
      substitution.setExpr
        (func[i], *(new class Variable
                  (*(params[i] =
                   new class VariableDefinition (func[i]))))->cse ());
      myFunctions.insert (FunctionMap::value_type
                    (name, new class Function
                     (name, func.getArity (), params,
                      const_cast<class Expression&>
                      (func.getExpr ()).substitute (substitution),
                      true)));
    }
  }

  // fuse the constants
  unsigned k;
  for (k = callee.myNumConstants; k--; ) {
    const char* name = callee.myConstantNames[k];
    class Constant& cc = *const_cast<class Constant*>(callee.myConstants[k]);
    if (const class Constant* c = getConstant (name)) {
      if (*c == cc)
      continue;
      printer.printRaw ("redefinition of constant ");
      printer.printQuoted (name);
      printer.finish ();
      ok = false;
    }
    else if (ok) {
      if (warn && getVariable (name)) {
      printer.printRaw ("Warning:callee constant ");
      printer.printQuoted (name);
      printer.printRaw (" shadows a variable");
      printer.finish ();
      }
      addConstant (newString (name),
               *static_cast<class Constant*>(cc.copy ()));
    }
  }

  // substitute replaced variables in constraints, gates, functions and arcs
  if (ok) {
    for (k = myNumWeaklyFair; k--; ) {
      class Expression* e = myWeaklyFairCond[k]->substitute (substitution);
      myWeaklyFairCond[k]->destroy ();
      myWeaklyFairCond[k] = e;
    }
    for (k = myNumStronglyFair; k--; ) {
      class Expression* e = myStronglyFairCond[k]->substitute (substitution);
      myStronglyFairCond[k]->destroy ();
      myStronglyFairCond[k] = e;
    }
    for (k = myNumEnabled; k--; ) {
      class Expression* e = myEnabledCond[k]->substitute (substitution);
      myEnabledCond[k]->destroy ();
      myEnabledCond[k] = e;
    }
    for (GateList::iterator g = myGates.begin (); g != myGates.end (); g++) {
      class Expression* e = (*g)->substitute (substitution);
      (*g)->destroy ();
      *g = e;
    }
    for (FunctionMap::iterator f = myFunctions.begin ();
       f != myFunctions.end (); f++)
      f->second->substitute (substitution);
    for (k = myNumInputs; k--; )
      myInputs[k]->substitute (substitution);
    for (k = myNumOutputs; k--; )
      myOutputs[k]->substitute (substitution);
  }

  // fuse the fairness and enabledness constraints
  for (k = callee.myNumWeaklyFair; k--; ) {
    if (!myNet->addConstraint (*const_cast<class Expression*>
                         (callee.myWeaklyFairCond[k])->substitute
                         (substitution), *this, Net::Weak)) {
      printer.printRaw ("unable to fuse `weakly_fair' constraint");
      printer.finish ();
      ok = false;
    }
  }
  for (k = callee.myNumStronglyFair; k--; ) {
    if (!myNet->addConstraint (*const_cast<class Expression*>
                         (callee.myStronglyFairCond[k])->substitute
                         (substitution), *this, Net::Strong)) {
      printer.printRaw ("unable to fuse `strongly_fair' constraint");
      printer.finish ();
      ok = false;
    }
  }
  for (k = callee.myNumEnabled; k--; ) {
    if (!myNet->addConstraint (*const_cast<class Expression*>
                         (callee.myEnabledCond[k])->substitute
                         (substitution), *this, Net::Enabled)) {
      printer.printRaw ("unable to fuse `enabled' constraint");
      printer.finish ();
      ok = false;
    }
  }

  if (ok) {
    // fuse the inputs
    for (k = callee.myNumInputs; k--; ) {
      const class Arc& arc = *callee.myInputs[k];
      if (callee.myNet->getParent () == myNet &&
        arc.isCopy () && getArc (false, arc.getPlace ())) {
      /*
       * We are constructing a fused synchronisation transition here,
       * by fusing together each synchronising transitions
       * (the parameter "callee") in child nets.
       *
       * This input arc has been copied to the callee from a
       * synchronisation label.  Thus, it will be copied to this
       * transition from some other source, and it must not be copied
       * here again.
       *
       * This modification was suggested by Charles Lakos.
       */
      continue;
      }
      addArc (*new class Arc (false, *static_cast<class Marking*>
                        (const_cast<class Marking&>
                         (arc.getExpr ()).substitute (substitution)),
                        arc.getPlace (), true));
    }
    // fuse the assertion status
    if (callee.myKind > myKind)
      myKind = callee.myKind;
    // fuse the outputs only for non-assertion transitions
    if (!myKind) {
      for (k = callee.myNumOutputs; k--; ) {
      const class Arc& arc = *callee.myOutputs[k];
      if (callee.myNet->getParent () == myNet &&
          arc.isCopy () && getArc (true, arc.getPlace ()))
        continue; // see the comment on input arcs, above
      addArc (*new class Arc (true, *static_cast<class Marking*>
                        (const_cast<class Marking&>
                         (arc.getExpr ()).substitute (substitution)),
                        arc.getPlace (), true));
      }
    }
    if (callee.myOutputMarking)
      myOutputMarking = true;
    if (!myPriority)
      myPriority = callee.myPriority;
  }

  return ok;
}

bool
01137 Transition::isUnifiable (enum Unif action,
                   const class Printer& printer)
{
  struct unif* u;
  for (; (u = myUnif); myUnif = u) { // clean up a previous definition
    u = u->next;
    delete myUnif->vars;
    delete myUnif;
  }

  // construct the unification list with a depth-first search algorithm:
  //   do
  //     take all arcs that can be fully evaluated
  //     (sorted in ascending order of maximum size of associated markings)
  //     pick an arc that can unify currently unbound variables
  //       and extend the set of unified variables
  //   until all input arcs have been processed
  //
  // Primary cost function:
  //   cost1[arc] = 0 if the arc contains unifiable variables, or
  //   cost1[arc] = number of preceding arcs containing unifiable variables
  // total cost: sum over cost1[] for all arcs
  //
  // Secondary cost function (applied when the primary one yields a tie):
  //   cost2[arc] = maximum number of iterations for the arc
  // total cost: cost2[0] * (1 + cost2[1] * (1 + (...)))

  /** number of split input arcs */
  unsigned numInputs;
  unsigned input;
  for (numInputs = input = 0; input < myNumInputs; input++)
    for (const class Marking* m = myInputs[input]->getExpr ().first ();
       m; m = m->next (), numInputs++);
  assert (numInputs >= myNumInputs);

  /** best primary cost found so far */
  unsigned* best1 = numInputs ? new unsigned[numInputs] : 0;
  /** primary cost of the combination being considered */
  unsigned* cost1 = numInputs ? new unsigned[numInputs] : 0;
  /** best secondary cost found so far */
  card_t* best2 = numInputs ? new card_t[numInputs] : 0;
  /** secondary cost of the combination being considered */
  card_t* cost2 = numInputs ? new card_t[numInputs] : 0;

  /** the split input arcs */
  const class Marking** arcs = new const class Marking*[numInputs];
  /** split arcs whose multiplicity depends on variables */
  class BitVector varMult (numInputs);
  /** best combination found so far */
  unsigned* best = numInputs ? new unsigned[numInputs] : 0;
  /** combination being considered */
  unsigned* comb = numInputs ? new unsigned[numInputs] : 0;
  /** number of variable-multiplicity unifiers in the best combination */
  unsigned bestvar = UINT_MAX;
  /** number of variable-multiplicity unifiers in current combination */
  unsigned combvar = 0;
  /** variable sets unified from each arc in the best solution */
  class VariableSet** varb = numInputs ? new class VariableSet*[numInputs] : 0;
  /** variable sets unified from each arc in current combination */
  class VariableSet** varc = numInputs ? new class VariableSet*[numInputs] : 0;

  // initialize the costs
  for (input = numInputs; input--; ) {
    best1[input] = UINT_MAX, best2[input] = CARD_T_MAX;
    varb[input] = varc[input] = 0;
  }
  // initialize the split input arcs
  for (numInputs = input = 0; input < myNumInputs; input++)
    for (const class Marking* m = myInputs[input]->getExpr ().first ();
       m; m = m->next (), numInputs++)
      if ((arcs[numInputs] = m)->hasVariableMultiplicity ())
      varMult.assign (numInputs, true);

  /** all variables that could be unified */
  class VariableSet vars;
  /** all variables that can definitely be unified */
  class VariableSet allVars;

  for (input = 0;;) {
    unsigned i, j;

    if (input < numInputs) {
      // see if there are any constant arcs
      for (i = numInputs; i--; ) {
      // skip already processed arc expressions
      for (j = input; j--; )
        if (comb[j] == i)
          goto skipConstant;
      if (arcs[i]->depends (allVars, true)) {
      skipConstant:
        continue;
      }
      // calculate the cost functions
      cost1[input] = 0;
      for (j = input; j--; )
        if (varc[j])
          cost1[input]++;
      cost2[input] = 1;
      varc[input] = 0;
      comb[input++] = i;
      }
    }

    if (input == numInputs) { // solution completed
      assert (bestvar >= combvar);
      if (bestvar > combvar) {
      bestvar = combvar;
      goto better;
      }
      for (input = numInputs, i = 0, j = 0; input--; )
      i += best1[input], j += cost1[input];
      if (i < j)
      goto worse;
      else if (i == j) {
      /** total secondary costs */
      card_t b = 0, c = 0;
      for (input = numInputs; input--; ) {
        if (b < CARD_T_MAX) {
          if (b && best2[input] < CARD_T_MAX / b)
            b *= best2[input];
          if (b < CARD_T_MAX) b++;
        }
        if (c < CARD_T_MAX) {
          if (c && cost2[input] < CARD_T_MAX / c)
            c *= cost2[input];
          if (c < CARD_T_MAX) c++;
        }
      }
      if (c > b) goto worse;
      }
    better:
      memcpy (best1, cost1, numInputs * sizeof *best1);
      memcpy (best2, cost2, numInputs * sizeof *best2);
      memcpy (best, comb, numInputs * sizeof *best);
      // copy the variable sets and count them
      for (input = numInputs, i = 0; input--; ) {
      delete varb[input];
      if ((varb[input] = varc[input]))
        varb[input] = new class VariableSet (*varb[input]), i++;
      }
      if (i > 5) {
      // more than 5 arcs with unifiable variables:
      // give up after the first solution
      // to avoid a combinatorial explosion
      for (input = numInputs; input--; ) {
        delete varc[input];
        varc[input] = 0;
      }
      goto finish;
      }
    worse:
      // backtrack to the last arc with unifiable variables
      for (input = numInputs; input--; )
      if (varc[input]) break;
      if (!(input + 1)) {
      // no variables (only constant arcs)
      assert (vars.empty () && allVars.empty ());
      goto finish;
      }
      vars.clear ();
      allVars.clear ();
      if (varMult[comb[input]]) {
      assert (combvar >= varc[input]->size ());
      combvar -= varc[input]->size ();
      }
      delete varc[input];
      varc[input] = 0;
      for (i = 0; i < input; i++) {
      if (varc[i]) {
        for (VariableSet::const_iterator v = varc[i]->begin ();
             v != varc[i]->end (); v++) {
          const class VariableDefinition& var = **v;
          assert (!allVars.contains (var));
          vars.insert (var);
          if (!varMult[comb[i]])
            allVars.insert (var);
        }
      }
      }
      i = comb[input];
    }
    else
      i = numInputs;

  nextUnifier:
    // see if there are arcs from which variables can be unified
    while (i--) {
      // skip already processed arc expressions
      for (j = input; j--; )
      if (comb[j] == i)
        goto skipVar;
      // skip arcs whose multiplicity cannot be evaluated
      for (const class Marking* mp = arcs[i]; mp; mp = mp->getParent ())
      if (const class Expression* mult = mp->getMultiplicity ())
        if (mult->depends (allVars, true))
          goto skipVar;
      arcs[i]->getToken ()->getLvalues (allVars, varc[input]);
      if (!varc[input]) {
      skipVar:
      continue;
      }
      // calculate the cost functions
      cost1[input] = 0;
      cost2[input] = arcs[i]->getType ()->getNumValues ();
      if (cost2[input] > arcs[i]->getPlace ()->getMaxNumTokens ())
      cost2[input] = arcs[i]->getPlace ()->getMaxNumTokens ();
      comb[input] = i;
      if (varMult[i]) {
      if ((combvar += varc[input]->size ()) > bestvar) {
        combvar -= varc[input]->size ();
        continue;
      }
      }
      for (VariableSet::const_iterator v = varc[input]->begin ();
         v != varc[input]->end (); v++) {
      const class VariableDefinition& var = **v;
      assert (!allVars.contains (var));
      vars.insert (var);
      if (!varMult[i])
        allVars.insert (var);
      }
      goto nextArc;
    }
    // no unifiable variables found: backtrack
    while (input--) {
      if (!varc[input])
      continue;
      vars.clear ();
      allVars.clear ();
      if (varMult[comb[input]]) {
      assert (combvar >= varc[input]->size ());
      combvar -= varc[input]->size ();
      }
      delete varc[input];
      varc[input] = 0;
      for (i = 0; i < input; i++) {
      if (varc[i]) {
        for (VariableSet::const_iterator v = varc[i]->begin ();
             v != varc[i]->end (); v++) {
          const class VariableDefinition& var = **v;
          assert (!allVars.contains (var));
          vars.insert (var);
          if (!varMult[comb[i]])
            allVars.insert (var);
        }
      }
      }
      i = comb[input];
      goto nextUnifier;
    }
    // out of solutions
  finish:
    break;
  nextArc:
    input++;
    continue;
  }

  assert (!myUnif);

  /** flag: is everything ok? */
  bool ok = bestvar < UINT_MAX;
  if (ok) {
    // sort contiguous sequences of constant arcs in ascending order of
    // place size
    for (input = numInputs; input--; ) {
      if (varb[input])
      continue;
      unsigned i = input;
      while (i--) {
      if (varb[i])
        break;
      assert (best2[i] == 1);
      best2[i] = arcs[best[i]]->getType ()->getNumValues ();
      if (best2[i] > arcs[best[i]]->getPlace ()->getMaxNumTokens ())
        best2[i] = arcs[best[i]]->getPlace ()->getMaxNumTokens ();
      }
      if (++i == input)
      continue;
      unsigned j = input + 1 - i, k = j / 2;
      while (k--)
	::heapify (best2 + i, best + i, j, k);
      while (j-- > 1) {
      k = best2[i], best2[i] = best2[i + j], best2[i + j] = k;
      k = best[i], best[i] = best[i + j], best[i + j] = k;
	::heapify (best2 + i, best + i, j, 0);
      }
      input = i;
    }

    // check that all input variables could be unified
    vars.clear ();
    for (input = numInputs; input--; ) {
      if (varb[input]) {
      for (VariableSet::const_iterator v = varb[input]->begin ();
           v != varb[input]->end (); v++) {
        const class VariableDefinition& var = **v;
        vars.insert (var);
        if (varMult[comb[input]])
          const_cast<class VariableDefinition&>(var).flagUndefined ();
      }
      }
    }
    // see that all variables of the transition can be unified
    for (const_iterator vd = begin (); vd != end (); vd++) {
      const class VariableDefinition& var = *vd->second;
      if (!var.isAggregate () && !vars.contains (var)) {
      switch (action) {
      case uNormal:
        break;
      case uRemove:
        // remove those gates that the variable depends on
        for (GateList::iterator i = myGates.begin (), j = i;
             i != myGates.end (); i = j)
          if (!(*j++)->forVariables
            (&::findVariable, const_cast<class VariableDefinition*>(&var)))
            (*i)->destroy (), myGates.erase (i);
        // fall through
      case uIgnore:
        if (!isInput (&var))
          continue;
      }
      printer.printRaw ("variable ");
      printer.print (var.getName ());
      printer.printRaw (" cannot be unified");
      printer.finish ();
      ok = false;
      }
    }
    if (ok) {
      // construct myUnif
      for (input = numInputs; input--; ) {
      u = new struct unif;
      u->next = myUnif;
      u->vars = varb[input], varb[input] = 0;
      u->m = arcs[best[input]];
      u->isSet = u->m->getToken ()->isSet ();
      u->varMult = varMult[best[input]];
      u->place = u->m->getPlace ()->getIndex ();
      assert (!u->isSet || !u->vars);
      myUnif = u;
      }
    }
  }

  delete[] best1; delete[] cost1;
  delete[] best2; delete[] cost2;
  delete[] comb;
  delete[] best; delete[] arcs;
  for (input = numInputs; input--; ) {
    delete varb[input];
    delete varc[input];
  }
  delete[] varb;
  delete[] varc;

  // child transitions are not assertions; their parents are
  if (ok && action == uRemove)
    myKind = tNormal;
  return ok;
}

void
01500 Transition::analyze (class GlobalMarking& m,
                 class StateReporter& reporter) const
{
  if (!myGates.empty () &&
      (*myGates.begin ())->getKind () == Expression::eConstant) {
    // there is a constant gate (which should be always disabled):
    // ignore the transition
#ifndef NDEBUG
    const class Expression* g = *myGates.begin ();
    const class Value& v = static_cast<const class Constant*>(g)->getValue ();
    assert (v.getKind () == Value::vLeaf);
    assert (!bool (static_cast<const class LeafValue&>(v)));
#endif // NDEBUG
    return;
  }

  class Valuation valuation;
  const struct unif* u = myUnif;
  /** processed tokens */
  class TokenList tokens;

  for (class Token* token = 0;;) {
    assert (valuation.isOK ());
    // get next input arc inscription (abstract token) to be unified
    if (u) { // have all arc inscriptions been processed?
      // evaluate the multiplicity of the token
      if (card_t mult = u->m->getMultiplicity (valuation)) {
      assert (valuation.isOK ());
      class PlaceMarking& pm = m[u->place];
      token = !u->isSet && pm.empty ()
        ? 0
        : new class Token (mult, pm, *u);
      }
      else if (valuation.isOK ()) { // zero multiplicity => skip the token
      u = u->next;
      continue;
      }
      else
      goto unifError;

      if (token) {
      if (!u->vars) {
        // Any variables in the token have been unified before.
        // Evaluate the token and see if it is present in the input place.
        if (token->isBindable (valuation)) {
          // reserve the token and advance to the next one
        bindToken:
          assert (valuation.isOK ());
          token->reserve ();
          tokens.push (*token);
          token = 0;
          u = u->next;
          continue;
        }
        delete token;
        if (!valuation.isOK ()) {
          // report unification error and backtrack
        unifError:
          willDo (false, *this, valuation, m, reporter, "unification:");
        }
      }
      else { // some variables must be unified from the token
        if (u->varMult)
          token->addUnified (valuation);
        for (;;) {
#ifndef NDEBUG
          token->assertUndefined (valuation);
#endif // NDEBUG

          if (!token->getConcrete ());
          else if (willDo (token->isCompatible (valuation),
                       *this, valuation, m, reporter)) {
            u->m->getToken ()->getLvalues (token->getValue (),
                                   valuation, *u->vars);
#ifndef NDEBUG
            token->assertDefined (valuation);
#endif // NDEBUG
            if (willDo (checkGates (valuation) &&
                    token->isCompatible (valuation) &&
                    tokens.isCompatible (valuation),
                    *this, valuation, m, reporter))
            goto bindToken;
          incompatible:
            token->undefine (valuation);
            goto incompatible2;
          }
          else {
          incompatible2:
            if (interrupted || reporter.isFatal ())
            return;
            if (token->next ())
            continue;
          }

          delete token;
          break;
        }
      }
      }
    }
    // everything unified => try to fire the transition
    else if (myKind) {
      // an assertion transition is enabled
      valuation.flagUndefined (myKind == tFatal);
      reporter.reject (*this, valuation, m, "undefined gate", 0);
      // clean up the unification stack and return
      while (!tokens.empty ())
      if ((token = &tokens.pop ())->isReserved ())
        token->free ();
      return;
    }
    else if (!willDo (true, *this, valuation, m, reporter,
                  checkGates (valuation, errNone)
                  ? 0 : "undefined gate:"));
    else if (myNumParents)
      reporter.reportSync (*this);
    else if (firstOutput (*this, valuation, m, reporter)) {
      /** tokens removed from the input places */
      class GlobalMarking* inputs = 0;
      if (myOutputMarking) {
      inputs = new class GlobalMarking (reporter.net);
      for (TokenList::const_iterator t = tokens.begin ();
           t != tokens.end (); t++) {
        const struct unif& unif = (*t)->getUnifier ();
        class PlaceMarking& pm = (*inputs)[unif.place];
        if (!(*t)->copyRemoved (pm))
          assert (false);
      }
      }
      valuation.setGlobalMarking (inputs);

      // Fire the transition for all allowed bindings of output variables
      do {
      /** Placeholder for the successor state */
      class GlobalMarking successor (m);
      // Evaluate the output arcs and add the resulting state
      fireOutputs (*this, valuation, successor, reporter);
      }
      while (!interrupted && !reporter.isFatal () &&
           nextOutput (*this, valuation, m, reporter));

      valuation.setGlobalMarking (0);
      delete inputs;
    }

    // Backtrack in the search
    while (!tokens.empty ()) {
      token = &tokens.pop ();

      // Restore the reserved token to the input place
      if (token->isReserved ())
      token->free ();

      // If the token is "constant", backtrack further
      if (!(u = &token->getUnifier ())->vars) {
      delete token;
      continue;
      }

      goto incompatible;
    }
    break;
  }
}

void
01666 Transition::report (const class Valuation& valuation,
                const class GlobalMarking& marking,
                const char* reason,
                const class Place* place,
                const class Printer& printer) const
{
  if (myName)
    printer.printQuoted (myName);
  else
    printer.printRaw ("(anonymous)");
  printer.delimiter (':');
  if (place) {
    printer.printRaw ("integrity violation for ");
    printer.printQuoted (place->getName ());
  }
  else
    printer.printRaw (reason ? reason : "rejected successor state");
  printer.linebreak ();
  valuation.display (printer);
  printer.finish ();
  marking.display (printer);
  printer.finish ();
}

void
01691 Transition::displayEdge (const class Valuation& valuation,
                   const class GlobalMarking& marking,
                   const class Printer& printer) const
{
  printer.printRaw ("transition ");
  printer.print (myName);
  printer.printRaw ("->");
  marking.display (printer);
  printer.finish ();
  valuation.display (printer);
  printer.finish ();
}

void
01705 Transition::unfold (class GlobalMarking& cover,
                class LNet& lnet,
                class DummyReporter& reporter) const
{
  assert (&lnet.getNet ().getTransition (myRootIndex) == this);
  if (myKind)
    return; // this is a "fact" transition (an assertion)
  if (!myGates.empty () &&
      (*myGates.begin ())->getKind () == Expression::eConstant) {
    // there is a constant gate (which should be always disabled):
    // ignore the transition
#ifndef NDEBUG
    const class Expression* g = *myGates.begin ();
    const class Value& v = static_cast<const class Constant*>(g)->getValue ();
    assert (v.getKind () == Value::vLeaf);
    assert (!bool (static_cast<const class LeafValue&>(v)));
#endif // NDEBUG
    return;
  }
  class Valuation valuation;
  const struct unif* u = myUnif;
  /** the input marking */
  class GlobalMarking& m (cover);
  /** processed tokens */
  class TokenList tokens;

  lnet.removeTransitions (myRootIndex);

  for (class Token* token = 0;;) {
    assert (valuation.isOK ());
    // get next input arc inscription (abstract token) to be unified
    if (u) { // have all arc inscriptions been processed?
      // evaluate the multiplicity of the token
      if (card_t mult = u->m->getMultiplicity (valuation)) {
      assert (valuation.isOK ());
      class PlaceMarking& pm = m[u->place];
      token = !u->isSet && pm.empty ()
        ? 0
        : new class Token (mult, pm, *u);
      }
      else if (valuation.isOK ()) { // zero multiplicity => skip the token
      u = u->next;
      continue;
      }
      else
      goto unifError;

      if (token) {
      if (!u->vars) {
        // Any variables in the token have been unified before.
        // Evaluate the token and see if it is present in the input place.
        if (token->isBindableUnfold (valuation)) {
          // reserve the token and advance to the next one
        bindToken:
          assert (valuation.isOK ());
          token->setReservedUnfold (true);
          tokens.push (*token);
          token = 0;
          u = u->next;
          continue;
        }
        delete token;
        if (!valuation.isOK ()) {
          // report unification error and backtrack
        unifError:
          willDo (false, *this, valuation, m, reporter, "unification:");
        }
      }
      else { // some variables must be unified from the token
        if (u->varMult)
          token->addUnified (valuation);
        for (;;) {
#ifndef NDEBUG
          token->assertUndefined (valuation);
#endif // NDEBUG

          if (!token->getConcreteUnfold ());
          else if (willDo (token->isCompatible (valuation),
                       *this, valuation, m, reporter)) {
            u->m->getToken ()->getLvalues (token->getValue (),
                                   valuation, *u->vars);
#ifndef NDEBUG
            token->assertDefined (valuation);
#endif // NDEBUG
            if (willDo (checkGates (valuation) &&
                    token->isCompatible (valuation) &&
                    tokens.isCompatible (valuation),
                    *this, valuation, m, reporter))
            goto bindToken;
          incompatible:
            token->undefine (valuation);
            goto incompatible2;
          }
          else {
          incompatible2:
            if (interrupted || reporter.isFatal ())
            return;
            if (token->next ())
            continue;
          }

          delete token;
          break;
        }
      }
      }
    }
    // everything unified => try to fire the transition
    else if (willDo (true, *this, valuation, m, reporter,
                 checkGates (valuation, errNone)
                 ? 0 : "undefined gate:") &&
           firstOutput (*this, valuation, m, reporter)) {
      /** tokens removed from the input places */
      class GlobalMarking inputs (lnet.getNet ());
      for (TokenList::const_iterator t = tokens.begin ();
         t != tokens.end (); t++) {
      const struct unif& unif = (*t)->getUnifier ();
      class PlaceMarking& pm = inputs[unif.place];
      if (!(*t)->copyRemoved (pm)) {
        willDo (false, *this, valuation, m, reporter,
              "input multiplicity overflow:");
        goto skip;
      }
      }

      valuation.setGlobalMarking (&inputs);

      // Fire the transition for all allowed bindings of output variables
      do {
      /** tokens added to the output places */
      class GlobalMarking outputs (lnet.getNet ());

      for (unsigned out = 0; out < myNumOutputs; out++) {
        const class Arc& arc = *myOutputs[out];
        class PlaceMarking& place = outputs[reporter.isFlattened ()
                                    ? arc.getPlace ().getIndex ()
                                    : arc.getIndex ()];
        if (!arc.getExpr ().add (place, 1, valuation)) {
          willDo (false, *this, valuation, m, reporter,
                "evaluating outputs:");
          goto skip;
        }
      }

      struct LNet::ltrans tr;
      tr.t = myRootIndex;
      class BitPacker buf;
      lnet.getNet ().encode (buf, *this, valuation, true);
      tr.data = const_cast<word_t*>(buf.getBuf ());
      tr.datalen = buf.getNumWords ();

      if (!tr.in.unfold (lnet, inputs) ||
          !tr.out.unfold (lnet, outputs) ||
          !lnet.addTransition (tr))
        willDo (false, *this, valuation, m, reporter, "unfolding:");
      for (unsigned i = outputs.getSize (); i--; ) {
        if (outputs[i].getPlace ()->isConstant () &&
            !(outputs[i] == inputs[i]))
          willDo (false, *this, valuation, m, reporter,
                "non-constant place:");
        cover[i].setUnion (outputs[i]);
      }
      }
      while (!interrupted && !reporter.isFatal () &&
           nextOutput (*this, valuation, m, reporter));

    skip:
      valuation.setGlobalMarking (0);
    }

    // Backtrack in the search
    while (!tokens.empty ()) {
      token = &tokens.pop ();
      token->setReservedUnfold (false);

      // Restore the reserved token to the input place
      if (token->isReserved ())
      token->free ();

      // If the token is "constant", backtrack further
      if (!(u = &token->getUnifier ())->vars) {
      delete token;
      continue;
      }

      goto incompatible;
    }

    break;
  }
}

/** Determine whether a variable is first unified from the specified token
 * @param u head of the token list
 * @param v limit for the search
 * @param var     variable to be examined
 * @return  false if the variable is unified from a token before v
 */
inline static bool
01904 isFirst (const struct unif* u,
       const struct unif* v,
       const class VariableDefinition& var)
{
  for (; u != v; u = u->next)
    if (u->varMult && u->vars && u->vars->contains (var))
      return false;
  return true;
}

void
01915 Transition::unfold (class LNet& lnet,
                class DummyReporter& reporter) const
{
  assert (&lnet.getNet ().getTransition (myRootIndex) == this);
  if (myKind)
    return; // this is a "fact" transition (an assertion)
  if (!myGates.empty () &&
      (*myGates.begin ())->getKind () == Expression::eConstant) {
    // there is a constant gate (which should be always disabled):
    // ignore the transition
#ifndef NDEBUG
    const class Expression* g = *myGates.begin ();
    const class Value& v = static_cast<const class Constant*>(g)->getValue ();
    assert (v.getKind () == Value::vLeaf);
    assert (!bool (static_cast<const class LeafValue&>(v)));
#endif // NDEBUG
    return;
  }
  class Valuation valuation;
  const struct unif* u = myUnif, *v;
  VariableSet::const_iterator vi;

  /** Dummy empty marking for diagnostics */
  const class GlobalMarking m (reporter.net);

  while (!interrupted && !reporter.isFatal ()) {
    assert (valuation.isOK ());
    if (!u) {
      if (willDo (true, *this, valuation, m, reporter,
              checkGates (valuation, errNone)
              ? 0 : "undefined gate:") &&
        firstOutput (*this, valuation, m, reporter)) {
      /** tokens removed from the input places */
      class GlobalMarking inputs (lnet.getNet ());
      /** transition variable iterator */
      const_iterator i;

      // clear the "referenced" flags of all variables */
      for (i = myVariables.begin (); i != myVariables.end (); i++)
        i->second->flagReferenced (false);

      // evaluate the input arcs
      for (unsigned in = 0; in < myNumInputs; in++) {
        const class Arc& arc = *myInputs[in];
        class PlaceMarking& place = inputs[reporter.isFlattened ()
                                   ? arc.getPlace ().getIndex ()
                                   : arc.getIndex ()];
        if (!arc.getExpr ().add (place, 1, valuation)) {
          if (valuation.getError () != errVar)
            willDo (false, *this, valuation, inputs, reporter,
                  "evaluating inputs:");
          goto cont;
        }
      }

      assert (valuation.isOK ());

      // check the "referenced" flags of the input variables
      for (i = myVariables.begin (); i != myVariables.end (); i++) {
        const class VariableDefinition& var = *i->second;
        if (var.isReferenced () || var.isAggregate () ||
            !valuation.getValue (var))
          continue;
        assert (var.isUndefined ());
        // An input variable is defined, even though it needn't be.
        // Thus, this is a redundant instance: backtrack
        goto cont;
      }

      // evaluate the output arcs
      valuation.setGlobalMarking (&inputs);

      do {
        /** tokens added to the output places */
        class GlobalMarking outputs (lnet.getNet ());

        for (unsigned out = 0; out < myNumOutputs; out++) {
          const class Arc& arc = *myOutputs[out];
          class PlaceMarking& place = outputs[reporter.isFlattened ()
                                    ? arc.getPlace ().getIndex ()
                                    : arc.getIndex ()];
          if (!arc.getExpr ().add (place, 1, valuation)) {
            willDo (false, *this, valuation, inputs, reporter,
                  "evaluating outputs:");
            goto cont;
          }
        }

        struct LNet::ltrans tr;
        tr.t = myRootIndex;
        class BitPacker buf;
        lnet.getNet ().encode (buf, *this, valuation, true);
        tr.data = const_cast<word_t*>(buf.getBuf ());
        tr.datalen = buf.getNumWords ();

        if (!tr.in.unfold (lnet, inputs) ||
            !tr.out.unfold (lnet, outputs) ||
            !lnet.addTransition (tr))
          willDo (false, *this, valuation, inputs, reporter, "unfolding:");
        for (unsigned o = outputs.getSize (); o--; ) {
          if (outputs[o].getPlace ()->isConstant () &&
            !(outputs[o] == inputs[o]))
            willDo (false, *this, valuation, inputs, reporter,
                  "non-constant place:");
        }
      }
      while (!interrupted && !reporter.isFatal () &&
             nextOutput (*this, valuation, inputs, reporter));

      valuation.setGlobalMarking (0);
      }
    cont:
#ifndef NDEBUG
      for (v = u; v; v = v->next)
      if (v->vars)
        for (vi = v->vars->begin (); vi != v->vars->end (); vi++)
          assert ((v->varMult && !::isFirst (myUnif, u, **vi)) ||
                !valuation.getValue (**vi));
#endif // NDEBUG
      const struct unif* w = 0;
      for (v = myUnif; v != u; v = v->next)
      if (v->vars) w = v;
      if (!(u = w))
      return;
      goto unify;
    }

    if ((u->varMult && !u->m->getMultiplicity (valuation)) || !u->vars) {
      if (valuation.isOK ())
      goto next;
      if (valuation.getError () == errVar) {
      valuation.clearErrors ();
      goto cont;
      }
    }
    if (valuation.isOK ()) {
      if (u->varMult) {
      for (vi = u->vars->begin (); vi != u->vars->end (); vi++)
        if (!valuation.getValue (**vi) && !::isFirst (myUnif, u, **vi))
          goto cont;
      }
      else {
      for (vi = u->vars->begin (); vi != u->vars->end (); vi++) {
        assert (!valuation.getValue (**vi));
        valuation.setValue (**vi, (*vi)->getType ().getFirstValue ());
      }
      }
    proceed:
      if (willDo (checkGates (valuation), *this, valuation, m, reporter))
      goto next;
    unify:
      if (u->varMult) {
      for (vi = u->vars->begin (); vi != u->vars->end (); vi++) {
        const class VariableDefinition& var = **vi;
        if (!::isFirst (myUnif, u, var)) continue;
        if (!valuation.getValue (var)) {
          valuation.setValue (var, var.getType ().getFirstValue ());
          goto proceed;
        }
        if (valuation.increment (var))
          goto proceed;
        valuation.undefine (var);
      }
      for (vi = u->vars->begin (); vi != u->vars->end (); vi++)
        if (::isFirst (myUnif, u->next, **vi))
          valuation.undefine (**vi);
      }
      else {
      for (vi = u->vars->begin (); vi != u->vars->end (); vi++)
        if (valuation.increment (**vi))
          goto proceed;
      for (vi = u->vars->begin (); vi != u->vars->end (); vi++)
        valuation.undefine (**vi);
      }
    }
    else
      willDo (false, *this, valuation, m, reporter, "undefined multiplicity:");
    goto cont;
  next:
    u = u->next;
    continue;
  }
}

void
02100 Transition::computeWeaklyFair (const class Valuation& valuation,
                         unsigned* sets) const
{
  assert (valuation.isOK ());
  assert (!!sets);
  *sets = 0;
  if (myNumWeaklyFair) {
    for (unsigned i = myNumWeaklyFair; i--; ) {
      if (class Value* value = myWeaklyFairCond[i]->eval (valuation)) {
      assert (value->getKind () == Value::vLeaf);
      if (bool (static_cast<class LeafValue&>(*value)))
        sets[++(*sets)] = myWeaklyFairSet[i];
      delete value;
      }
      else {
      assert (!valuation.isOK ());
      return;
      }
    }
  }
}

void
02123 Transition::computeStronglyFair (const class Valuation& valuation,
                         unsigned* sets) const
{
  assert (valuation.isOK ());
  assert (!!sets);
  *sets = 0;
  if (myNumStronglyFair) {
    for (unsigned i = myNumStronglyFair; i--; ) {
      if (class Value* value = myStronglyFairCond[i]->eval (valuation)) {
      assert (value->getKind () == Value::vLeaf);
      if (bool (static_cast<class LeafValue&>(*value)))
        sets[++(*sets)] = myStronglyFairSet[i];
      delete value;
      }
      else {
      assert (!valuation.isOK ());
      return;
      }
    }
  }
}

void
02146 Transition::logEnabled (const class Valuation& valuation,
                  char* log) const
{
  assert (valuation.isOK () && log);
  if (!myName) return;
  for (unsigned i = myNumEnabled; i--; ) {
    if (log[myEnabledSet[i]]);
    else if (class Value* value = myEnabledCond[i]->eval (valuation)) {
      assert (value->getKind () == Value::vLeaf);
      log[myEnabledSet[i]] = bool (static_cast<class LeafValue&>(*value));
      delete value;
    }
    else {
      assert (!valuation.isOK ());
      valuation.clearErrors ();
    }
  }
}

#ifdef EXPR_COMPILE
# include "CExpression.h"
# include "Net.h"
# include "util.h"

/** Compile transition output variable advancement
 * @param cexpr         compilation output
 * @param indent  indentation level
 * @param vars          the output variables
 * @param varbase name of the temporary variable
 * @param varsuffix     offset to varbase
 * @param fired         name of the "fired" flag
 */
static void
compileOutputAdvance (class CExpression& cexpr,
                  unsigned indent,
                  const class QuantifierList& vars,
                  const char* varbase,
                  char* varsuffix,
                  const char* fired)
{
  const char* wrap = cexpr.getTmpFlag ();
  class StringBuffer& out = cexpr.getOut ();
  QuantifierList::const_iterator i;
  for (i = vars.begin (); i != vars.end (); i++) {
    const class VariableDefinition& var = (*i)->getVariable ();
    const class Type& type = var.getType ();
    snprintf (varsuffix, 21, "%u", var.getNumber ());
    out.indent (indent), out.append (wrap), out.append ("=0;\n");
    type.compileSuccessor (out, indent, varbase, varbase, wrap);
    out.indent (indent);
    out.append ("if ("), out.append (wrap), out.append (") {\n");
    indent += 2;
  }

  out.indent (indent);
  out.append ("if ("), out.append (fired), out.append (")\n");
  cexpr.compileError (indent + 2, errComp);
  out.indent (indent), out.append (fired), out.append ("=1;\n");

  for (i = vars.begin (); i != vars.end (); i++)
    out.indent (indent -= 2), out.append ("}\n");

  for (i = vars.begin (); i != vars.end (); i++) {
    if (const class Expression* cond = (*i)->getCondition ()) {
      const char* pass = cexpr.getFlag ();
      cond->compile (cexpr, indent, pass, 0);
      out.indent (indent);
      out.append ("if (!"), out.append (pass), out.append (")\n");
      out.indent (indent + 2), out.append ("continue;\n");
    }
  }
}

/** Compile deassignment of optionally undefined variables
 * @param out           output stream
 * @param indent  indentation level
 * @param t       head of symbolic token list
 * @param u       current symbolic token
 */
static void
compileDeassign (class StringBuffer& out,
             unsigned indent,
             const struct unif* t,
             const struct unif* u)
{
  for (VariableSet::const_iterator vi = u->vars->begin ();
       vi != u->vars->end (); vi++) {
    const class VariableDefinition& var = **vi;
    if (var.isUndefined ()) {
      const struct unif* v;
      /** flag: could the variable have been assigned previously? */
      bool assigned = false;
      for (v = t; v != u; v = v->next) {
      if (v->vars && v->vars->contains (var)) {
        assigned = true;
        break;
      }
      }
      out.indent (indent);
      if (assigned) {
      /** index number of symbolic token */
      unsigned i;
      out.append ("if (");
      for (v = t, i = 0; v != u; v = v->next, i++) {
        if (v->vars && v->vars->contains (var)) {
          if (!assigned) {
            out.append ("&&\n");
            out.indent (indent + 4);
          }
          assigned = false;
          out.append ("!token"), out.append (i), out.append (".count");
        }
      }
      out.append (")\n");
      out.indent (indent + 2);
      }
      out.append ("DEASSIGN (vars, ");
      out.append (var.getNumber () - 1);
      out.append (");\n");
    }
  }
}

/** Compile code for determining whether a transition is hidden
 * @param out           output stream
 * @param indent  indentation level
 * @param t       head of symbolic token list
 * @param u       current symbolic token
 */
static void
compileHidden (class CExpression& cexpr,
             unsigned indent,
             const class Expression& expr,
             const char* flag)
{
  expr.compile (cexpr, indent, flag, 0);
}

void
Transition::compileAnalysis (class CExpression& cexpr,
                       const slist<const class Place*>&
                       inputPlaces,
                       unsigned numOptVars) const
{
  assert (!!myNet);
  /** base name for output variables */
  static const char varbase[] = "vars.x";
  /** output variable name */
  char varname[21 + sizeof varbase];
  memcpy (varname, varbase, sizeof varbase);
  /** base name for successor places */
  static const char msetbase[] = "mDest.p";
  /** successor place name */
  char msetname[21 + sizeof msetbase];
  memcpy (msetname, msetbase, sizeof msetbase);

  /** the output stream */
  class StringBuffer& out = cexpr.getOut ();

  if (!myGates.empty () &&
      (*myGates.begin ())->getKind () == Expression::eConstant) {
    // there is a constant gate (which should be always disabled):
    // ignore the transition
#ifndef NDEBUG
    const class Expression* g = *myGates.begin ();
    const class Value& v = static_cast<const class Constant*>(g)->getValue ();
    assert (v.getKind () == Value::vLeaf);
    assert (!bool (static_cast<const class LeafValue&>(v)));
#endif // NDEBUG
    out.append ("  return 0;\n");
    return;
  }

  cexpr.setFatalError ("return *fatal=1, ++numErrors;\n");

  const struct unif* u, *v;
  unsigned i, j;

  // variable declarations
  out.append ("  unsigned numErrors=0;\n");
  if (myOutputVariables)
    out.append ("  unsigned fired;\n");

  for (u = myUnif, i = 0; u; u = u->next, i++) {
    out.indent (2);
    if (myNet->getPlace (u->place)->getMaxNumTokens () == 1)
      out.append ("TOKEN1");
    else
      out.append (u->vars ? "TOKEN" : (u->isSet ? "TOKENM" : "TOKENC"));
    out.append (" (");
    u->m->getType ()->appendIndex (out);
    out.append (", ");
    out.append (i);
    out.append (");\n");
  }

  // check for insufficiently marked input places
  slist<const class Place*>::const_iterator p;
  out.append ("#ifdef TRANSITION_EMPTY\n"
            "  if (0");
  for (p = inputPlaces.begin (); p != inputPlaces.end (); p++) {
    if (!(*p)->getCapacityBits ())
      continue; // do not check places with constant number of tokens
    /** minimum number of tokens the place is guaranteed to contain */
    card_t minTokens = 0;

    if (const class Constraint* c = (*p)->getCapacity ()) {
      const class Value& value = c->getFirstValue ();
      assert (value.getKind () == Value::vLeaf);
      minTokens =
      static_cast<card_t>(static_cast<const class LeafValue&>(value));
    }
    /** minimum number of required tokens from the place */
    card_t reqTokens = 0;

    for (u = myUnif; u; u = u->next) {
      if (u->varMult || myNet->getPlace (u->place) != *p || u->isSet)
      continue;
      if (const class Expression* mult = u->m->getMultiplicity ()) {
      assert (mult->getKind () == Expression::eConstant);
      const class Value& value =
        static_cast<const class Constant*>(mult)->getValue ();
      assert (value.getKind () == Value::vLeaf);
      reqTokens +=
        static_cast<card_t>(static_cast<const class LeafValue&>(value));
      }
      else
      reqTokens++;
    }

    if (reqTokens > minTokens) {
      out.append ("\n      ||numTokens[");
      out.append ((*p)->getIndex ());
      out.append ("]<");
      out.append (reqTokens);
    }
  }
  out.append (")\n"
            "    return 0;\n"
            "#endif /* TRANSITION_EMPTY */\n");

  // clear the optional variables
  if (numOptVars)
    out.append ("  memset (vars.y, 0, sizeof vars.y);\n");

  // generate the unification code
  unsigned indent = 2;
  VariableSet::const_iterator vi;
  class VariableSet oldvars;
  for (u = myUnif, i = 0; u; u = u->next, i++) {
    char token[34];
    snprintf (token, sizeof token, "token%u.count", i);
    if (i) {
      out.append ("#define ERROR(err){numErrors++;goto cont");
      out.append (i);
      out.append (";}\n");
    }
    else
      out.append ("#define ERROR(err)return++numErrors\n");
    bool* checkpoint = 0;
    unsigned checkpointSize =
      u->varMult || u->isSet ? cexpr.getCheckpoint (checkpoint) : 0;
    if (!u->isSet) {
      u->m->compileMultiplicity (cexpr, indent, token, &oldvars);
      cexpr.compileCleanup (indent);
      if (u->varMult) {
      out.indent (indent);
      out.append ("if (!");
      out.append (token);
      out.append (") goto unified");
      out.append (i), out.append (";\n");
      }
    }
    out.append ("#undef ERROR\n");

    if (myNet->getPlace (u->place)->getMaxNumTokens () != 1) {
      out.indent (indent);
      out.append (u->vars ? "INIT_TOKEN" :
              (u->isSet ? "INIT_TOKENM" : "INIT_TOKENC"));
      out.append (" (");
      out.append (i);
      out.append (", mSrc.p");
      out.append (u->place);
      out.append (");\n");
    }

    out.indent (indent);
    out.append ("for (;;) {\n");
    indent += 2;

    if (myNet->getPlace (u->place)->getMaxNumTokens () == 1) {
      // place with at most one token: simpler data structure
      if (u->isSet) {
      // multiset-valued token: evaluate and compare to place contents
      snprintf (token, sizeof token, "token%u.item", i);
      out.append ("#define ERROR(err){numErrors++;break;}\n");
      out.indent (indent);
      out.append (token);
      out.append ("=0;\n");
      u->m->getToken ()->compileScalarMset (cexpr, indent, token, 0, true);
      cexpr.setCheckpoint (indent, checkpoint, checkpointSize);
      delete[] checkpoint;
      out.append ("#undef ERROR\n");
      out.indent (indent);
      out.append ("if (");
      out.append (token);
      out.append (" &&\n");
      out.indent (indent + 4);
      out.append ("(!mSrc.p");
      out.append (u->place);
      out.append (" ||\n");
      out.indent (indent + 6);
      out.append (" (\n");
      snprintf (token, sizeof token, "(*token%u.item)", i);
      char pm[34];
      snprintf (pm, sizeof pm, "(*mSrc.p%u)", i);
      if (!u->m->getType ()->compileEqual (out, indent + 6, token, pm,
                                   false, true, true, false))
        out.append ("0");
      out.append ("))) {\n");
      out.indent (indent + 2);
      out.append ("token");
      out.append (i);
      out.append (".item = 0;\n");
      out.indent (indent + 2);
      out.append ("break;\n");
      out.indent (indent);
      out.append ("}\n");
      }
      else {
      out.indent (indent);
      out.append ("if (!(token");
      out.append (i);
      out.append (".item=mSrc.p");
      out.append (u->place);
      out.append (")");
      if (u->m->getMultiplicity ())
        out.append ("||token"), out.append (i), out.append (".count!=1");
      out.append (") break;\n");
      snprintf (token, sizeof token, "(*token%u.item)", i);
      if (u->vars) {
        // token with variables: unify
        out.append ("#define ERROR(err) goto cont");
        out.append (i);
        out.append ("\n");
        for (vi = u->vars->begin (); vi != u->vars->end (); vi++)
          oldvars.insert (**vi);
        // bind the variables
        u->m->getToken ()->compileLvalue (cexpr, indent, *u->vars, token);

        // are all tokens unified so far compatible with the new bindings?
        for (j = 0, v = myUnif; j <= i; v = v->next, j++) {
          if (!v->m->getToken ()->depends (*u->vars, false))
            continue;
          if (v == u &&
            u->m->getToken ()->getKind () == Expression::eVariable &&
            u->vars->size () == 1 &&
            &static_cast<const class Variable*>
            (u->m->getToken ())->getVariable () == *u->vars->begin ())
            continue; // the token is a variable unified from the place
          bool hasMult = v->m->hasMultiplicity ();
          if (hasMult) {
            out.indent (indent);
            out.append ("if (token");
            out.append (j);
            out.append (".count) {\n");
            indent += 2;
          }
          snprintf (token, sizeof token, "(*token%u.item)", j);
          v->m->getToken ()->compileCompatible (cexpr, indent, oldvars, token);
          if (hasMult) {
            indent -= 2;
            out.indent (indent);
            out.append ("}\n");
          }
        }

        /** flag: has the error macro been redefined? */
        bool errors = false;
        // are all gates compatible with the new bindings?
        for (GateList::const_iterator g = myGates.begin ();
             g != myGates.end (); g++) {
          if (!(*g)->depends (*u->vars, false) ||
            (*g)->depends (oldvars, true))
            continue;
          if (!errors) {
            errors = true;
            out.append ("#undef ERROR\n"
                    "#define ERROR(err)"
                    "{if(err!=errVar&&err!=errComp)numErrors++;goto cont");
            out.append (i);
            out.append (";}\n");
          }
          const char* work = cexpr.getFlag ();
          out.indent (indent);
          out.append ("do {\n");
          (*g)->compile (cexpr, indent + 2, work, &oldvars);
          out.indent (indent + 2);
          out.append ("if (!");
          out.append (work);
          out.append (")\n");
          cexpr.compileError (indent + 4, errComp);
          out.indent (indent);
          out.append ("} while (0);\n");
        }

        out.append ("#undef ERROR\n");
        cexpr.compileCleanup (indent);
        out.indent (indent);
        out.append ("goto unified");
        out.append (i);
        out.append (";\n");
        if (u->varMult) {
          cexpr.setCheckpoint (indent, checkpoint, checkpointSize, false);
          ::compileDeassign (out, indent, myUnif, u);
        }
        out.indent (indent);
        out.append ("break;\n");
      }
      else if (u->m->getToken ()->getKind () == Expression::eConstant) {
        // constant token: compare to place contents
        out.indent (indent);
        out.append ("if (");
        if (!static_cast<const class Constant*>(u->m->getToken ())
            ->getValue ().compileEqual (out, indent + 4, token,
                                false, true, true))
          out.append ("0");
        out.append (") break;\n");
      }
      else {
        // scalar-valued token: evaluate and compare to place contents
        out.indent (indent);
        out.append ("else {\n");
        out.indent (indent + 2);
        u->m->getType ()->appendName (out);
        out.append (" item;\n"
                  "#define ERROR(err){numErrors++;break;}\n");
        u->m->getToken ()->compile (cexpr, indent + 2, "item", 0);
        out.append ("#undef ERROR\n");
        out.indent (indent + 2);
        out.append ("if (");
        if (!u->m->getType ()->compileEqual (out, indent + 6,
                                     token, "item",
                                     false, true, true, false))
          out.append ("0");
        out.append (") break;\n");
        out.indent (indent);
        out.append ("}\n");
      }
      }
    }
    else if (u->vars) {
      // token with variables: unify
      out.indent (indent - 2);
      out.append ("next");
      out.append (i);
      out.append (":\n");
      out.indent (indent);
      out.append ("while (token");
      out.append (i);
      out.append (".i) {\n");
      out.indent (indent + 2);
      out.append ("if (!ENOUGH_TOKEN (");
      out.append (i);
      out.append (")) { NEXT_TOKEN (");
      out.append (i);
      out.append ("); continue; }\n");

      snprintf (token, sizeof token, "token%u.i->item", i);

      // is the token compatible with the existing variable bindings?
      out.append ("#define ERROR(err){if(err==errVar)continue;\\\n"
              "else{NEXT_TOKEN (");
      out.append (i), out.append (");goto next");
      out.append (i), out.append (";}}\n");
      for (vi = u->vars->begin (); vi != u->vars->end (); vi++)
      oldvars.insert (**vi);
      // bind the variables
      u->m->getToken ()->compileLvalue (cexpr, indent + 2, *u->vars, token);

      // are all tokens unified so far compatible with the new bindings?
      for (j = 0, v = myUnif; j <= i; v = v->next, j++) {
      if (!v->m->getToken ()->depends (*u->vars, false))
        continue;
      if (v == u &&
          u->m->getToken ()->getKind () == Expression::eVariable &&
          u->vars->size () == 1 &&
          &static_cast<const class Variable*>
          (u->m->getToken ())->getVariable () == *u->vars->begin ())
        continue; // the token is a variable unified from the place
      bool hasMult = v->m->hasMultiplicity ();
      if (hasMult) {
        out.indent (indent + 2);
        out.append ("if (token"), out.append (j), out.append (".count) {\n");
        indent += 2;
      }
      snprintf (token, sizeof token, "token%u.i->item", j);
      v->m->getToken ()->compileCompatible (cexpr, indent + 2,
                                    oldvars, token);
      if (hasMult) {
        indent -= 2;
        out.indent (indent + 2);
        out.append ("}\n");
      }
      }

      // are all gates compatible with the new bindings?
      for (GateList::const_iterator g = myGates.begin ();
         g != myGates.end (); g++) {
      if (!(*g)->depends (*u->vars, false) ||
          (*g)->depends (oldvars, true))
        continue;
      const char* work = cexpr.getFlag ();
      out.indent (indent + 2);
      out.append ("do {\n");
      (*g)->compile (cexpr, indent + 4, work, &oldvars);
      out.indent (indent + 4);
      out.append ("if (!");
      out.append (work);
      out.append (")\n");
      cexpr.compileError (indent + 6, errComp);
      out.indent (indent + 2);
      out.append ("} while (0);\n");
      }

      out.append ("#undef ERROR\n");
      cexpr.compileCleanup (indent + 2);
      out.indent (indent + 2);
      out.append ("goto unified");
      out.append (i);
      out.append (";\n");
      out.indent (indent);
      out.append ("}\n");
      if (u->varMult) {
      cexpr.setCheckpoint (indent, checkpoint, checkpointSize, false);
      ::compileDeassign (out, indent, myUnif, u);
      }
      out.indent (indent);
      out.append ("break;\n");
    }
    else if (u->isSet) {
      // multiset-valued token: evaluate and see if subset of input marking
      out.append ("#define ERROR(err){numErrors++;break;}\n");
      snprintf (token, sizeof token, "token%u.v", i);
      u->m->getToken ()->compileMset (cexpr, indent, 0, token, 0);
      cexpr.setCheckpoint (indent, checkpoint, checkpointSize);
      delete[] checkpoint;
      out.append ("#undef ERROR\n");
      out.indent (indent);
      out.append ("if (!FIND_TOKENM (");
      out.append (i);
      out.append (", ");
      u->m->getType ()->appendIndex (out);
      out.append (")) { FREE (");
      out.append (token);
      out.append ("); break; }\n");
    }
    else {
      // scalar-valued token: evaluate and search for it in the place
      out.append ("#define ERROR(err){numErrors++;break;}\n");
      snprintf (token, sizeof token, "token%u.item", i);
      u->m->getToken ()->compile (cexpr, indent, token, 0);
      out.append ("#undef ERROR\n");
      out.indent (indent);
      out.append ("if (!FIND_TOKEN (");
      out.append (i);
      out.append (", ");
      u->m->getType ()->appendIndex (out);
      out.append (")) break;\n");
    }

    // unified a token
    out.indent (indent - 2);
    out.append ("unified");
    out.append (i);
    out.append (":\n");
    if (u->varMult && !u->isSet) {
      cexpr.setCheckpoint (indent, checkpoint, checkpointSize);
      delete[] checkpoint;
    }

    out.indent (indent);
    if (u->varMult) {
      out.append ("if (token");
      out.append (i);
      out.append (".count)\n");
      out.indent (indent + 2);
    }

    if (myNet->getPlace (u->place)->getMaxNumTokens () == 1) {
      out.append ("mSrc.p");
      out.append (u->place);
      out.append ("=0;\n");
    }
    else if (u->isSet) {
      // multiset-valued token
      out.append ("RESERVE_TOKENM (");
      out.append (i);
      out.append (", ");
      u->m->getType ()->appendIndex (out);
      out.append (");\n");
    }
    else {
      // scalar-valued token
      out.append ("RESERVE_TOKEN (");
      out.append (i);
      out.append (");\n");
    }
  }

  out.append ("#define ERROR(err){if (err!=errComp)numErrors++;goto cont");
  out.append (i);
  out.append (";}\n");

  // check the gates depending on possibly undefined variables
  class VariableSet undefVars;
  for (const_iterator ui = myVariables.begin ();
       ui != myVariables.end (); ui++) {
    const class VariableDefinition& var = *ui->second;
    if (var.isUndefined ()) undefVars.insert (var);
  }
  for (GateList::const_iterator g = myGates.begin ();
       g != myGates.end (); g++)
    if ((*g)->depends (undefVars, false))
      (*g)->compile (cexpr, indent, cexpr.getFlag (), 0);

  if (myKind) {
    // an assertion transition is enabled
    out.append ("#undef ERROR\n");
    cexpr.compileCleanup (indent);
    // unwind the unification stack and return
    for (unsigned k = i; k--; ) {
      for (u = myUnif, j = k; j--; u = u->next);
      out.indent (indent);
      if (myNet->getPlace (u->place)->getMaxNumTokens () == 1) {
      out.append ("mSrc.p");
      out.append (u->place);
      out.append (" = token");
      out.append (k);
      out.append (".item;\n");
      }
      else if (u->isSet) {
      out.append ("RELEASE_TOKENM (");
      out.append (k);
      out.append (", ");
      u->m->getType ()->appendIndex (out);
      out.append (");\n");
      }
      else {
      out.append ("RELEASE_TOKEN (");
      out.append (k);
      out.append (");\n");
      }

      if (u->vars)
      ::compileDeassign (out, indent, myUnif, u);
    }
    if (myKind == tFatal)
      cexpr.compileError (indent, errFatal);
    else {
      out.indent (indent);
      out.append ("return ++numErrors;\n");
    }
    i--;
    goto finish;
  }

  if (myNumParents) {
    // report that a synchronisation transition is enabled
    out.indent (indent);
    out.append ("(*syncstate) (");
    out.append (myLocalIndex);
    out.append (", ctx);\n");
    goto skip;
  }

  if (myOutputMarking) {
    // Determine which place markings are referenced from the output arcs
    class BitVector outputArcs (myNet->getNumPlaces ());
    for (unsigned arc = 0; arc < myNumOutputs; arc++)
      if (!myOutputs[arc]->getExpr ().forVariables (&::findOutput,
                                        &outputArcs))
      assert (false);
    cexpr.setMultiset ("mIn");
    out.indent (indent);
    out.append ("freem (&mIn);\n");
    for (u = myUnif, i = 0; u; u = u->next, i++) {
      if (!outputArcs[u->place])
      continue;
      out.indent (indent);
      if (myNet->getPlace (u->place)->getMaxNumTokens () == 1) {
      out.append ("if (token"), out.append (i);
      out.append (".item)\n");
      out.indent (indent + 2);
      out.append ("mIn.p"), out.append (u->place);
      out.append ("=memcpy(malloc(sizeof(");
      u->m->getType ()->appendName (out);
      out.append (")), token"), out.append (i);
      out.append (".item, sizeof(");
      u->m->getType ()->appendName (out);
      out.append ("));\n");
      }
      else {
      out.append ("mIn.p"), out.append (u->place);
      out.append ("=insert");
      u->m->getType ()->appendIndex (out);
      out.append (" (mIn.p"), out.append (u->place);
      out.append (", &token"), out.append (i);
      out.append (".i->item, token"), out.append (i);
      out.append (".count);\n");
      }
    }
  }

  if (myOutputVariables) {
    // initialize the output variables to maximum values
    QuantifierList::const_iterator q;
    /** flag: is there a condition on the output variables? */
    bool cond = false;
    for (q = myOutputVariables->begin ();
       q != myOutputVariables->end (); q++) {
      const class VariableDefinition& var = (*q)->getVariable ();
      if ((*q)->getCondition ())
      cond = true;
      snprintf (varname + (sizeof varbase) - 1, 21, "%u", var.getNumber ());
      var.getType ().compileTop (out, indent, varname);
    }
    out.indent (indent);
    out.append ("fired=0;\n");
    out.indent (indent);
    out.append ("while (!*intr && !*fatal) {\n");
    indent += 2;

    if (cond) {
      out.indent (indent);
      out.append ("for (;;) {\n");
      ::compileOutputAdvance (cexpr, indent + 2, *myOutputVariables, varname,
                        varname + (sizeof varbase) - 1,
                        "fired");
      out.indent (indent + 2);
      out.append ("break;\n");
      out.indent (indent);
      out.append ("}\n");
    }
    else
      ::compileOutputAdvance (cexpr, indent, *myOutputVariables, varname,
                        varname + (sizeof varbase) - 1,
                        "fired");
  }
  out.indent (indent);
  out.append ("initm ();\n");
  // fire the outputs
  for (unsigned arc = 0; arc < myNumOutputs; arc++) {
    const class Place& place = myOutputs[arc]->getPlace ();
    assert (myOutputs[arc]->isOutput ());
    snprintf (msetname + (sizeof msetbase) - 1, 22, "%u", place.getIndex ());

    bool* checkpoint = 0;
    unsigned checkpointSize = 0;
    if (place.isImplicit ()) {
      checkpointSize = cexpr.getCheckpoint (checkpoint);
      out.append ("#if !NO_INVARIANT_CHECK(");
      out.append (place.getIndex ());
      out.append (")\n");
    }

    if (place.getMaxNumTokens () == 1) {
      myOutputs[arc]->getExpr ().compileScalarMset (cexpr, indent,
                                        msetname, 0, true);
      out.indent (indent);
      out.append ("if (");
      out.append (msetname);
      out.append (")\n");
      out.indent (indent + 2);
      out.append (msetname);
      out.append (" = memcpy (malloc (sizeof *");
      out.append (msetname);
      out.append ("), ");
      out.append (msetname);
      out.append (", sizeof *");
      out.append (msetname);
      out.append (");\n");
      if (!place.getCapacityBits ()) {
      out.indent (indent);
      out.append ("else\n");
      cexpr.compileError (indent + 2, errConst);
      }
    }
    else
      myOutputs[arc]->getExpr ().compileMset (cexpr, indent, 0, msetname, 0);

    if (place.isImplicit ()) {
      out.append ("#endif /* NO_INVARIANT_CHECK */\n");
      cexpr.setCheckpoint (indent, checkpoint, checkpointSize);
      delete[] checkpoint;
    }
  }
  cexpr.setMultiset (0);
  // compute the enabling sets
  if (myNumEnabled) {
    const char* work = cexpr.getFlag ();
    out.indent (indent), out.append ("if (log) {\n");
    for (j = 0; j < myNumEnabled; j++) {
      out.indent (indent + 2);
      out.append ("if (!log["), out.append (j), out.append ("]) {\n");
      myEnabledCond[j]->compile (cexpr, indent + 4, work, 0);
      out.indent (indent + 4);
      out.append ("log["), out.append (j), out.append ("] = ");
      out.append (work), out.append (";\n");
      out.indent (indent + 2);
      out.append ("}\n");
    }
    out.indent (indent), out.append ("}\n");
  }
  // encode the marking and add the arcs
  // determine whether the transition is hidden
  if (myHide) {
    const char* work = cexpr.getFlag ();
    ::compileHidden (cexpr, indent, *myHide, work);
    cexpr.compileCleanup (indent);
    out.indent (indent);
    out.append ("if (encode ("), out.append (myNet->getIndex ());
    out.append (", "), out.append (myLocalIndex);
    out.append (", "), out.append (myRootIndex);
    out.append (", "), out.append (work), out.append (", ctx))\n");
  }
  else {
    cexpr.compileCleanup (indent);
    out.indent (indent);
    out.append ("if (encode ("), out.append (myNet->getIndex ());
    out.append (", "), out.append (myLocalIndex);
    out.append (", "), out.append (myRootIndex);
    out.append (", 0, ctx))\n");
  }
  cexpr.compileError (indent + 2, errCard);
  // encode the arc inscription
  out.indent (indent);
  out.append ("if (arcs) e ();\n");
  if (myOutputVariables)
    out.indent (indent -= 2), out.append ("}\n");
 skip:
  out.append ("#undef ERROR\n");
  if (i) {
    out.indent (indent - 2);
    out.append ("cont");
    out.append (i);
    out.append (":\n");
    out.indent (indent);
    out.append ("if (*intr || *fatal) return numErrors;\n");
  }

  // move to next token
  while (i--) {
    for (u = myUnif, j = i; j--; u = u->next);
    if (u->next) {
      out.indent (indent - 2);
      out.append ("cont");
      out.append (i + 1);
      out.append (":\n");
    }

    if (u->varMult) {
      out.indent (indent);
      out.append ("if (!token"), out.append (i), out.append (".count)\n");
      out.indent (indent + 2);
      out.append ("goto cont"), out.append (i), out.append (";\n");
    }

    out.indent (indent);
    if (myNet->getPlace (u->place)->getMaxNumTokens () == 1) {
      out.append ("mSrc.p");
      out.append (u->place);
      out.append (" = token");
      out.append (i);
      out.append (".item;\n");

      if (u->vars)
      ::compileDeassign (out, indent, myUnif, u);

      out.indent (indent);
      out.append ("break;\n");
    }
    else {
      if (u->isSet) {
      out.append ("RELEASE_TOKENM (");
      out.append (i);
      out.append (", ");
      u->m->getType ()->appendIndex (out);
      out.append (");\n");
      }
      else {
      out.append ("RELEASE_TOKEN (");
      out.append (i);
      out.append (");\n");
      }
      if (u->vars) {
      ::compileDeassign (out, indent, myUnif, u);
      out.indent (indent);
      out.append ("NEXT_TOKEN (");
      out.append (i);
      out.append (");\n");
      out.indent (indent);
      out.append ("if (!token");
      out.append (i);
      out.append (".i)\n");
      out.indent (indent + 2);
      }
      else
      out.indent (indent);
      out.append ("goto cont"), out.append (i), out.append (";\n");
    }
 finish:
    out.indent (indent -= 2);
    out.append ("}\n");
  }

  // finish
  cexpr.compileCleanup (indent);
  cexpr.setFatalError (0);
  out.append ("cont0:\n"
            "  return numErrors;\n");
}

/** Compile transition instance encoder
 * @param cexpr         compilation output
 * @param numTrans      number of transitions in the net
 * @param i       index number of the transition
 * @param vars          transition variables
 */
inline static void
compileEncoder (class CExpression& cexpr,
            unsigned i,
            unsigned numTrans,
            const Transition::VariableMap& vars)
{
  class StringBuffer& out = cexpr.getOut ();
  if (numTrans > 1) {
    out.append ("  enc (");
    out.append (i);
    out.append (", ");
    out.append (log2 (numTrans));
    out.append (");\n");
  }
  static const char varbase[] = "vars.";
  char varname[21 + sizeof varbase];
  memcpy (varname, varbase, sizeof varbase);

  for (Transition::const_iterator v = vars.begin (); v != vars.end (); v++) {
    const class VariableDefinition& var = *v->second;
    if (var.isUndefined ()) {
      snprintf (varname + (sizeof varbase) - 1, 22, "y%u", var.getNumber ());
      out.append ("  if (ASSIGNED (vars, ");
      out.append (var.getNumber () - 1);
      out.append (")) {\n    enc (0, 1);\n");
      var.getType ().compileEncoder (cexpr, 4, "enc", varname);
      out.append ("  }\n  else\n    enc (1, 1);\n");
    }
    else {
      snprintf (varname + (sizeof varbase) - 1, 22, "x%u", var.getNumber ());
      var.getType ().compileEncoder (cexpr, 2, "enc", varname);
    }
  }
}

/** Compile transition instance decoder and fairness checks
 * @param cexpr         compilation output
 * @param vars          transition variables
 */
inline static void
compileDecoder (class CExpression& cexpr,
            const Transition::VariableMap& vars)
{
  static const char varbase[] = "vars.";
  char varname[21 + sizeof varbase];
  memcpy (varname, varbase, sizeof varbase);
  class StringBuffer& out = cexpr.getOut ();

  for (Transition::const_iterator v = vars.begin (); v != vars.end (); v++) {
    const class VariableDefinition& var = *v->second;
    if (var.isUndefined ()) {
      snprintf (varname + (sizeof varbase) - 1, 22, "y%u", var.getNumber ());
      out.append ("  if (dec (1))\n    DEASSIGN (vars, ");
      out.append (var.getNumber () - 1);
      out.append (");\n"
              "  else {\n"
              "    ASSIGN (vars, ");
      out.append (var.getNumber () - 1);
      out.append (");\n");
      var.getType ().compileDecoder (cexpr, 4, "dec", varname);
      out.append ("  }\n");
    }
    else {
      snprintf (varname + (sizeof varbase) - 1, 22, "x%u", var.getNumber ());
      var.getType ().compileDecoder (cexpr, 2, "dec", varname);
    }
  }
}

/** Compile fairness constraints
 * @param cexpr         compilation output
 * @param indent  indentation level
 * @param fair          variable name of the computed fairness set
 * @param numFair number of fairness constraints
 * @param fairCond      the fairness conditions
 * @param fairSet the fairness set numbers
 */
static void
compileFairness (class CExpression& cexpr,
             unsigned indent,
             const char* fair,
             unsigned numFair,
             const class Expression*const* fairCond,
             const unsigned* fairSet)
{
  const char* work = 0;
  class StringBuffer& out = cexpr.getOut ();
  out.indent (indent);
  out.append ("*"), out.append (fair), out.append (" = 0;\n");
  for (unsigned i = numFair; i--; ) {
    if (!work) work = cexpr.getFlag ();
    fairCond[i]->compile (cexpr, indent, work, 0);
    out.indent (indent);
    out.append ("if ("); out.append (work); out.append (") ");
    out.append (fair), out.append ("[++*(");
    out.append (fair), out.append (")]=");
    out.append (fairSet[i]);
    out.append (";\n");
  }
}

/** Compile constant declarations
 * @param out           the output stream
 * @param numConstants  number of constants
 * @param constants     the constants
 * @param constantNames the names of the constants
 */
inline static void
compileConstantDecl (class StringBuffer& out,
                 unsigned numConstants,
                 const class Constant*const* constants,
                 const char*const* constantNames)
{
  class Printer printer;
  printer.setOutput (&out);
  for (unsigned i = 0; i < numConstants; i++) {
    out.append ("#if 0\n");
    printer.printQuoted (constantNames[i]);
    out.append ("\n"
            "#endif\n"
            "static ");
    constants[i]->getType ()->appendName (out);
    out.append (" c_");
    out.append (i);
    out.append (";\n");
  }
}

/** Compile constant initializations
 * @param out           the output stream
 * @param numConstants  number of constants
 * @param constants     the constants
 */
inline static void
compileConstantInit (class StringBuffer& out,
                 unsigned numConstants,
                 const class Constant*const* constants)
{
  char name[23];
  for (unsigned i = 0; i < numConstants; i++) {
    snprintf (name, sizeof name, "c_%u", i);
    constants[i]->getValue ().compileInit (name, 2, out);
  }
}

void
Transition::compile (class StringBuffer& out) const
{
  assert (!!myNet);
  class CExpression cexpr (out, *myNet, this);
  out.append ("#include \"mset.h\"\n"
            "#include \"event.h\"\n"
            "#include \"token.h\"\n\n"
            "#ifdef TRANSITION_ID\n"
            "static const char transition_id[] = ");
  {
    class Printer printer;
    printer.setOutput (&out);
    printer.printQuoted (myName);
  }
  out.append (";\n"
            "#endif\n\n"
            "#ifndef NO_INVARIANT_CHECK\n"
            "# define NO_INVARIANT_CHECK(p) 0\n"
            "#endif\n\n");
  unsigned numOptVars = 0;
  if (!myVariables.empty ()) {
    out.append ("static struct {\n");
    unsigned numVars = 0;
    for (const_iterator i = myVariables.begin ();
       i != myVariables.end (); i++) {
      const class VariableDefinition& var = *i->second;
      out.indent (2);
      var.getType ().appendName (out);
      numVars++;
      if (var.isUndefined ()) {
      const_cast<class VariableDefinition&>(var).setNumber (++numOptVars);
      out.append (" y");
      }
      else {
      const_cast<class VariableDefinition&>(var).setNumber (numVars);
      out.append (" x");
      }
      out.append (var.getNumber ());
      out.append (";\n");
    }
    if (numOptVars) {
      out.append ("  unsigned long y[(");
      out.append (numOptVars);
      out.append (" + sizeof (long) - 1) / sizeof (long)];\n");
    }
    out.append ("} vars;\n\n");
    cexpr.setValuation ("vars");
  }

  ::compileConstantDecl (out, myNumConstants, myConstants, myConstantNames);
  out.append ("extern void\ni");
  out.append (myRootIndex);
  out.append (" (void)\n{\n");
  ::compileConstantInit (out, myNumConstants, myConstants);
  out.append ("}\n");

  slist<const class Place*> inputPlaces;
  slist<const class Place*>::const_iterator ini;
  for (unsigned in = myNumInputs; in--; ) {
    for (ini = inputPlaces.begin (); ini != inputPlaces.end (); ini++)
      if (*ini == &myInputs[in]->getPlace ()) break;
    if (ini == inputPlaces.end ())
      inputPlaces.push_front (&myInputs[in]->getPlace ());
  }

  // encoding
  {
    const class Net* root = myNet;
    while (root->getParent ())
      root = root->getParent ();
    ::compileEncoder (cexpr, myRootIndex,
                  root->getNumAllTransitions (), myVariables);
  }
  cexpr.compileCleanup (2);
  out.append ("static void\ne (void)\n{\n");
  cexpr.generate ();
  out.append ("}\n");

  // instance analysis
  compileAnalysis (cexpr, inputPlaces, numOptVars);
  out.append ("extern unsigned\na");
  out.append (myRootIndex);
  out.append (" (void* ctx, char* log)\n{\n");
  cexpr.generate ();
  out.append ("}\n");

  // decoding
  ::compileDecoder (cexpr, myVariables);
  cexpr.getOut ().append ("#define ERROR(err) return err\n");
  ::compileFairness (cexpr, 2, "wfair",
                 myNumWeaklyFair, myWeaklyFairCond, myWeaklyFairSet);
  cexpr.getOut ().append ("  if (sf) {\n");
  ::compileFairness (cexpr, 4, "sfair",
                 myNumStronglyFair, myStronglyFairCond, myStronglyFairSet);
  cexpr.getOut ().append ("  }\n"
                    "#undef ERROR\n"
                    "  return errNone;\n");
  cexpr.compileCleanup (2);
  out.append ("enum Error\nd");
  out.append (myRootIndex);
  out.append (" (unsigned sf)\n{\n");
  cexpr.generate ();
  out.append ("}\n");
}
#endif // EXPR_COMPILE

void
03328 Transition::display (const class Printer& printer) const
{
  printer.printRaw ("trans");
  printer.delimiter (' ');
  printer.print (myName);
  if (myPriority)
    printer.delimiter (' '), printer.print (myPriority);
  printer.finish ();
  if (myKind) {
    printer.printRaw (myKind == tFatal ? "gate fatal" : "gate undefined");
    printer.finish ();
  }

  if (myOutputVariables) {
    printer.delimiter ('{')++.linebreak ();

    for (QuantifierList::const_iterator i = myOutputVariables->begin ();
       i != myOutputVariables->end (); i++) {
      const class VariableDefinition& v = (*i)->getVariable ();
      if (const char* name = v.getType ().getName ())
      printer.print (name);
      else
      printer.print (v.getType ().getSyntacticName ());
      printer.delimiter (' ');
      printer.print (v.getName ());
      printer.delimiter ('!');
      if (const class Expression* cond = (*i)->getCondition ()) {
      printer.delimiter ('(')++;
      cond->display (printer);
      --printer.delimiter (')');
      }
      printer.delimiter (';');
      printer.linebreak ();
    }
    printer--;
    printer.linebreak ();
    printer.delimiter ('}').finish ();
  }
  unsigned i;
  if (myNumInputs) {
    printer.finish ();
    printer.printRaw ("in ");
    printer.delimiter ('{')++;
    for (i = 0; i < myNumInputs; i++) {
      printer.linebreak ();
      printer.printRaw ("place ");
      printer.print (myInputs[i]->getPlace ().getName ());
      printer.delimiter (':');
      myInputs[i]->getExpr ().display (printer);
      printer.delimiter (';');
    }
    printer--;
    printer.linebreak ();
    printer.delimiter ('}');
  }

  if (myNumOutputs) {
    printer.finish ();
    printer.printRaw ("out ");
    printer.delimiter ('{')++;
    for (i = 0; i < myNumOutputs; i++) {
      printer.linebreak ();
      printer.printRaw ("place ");
      printer.print (myOutputs[i]->getPlace ().getName ());
      printer.delimiter (':');
      myOutputs[i]->getExpr ().display (printer);
      printer.delimiter (';');
    }
    printer--;
    printer.linebreak ();
    printer.delimiter ('}');
  }

  if (!myGates.empty ()) {
    printer.finish ();
    printer.printRaw ("gate ");
    for (GateList::const_iterator g = myGates.begin ();; ) {
      (*g)->display (printer);
      if (++g == myGates.end ())
      break;
      printer.delimiter (',');
    }
  }

  if (myHide) {
    printer.finish ();
    printer.printRaw ("hide ");
    myHide->display (printer);
  }

  if (myNumWeaklyFair) {
    printer.finish ();
    printer.printRaw ("weakly_fair ");
    for (i = 0;;) {
      printer.printRaw ("/*");
      printer.print (myWeaklyFairSet[i]);
      printer.printRaw ("*/");
      myWeaklyFairCond[i]->display (printer);
      if (++i == myNumWeaklyFair)
      break;
      printer.delimiter (',');
    }
  }
  if (myNumStronglyFair) {
    printer.finish ();
    printer.printRaw ("strongly_fair ");
    for (i = 0;;) {
      printer.printRaw ("/*");
      printer.print (myStronglyFairSet[i]);
      printer.printRaw ("*/");
      myStronglyFairCond[i]->display (printer);
      if (++i == myNumStronglyFair)
      break;
      printer.delimiter (',');
    }
  }
  if (myNumEnabled) {
    printer.finish ();
    printer.printRaw ("enabled ");
    for (i = 0;;) {
      printer.printRaw ("/*");
      printer.print (myEnabledSet[i]);
      printer.printRaw ("*/");
      myEnabledCond[i]->display (printer);
      if (++i == myNumEnabled)
      break;
      printer.delimiter (',');
    }
  }

  printer.delimiter (';');
  printer.finish ();
}

Generated by  Doxygen 1.6.0   Back to index