Logo Search packages:      
Sourcecode: maria version File versions

Net.C

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

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "Net.h"
#include "Place.h"
#include "Transition.h"
#include "Arc.h"
#include "Type.h"
#include "BoolType.h"
#include "IntType.h"
#include "CardType.h"
#include "CharType.h"
#include "GlobalMarking.h"
#include "Marking.h"
#include "Constant.h"
#include "Valuation.h"
#include "VariableDefinition.h"
#include "Function.h"
#include "BooleanBinop.h"
#include "PlaceContents.h"
#include "LeafValue.h"
#include "Quantifier.h"
#include "Printer.h"
#include "StateSet.h"
#include "Property.h"
#include "Dotty.h"

/** @file Net.C
 * Nested modular 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. */

/** The predefined boolean type */
00057 static class BoolType boolType;
/** The predefined signed integer type */
00059 static class IntType intType;
/** The predefined unsigned integer type */
00061 static class CardType cardType;
/** The predefined character type */
00063 static class CharType charType;

/** Determine whether a type is predefined
 * @param type    type to be checked
 * @return  true if the type is predefined
 */
inline static bool
00070 isPredefinedType (const class Type* type)
{
  return
    type == &boolType || type == &intType ||
    type == &cardType || type == &charType;
}

/** Determine whether a state is fatally rejected
 * @param m       the state
 * @param expr          the rejection condition
 * @return        the status of the check
 */
static enum Net::Status
00083 isFatal (const class GlobalMarking& m,
       const class Expression& expr)
{
  class Valuation valuation;
  valuation.setGlobalMarking (&m);
  bool rejected = false;
  if (class Value* value = expr.eval (valuation)) {
    assert (value->getKind () == Value::vLeaf);
    rejected = bool (static_cast<class LeafValue&>(*value));
    delete value;
    if (!rejected)
      return Net::OK;
  }
  return rejected ? Net::Error : Net::Fatal;
}

00099 Net::Net (
#ifdef EXPR_COMPILE
        unsigned ix,
#endif // EXPR_COMPILE
        class Net* parent,
        unsigned parentix,
        char* name) :
#ifdef EXPR_COMPILE
  myIndex (ix), myNumDescendents (0), myNumCompiled (0),
#endif // EXPR_COMPILE
  myName (name), myParent (parent), myParentIndex (parentix),
  myNumChildren (0), myChildren (0),
  myMaxPriority (UINT_MAX),
  myNumPlaces (parent ? parent->myNumPlaces : 0), myPlaces (0),
  myNumTransitions (0), myNumAllTransitions (0), myTransitions (0),
  myNumCallees (0), myCallees (0),
  myFunctionMap (), myPlaceMap (), myTransitionMap (), myCalleeMap (),
  myTypeMap (), myTypeList (),
  myInitMarking (0),
  myReject (0), myDeadlock (0),
  myNumWeaklyFair (0), myNumStronglyFair (0), myNumMaxFair (0),
  myNumEnabled (0),
  myNumProps (0), myPropNames (0), myProps (0),
  myNumConstants (0), myConstantNames (0), myConstants (0)
{
  if (myNumPlaces) {
    unsigned n;
    for (n = 1; n <= myNumPlaces; n <<= 1);
    myPlaces = new class Place*[n];
    memset (myPlaces, 0, myNumPlaces * sizeof *myPlaces);
  }
}

00132 Net::~Net ()
{
  unsigned i;
  for (i = myNumPlaces; i--; )
    if (myPlaces[i] && &myPlaces[i]->getNet () != this)
      myPlaces[i] = 0; // clear references to places in child nets

  delete[] myName;
  for (i = myNumChildren; i--; )
    delete myChildren[i];
  delete[] myChildren;

  for (i = myNumPlaces; i--; )
    if (myPlaces[i] && &myPlaces[i]->getNet () == this)
      delete myPlaces[i];
  delete[] myPlaces;

  for (i = myNumTransitions; i--; )
    delete myTransitions[i];
  delete[] myTransitions;

  for (i = myNumCallees; i--; )
    delete myCallees[i];
  delete[] myCallees;

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

  for (TypeList::iterator t = myTypeList.begin ();
       t != myTypeList.end (); t++) {
    class Type* const type = *t;
    // do not delete types defined in parent nets
    for (const class Net* p = myParent; p; p = p->myParent)
      for (TypeList::const_iterator pt = p->myTypeList.begin ();
         pt != p->myTypeList.end (); pt++)
      if (*pt == type)
        goto notmytype;
    // do not delete predefined types
    if (!::isPredefinedType (type))
      delete type;
  notmytype:
    continue;
  }

  delete myInitMarking;
  myReject->destroy ();
  myDeadlock->destroy ();
  for (i = myNumProps; i--; ) {
    delete[] myPropNames[i];
    myProps[i]->destroy ();
  }
  delete[] myPropNames;
  delete[] myProps;
  for (i = myNumConstants; i--; ) {
    delete[] myConstantNames[i];
    myConstants[i]->destroy ();
  }
  delete[] myConstantNames;
  delete[] myConstants;
}

class Net&
00195 Net::addChild (char* name)
{
  if (!(myNumChildren & (myNumChildren + 1))) {
    class Net** n = new class Net*[(myNumChildren + 1) << 1];
    memcpy (n, myChildren, sizeof (*myChildren) * myNumChildren);
    delete[] myChildren;
    myChildren = n;
  }

#ifdef EXPR_COMPILE
  /** the root net */
  class Net* root = this;
  while (root->myParent) root = root->myParent;
#endif // EXPR_COMPILE

  myChildren[myNumChildren] =
    new class Net (
#ifdef EXPR_COMPILE
               ++root->myNumDescendents,
#endif // EXPR_COMPILE
               this, myNumChildren, name);
  return *myChildren[myNumChildren++];
}

void
00220 Net::addPlaces (const class Transition& t)
{
  unsigned i;
  for (i = t.getNumInputs (); i--; ) {
    unsigned p = t.getInput (i).getPlace ().getIndex ();
    assert (p < myNumPlaces);
    assert (p < myParent->myNumPlaces);
    assert (!myPlaces[p] || myPlaces[p] == myParent->myPlaces[p]);
    myPlaces[p] = myParent->myPlaces[p];
  }
  for (i = t.getNumOutputs (); i--; ) {
    unsigned p = t.getOutput (i).getPlace ().getIndex ();
    assert (p < myNumPlaces);
    assert (p < myParent->myNumPlaces);
    assert (!myPlaces[p] || myPlaces[p] == myParent->myPlaces[p]);
    myPlaces[p] = myParent->myPlaces[p];
  }
}

void
00240 Net::addFunction (class Function& function)
{
  assert (!getFunction (function.getName ()));
  myFunctionMap[function.getName ()] = &function;
}

bool
00247 Net::addConstraint (class Expression& qualifier,
                enum CKind kind)
{
  unsigned id = UINT_MAX;
  switch (kind) {
  case Weak:
    id = myNumWeaklyFair; break;
  case Strong:
    id = myNumStronglyFair; break;
  case Enabled:
    id = myNumEnabled; break;
  }
  assert (id != UINT_MAX);
  if (qualifier.getKind () == Expression::eMarking) {
    class Valuation valuation;
    for (const class Marking* m =
         static_cast<class Marking&>(qualifier).first ();
       m; m = m->next ()) {
      if (m->getMultiplicity (valuation)) {
      for (unsigned tr = myNumTransitions; tr--; ) {
        if (class Expression* expr =
            m->getToken ()->disqualify (*myTransitions[tr])) {
          switch (kind) {
            unsigned n;
          case Weak:
          case Strong:
            n = myTransitions[tr]->addFairness (*expr, id, kind == Strong);
            if (n > myNumMaxFair) myNumMaxFair = n;
            break;
          case Enabled:
            myTransitions[tr]->addEnabledness (*expr, id);
            break;
          }
        }
      }
      }
      else if (!valuation.isOK ()) {
      qualifier.destroy ();
      return false;
      }
      switch (kind) {
      case Weak:
      id = ++myNumWeaklyFair; break;
      case Strong:
      id = ++myNumStronglyFair; break;
      case Enabled:
      id = ++myNumEnabled; break;
      }
    }
  }
  else {
    for (unsigned tr = myNumTransitions; tr--; ) {
      if (class Expression* expr = qualifier.disqualify (*myTransitions[tr])) {
      switch (kind) {
        unsigned n;
      case Weak:
      case Strong:
        n = myTransitions[tr]->addFairness (*expr, id, kind == Strong);
        if (n > myNumMaxFair) myNumMaxFair = n;
        break;
      case Enabled:
        myTransitions[tr]->addEnabledness (*expr, id);
        break;
      }
      }
    }
    switch (kind) {
    case Weak:
      ++myNumWeaklyFair; break;
    case Strong:
      ++myNumStronglyFair; break;
    case Enabled:
      ++myNumEnabled; break;
    }
  }
  qualifier.destroy ();
  return true;
}

bool
00327 Net::addConstraint (class Expression& qualifier,
                class Transition& transition,
                enum CKind kind)
{
  unsigned id = UINT_MAX;
  switch (kind) {
  case Weak:
    id = myNumWeaklyFair; break;
  case Strong:
    id = myNumStronglyFair; break;
  case Enabled:
    id = myNumEnabled; break;
  }
  assert (id != UINT_MAX);
  if (qualifier.getKind () == Expression::eMarking) {
    class Valuation valuation;
    for (const class Marking* m =
         static_cast<class Marking&>(qualifier).first ();
       m; m = m->next ()) {
      if (m->getMultiplicity (valuation)) {
      if (class Expression* expr =
          m->getToken ()->disqualify (transition)) {
        switch (kind) {
          unsigned n;
        case Weak:
        case Strong:
          n = transition.addFairness (*expr, id, kind == Strong);
          if (n > myNumMaxFair) myNumMaxFair = n;
          break;
        case Enabled:
          transition.addEnabledness (*expr, id);
          break;
        }
      }
      }
      else if (!valuation.isOK ()) {
      qualifier.destroy ();
      return false;
      }
      switch (kind) {
      case Weak:
      id = ++myNumWeaklyFair; break;
      case Strong:
      id = ++myNumStronglyFair; break;
      case Enabled:
      id = ++myNumEnabled; break;
      }
    }
    qualifier.destroy ();
  }
  else {
    switch (kind) {
      unsigned n;
    case Weak:
      ++myNumWeaklyFair;
      goto fair;
    case Strong:
      ++myNumStronglyFair;
    fair:
      n = transition.addFairness (qualifier, id, kind == Strong);
      if (n > myNumMaxFair) myNumMaxFair = n;
      break;
    case Enabled:
      transition.addEnabledness (qualifier, id);
      ++myNumEnabled;
      break;
    }
  }
  return true;
}

static bool
flagVisible (const class Expression& expr,
           void*)
{
  if (expr.getKind () == Expression::ePlaceContents)
    const_cast<class Place&>(static_cast<const class PlaceContents&>
                       (expr).getPlace ()).flagVisible ();
  return true;
}

void
00409 Net::addReject (class Expression& expr)
{
  assert (!expr.isTemporal ());
  assert (expr.getKind () == Expression::eUndefined ||
        expr.getType () && expr.getType ()->getKind () == Type::tBool);
  if (!expr.forVariables (&::flagVisible, 0))
    assert (false);
  if (myReject)
    myReject = BooleanBinop::construct (false, *myReject, expr);
  else
    myReject = &expr;
}

void
00423 Net::addDeadlock (class Expression& expr)
{
  assert (!expr.isTemporal ());
  assert (expr.getKind () == Expression::eUndefined ||
        expr.getType () && expr.getType ()->getKind () == Type::tBool);
  if (!expr.forVariables (&::flagVisible, 0))
    assert (false);
  if (myDeadlock)
    myDeadlock = BooleanBinop::construct (false, *myDeadlock, expr);
  else
    myDeadlock = &expr;
}

class Place&
00437 Net::addPlace (char* name,
             class Constraint* capacity,
             const class Type& type)
{
  assert (!myInitMarking);
  assert (name && myPlaceMap.find (name) == myPlaceMap.end ());

  class Place* place = new class Place (*this, myNumPlaces, name,
                              capacity, type);
  myPlaceMap[place->getName ()] = place;
  // copy the place also to the parent nets
  for (class Net* net = this; net; net = net->myParent) {
    if (!(net->myNumPlaces & (net->myNumPlaces + 1))) {
      class Place** p = new class Place*[(net->myNumPlaces + 1) << 1];
      memcpy (p, net->myPlaces, sizeof (*net->myPlaces) * net->myNumPlaces);
      delete[] net->myPlaces;
      net->myPlaces = p;
    }
    net->myPlaces[net->myNumPlaces++] = place;
  }

  return *place;
}

class Transition&
00462 Net::addTransition (char* name, bool callee)
{
  assert (!!name);
  assert (callee
        ? myCalleeMap.find (name) == myCalleeMap.end ()
        : myTransitionMap.find (name) == myTransitionMap.end ());
  assert (myNumTransitions == myNumAllTransitions);

  class Transition* transition =
    new class Transition (*this,
                    callee ? myNumCallees : myNumTransitions,
                    name);
  if (callee) {
    myCalleeMap.insert (TransitionMap::value_type
                  (transition->getName (), transition));
    if (!(myNumCallees & (myNumCallees + 1))) {
      class Transition** t =
      new class Transition*[(myNumCallees + 1) << 1];
      memcpy (t, myCallees, sizeof (*myCallees) * myNumCallees);
      delete[] myCallees;
      myCallees = t;
    }
    return *(myCallees[myNumCallees++] = transition);
  }
  else {
    myTransitionMap.insert (TransitionMap::value_type
                      (transition->getName (), transition));
    if (!(myNumAllTransitions & (myNumAllTransitions + 1))) {
      class Transition** t =
      new class Transition*[(myNumAllTransitions + 1) << 1];
      memcpy (t, myTransitions, sizeof (*myTransitions) * myNumAllTransitions);
      delete[] myTransitions;
      myTransitions = t;
    }
    myNumAllTransitions++;
    return *(myTransitions[myNumTransitions++] = transition);
  }
}

void
00502 Net::addType (class Type& t, char* name)
{
  assert (!myInitMarking);
  class Type* type = &t;

  if (name) {
    if (type->getName ()) {
      assert (strcmp (type->getName (), name));
      type = type->copy ();
    }
    type->setName (name);
    assert (myTypeMap.find (type->getName ()) == myTypeMap.end ());
    myTypeMap[type->getName ()] = type;
  }

  if (!hasType (*type))
    myTypeList.push_back (type);
}

bool
00522 Net::addProp (char* name, class Expression& prop)
{
  assert (name && !prop.isTemporal ());
  assert (prop.getType () && prop.getType ()->getKind () == Type::tBool);

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

  if (!(myNumProps & (myNumProps + 1))) {
    char** propNames = new char*[(myNumProps + 1) << 1];
    memcpy (propNames, myPropNames, myNumProps * sizeof *myPropNames);
    delete[] myPropNames;
    myPropNames = propNames;

    class Expression** props = new class Expression*[(myNumProps + 1) << 1];
    memcpy (props, myProps, myNumProps * sizeof *myProps);
    delete[] myProps;
    myProps = props;
  }

  myPropNames[myNumProps] = name;
  myProps[myNumProps++] = &prop;
  return true;
}

bool
00549 Net::checkProps (const class GlobalMarking& m,
             bool (*operation) (unsigned, const void*),
             const void* data) const
{
  if (myNumProps) {
    class Valuation valuation;
    valuation.setGlobalMarking (&m);
    bool hold;

    for (unsigned i = 0; i < myNumProps; i++) {
      if (class Value* value = myProps[i]->eval (valuation)) {
      assert (value->getKind () == Value::vLeaf);
      hold = bool (static_cast<class LeafValue&>(*value));
      delete value;
      if (hold && !(*operation) (i, data))
        return false;
      }
      else
      valuation.clearErrors ();
    }
  }

  return true;
}

bool
00575 Net::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*
00603 Net::getConstant (const char* name) const
{
  for (unsigned i = myNumConstants; i--; )
    if (!strcmp (name, myConstantNames[i]))
      return myConstants[i];
  return 0;
}

bool
00612 Net::addSyncTrans (const class Printer& printer)
{
  /** flag: did the operation succeed? */
  bool ok = true;

  unsigned i;
  if (myParent) {
    // copy the referred places from the parent nets
    for (i = myNumTransitions; i--; )
      addPlaces (*myTransitions[i]);
    for (i = myNumCallees; i--; )
      if (myCallees[i]->getNumChildren ())
      addPlaces (*myCallees[i]);
  }

  // recursively process the subnets
  for (i = myNumChildren; i--; )
    if (!myChildren[i]->addSyncTrans (printer))
      ok = false;

  // adjust myUnif->place numbers in the synchronisation transitions
  if (myParent)
    for (i = myNumTransitions; ok && i--; )
      if (myTransitions[i]->getNumParents () &&
        !myTransitions[i]->isUnifiable (Transition::uIgnore, printer))
      ok = false;

  // instantiate a transition for each synchronisation label

  /** buffer for instantiated transition names */
  class StringBuffer name;

  for (i = myNumCallees; i--; ) {
    /** the callee transition */
    const class Transition& t = *myCallees[i];
    if (!t.getNumChildren ())
      continue;

    // create an unique name
    name.create (0);
    name.append (':', 1), name.append (t.getName ());
    // ensure that the name is unique
    if (myTransitionMap.find (name.getString ()) !=
      myTransitionMap.end ()) {
      const unsigned namelen = name.getLength ();
      for (unsigned k = 0;; k++) {
      name.append (':', 1), name.append (k);
      if (myTransitionMap.find (name.getString ()) ==
          myTransitionMap.end ())
        break;
      name.chop (name.getLength () - namelen);
      }
    }

    /** the instantiated transition where all the children are fused */
    class Transition& trans = addTransition (name.copy (), false);
    for (unsigned p = t.getNumParents (); p--; )
      const_cast<class Transition&>(t.getParent (p)).addChild (trans);

    unsigned k;
    for (k = 0; k < t.getNumChildren (); k++) {
      const class Transition& u = t.getChild (k);
      if (u.getLocalIndex () < u.getNet ()->myNumCallees &&
        u.getNet ()->myCallees[u.getLocalIndex ()] == &u)
      continue; // do not fuse callee transitions in the child net

      // copy the arcs to the global synchronisation transition
      if (!trans.fuse (u, printer, true))
      ok = false;
      else {
      class Transition& child = const_cast<class Transition&>(u);
      trans.addChild (child);
      child.changeParent (t, trans);
      if (!child.isUnifiable (Transition::uRemove, printer))
        ok = false;
      }
    }

    // see that the fused synchronisation transition is unifiable
    if (ok && !trans.isUnifiable (t.getNumParents ()
                          ? Transition::uIgnore
                          : Transition::uNormal,
                          printer))
      ok = false;
  }

  return ok;
}

void
00702 Net::addLocalTransitions (class Net& root) const
{
  assert (myParent && !root.myParent);
  unsigned i;

  for (i = 0; i < myNumTransitions; i++) {
    if (!myTransitions[i]->getNumParents ()) {
      // add the transition to the root net
      if (!(root.myNumAllTransitions & (root.myNumAllTransitions + 1))) {
      class Transition** t =
        new class Transition*[(root.myNumAllTransitions + 1) << 1];
      memcpy (t, root.myTransitions,
            root.myNumAllTransitions * sizeof (*root.myTransitions));
      delete[] root.myTransitions;
      root.myTransitions = t;
      }
      myTransitions[i]->setRootIndex (root.myNumAllTransitions);
      root.myTransitions[root.myNumAllTransitions++] = myTransitions[i];
    }
  }

  for (i = 0; i < myNumChildren; i++)
    myChildren[i]->addLocalTransitions (root);
}

bool
00728 Net::prepareModular (const class Printer& printer)
{
  assert (!myParent);
  if (!addSyncTrans (printer))
    return false;
  for (unsigned i = 0; i < myNumChildren; i++)
    myChildren[i]->addLocalTransitions (*this);
  return true;
}

bool
00739 Net::computeInitMarking (const class Printer& printer)
{
  bool ok = true;
  assert (!myInitMarking);
  if (myInitMarking)
    return ok;
  myInitMarking = new class GlobalMarking (*this);
  class Valuation v;
  unsigned i;
  // non-implicit places
  for (i = 0; i < myNumPlaces; i++) {
    if (const class Marking* m =
      myPlaces[i] ? myPlaces[i]->getInitMarking () : 0) {
      if (!myPlaces[i]->isImplicit ()) {
      v.clearErrors ();
      if (!m->add ((*myInitMarking)[i], 1u, v)) {
        assert (!v.isOK ());
        printer.printRaw ("place ");
        printer.print (myPlaces[i]->getName ());
        printer.printRaw (": error in the initial marking expression:");
        printer.finish ();
        v.display (printer);
        printer.finish ();
        ok = false;
      }
      }
    }
  }
  // implicit places
  v.setGlobalMarking (myInitMarking);
  for (i = 0; i < myNumPlaces; i++) {
    if (const class Marking* m =
      myPlaces[i] ? myPlaces[i]->getInitMarking () : 0) {
      if (myPlaces[i]->isImplicit ()) {
      v.clearErrors ();
      if (!m->add ((*myInitMarking)[i], 1u, v)) {
        assert (!v.isOK ());
        printer.printRaw ("place ");
        printer.print (myPlaces[i]->getName ());
        printer.printRaw (": error in the initial marking expression:");
        printer.finish ();
        v.display (printer);
        printer.finish ();
        ok = false;
      }
      }
    }
  }
  if (isReject (*myInitMarking, true))
    ok = false;
  return ok;
}

const class BoolType&
00793 Net::getBoolType ()
{
  return boolType;
}

const class IntType&
00799 Net::getIntType ()
{
  return intType;
}

const class CardType&
00805 Net::getCardType ()
{
  return cardType;
}

const class CharType&
00811 Net::getCharType ()
{
  return charType;
}

enum Net::Status
00817 Net::isReject (const class GlobalMarking& m,
             bool flattened) const
{
  enum Status status = myReject ? ::isFatal (m, *myReject) : OK;
  if (flattened && status != Fatal) {
    for (unsigned i = myNumChildren; i--; ) {
      switch (myChildren[i]->isReject (m, true)) {
      case Fatal:
      return Fatal;
      case Error:
      status = Error;
      case OK:
      break;
      }
    }
  }
  return status;
}

enum Net::Status
00837 Net::isDeadlock (const class GlobalMarking& m,
             bool flattened) const
{
  enum Status status = myDeadlock ? ::isFatal (m, *myDeadlock) : OK;
  if (flattened && status != Fatal) {
    for (unsigned i = myNumChildren; i--; ) {
      switch (myChildren[i]->isDeadlock (m, true)) {
      case Fatal:
      return Fatal;
      case Error:
      status = Error;
      case OK:
      break;
      }
    }
  }
  return status;
}

bool
00857 Net::isPredefinedType (const class Type& type)
{
  return ::isPredefinedType (&type);
}

void
00863 Net::encode (class BitPacker& buf,
           const class Transition& transition,
           const class Valuation& valuation,
           bool flattened) const
{
  assert (flattened
        ? &getTransition (transition.getRootIndex ()) == &transition
        : &getTransition (transition.getLocalIndex ()) == &transition);
  assert (valuation.isOK ());
  if (flattened && myNumAllTransitions > 1)
    buf.append (transition.getRootIndex (), log2 (myNumAllTransitions));
  else if (myNumTransitions > 1) {
    assert (!flattened);
    buf.append (transition.getLocalIndex (), log2 (myNumTransitions));
  }
  else
    assert (flattened ? myNumAllTransitions == 1 : myNumTransitions == 1);

  for (Transition::const_iterator i = transition.begin ();
       i != transition.end (); i++) {
    const class Value* value = valuation.getValue (*i->second);
    if (i->second->isUndefined ())
      buf.append (!value, 1);
    else
      assert (!!value);
    if (value)
      buf.append (*value);
  }
}

void
00894 Net::decode (class BitUnpacker& buf,
           const class Transition*& transition,
           class Valuation& valuation,
           bool flattened) const
{
  const unsigned numTransitions =
    flattened ? myNumAllTransitions : myNumTransitions;
  transition = &getTransition
    (numTransitions > 1 ? buf.extract (log2 (numTransitions)) : 0);

  for (Transition::const_iterator i = transition->begin ();
       i != transition->end (); i++)
    if (!i->second->isUndefined () || !buf.extract (1))
      valuation.setValue (*i->second, *buf.extract (i->second->getType ()));
}

#ifdef EXPR_COMPILE
# include "Compilation.h"
# include "CExpression.h"

/** Start generating a block specific to a child net and all its parents
 * @param out           the output stream
 * @param indent  indentation level
 * @param child         the child net
 */
static void
compileNetStart (class StringBuffer& out,
             unsigned& indent,
             const class Net& child)
{
  out.indent (indent);
  out.append ("if (!net");
  for (const class Net* n = &child; n->getParent (); n = n->getParent ()) {
    out.append (" ||\n");
    out.indent (indent + 4);
    out.append ("net == "), out.append (n->getIndex ());
  }
  out.append (") {\n");
  indent += 2;
}

/** Finish generating a block specific to a child net and all its parents
 * @param out           the output stream
 * @param indent  indentation level
 */
static void
compileNetEnd (class StringBuffer& out,
             unsigned& indent)
{
  out.indent (indent -= 2);
  out.append ("}\n");
}

void
Net::compileEncoder (class CExpression& cexpr) const
{
  unsigned i;
  class StringBuffer& out = cexpr.getOut ();
  class StringBuffer itemname;
  unsigned indent = 2;

  cexpr.setFatalError ("FREE(p); return *fatal=1, errFatal;\n");
  if (myNumChildren)
    out.append ("  if (flattened) net = 0;\n");

  /** flag: are there any implicit places? */
  bool hasImplicit = false;
  for (i = myNumPlaces; i--; ) {
    if (!myPlaces[i]->isImplicit ())
      continue;
    if (!hasImplicit) {
      hasImplicit = true;
      out.append ("#ifndef NO_INVARIANT_CHECK\n"
              "# define NO_INVARIANT_CHECK(p) 0\n"
              "#endif\n");
      out.indent (indent), out.append ("struct tree* p = 0;\n");
    }
    out.append ("#if !NO_INVARIANT_CHECK(");
    out.append (i), out.append (")\n");
    out.append ("# define ERROR(err){FREE(p);return err;}\n");

    if (myNumChildren)
      ::compileNetStart (out, indent, myPlaces[i]->getNet ());

    if (myPlaces[i]->getMaxNumTokens () == 1) {
      out.indent (indent);
      out.append ("{\n");
      out.indent (indent += 2);
      myPlaces[i]->getType ().appendName (out);
      out.append ("* item;\n");
      myPlaces[i]->getInitMarking ()->compileScalarMset (cexpr, indent,
                                           "item", 0, false);
      itemname.append ("(*");
      itemname.append (cexpr.getMultiset ());
      itemname.append (".p");
      itemname.append (i);
      itemname.append (")");
      if (!myPlaces[i]->getCapacityBits ()) {
      out.indent (indent);
      out.append ("if (!item)\n");
      cexpr.compileError (indent + 2, errConst);
      }
      out.indent (indent);
      out.append ("if (");
      if (myPlaces[i]->getCapacityBits ()) {
      out.append ("item != ");
      out.append (cexpr.getMultiset ());
      out.append (".p");
      out.append (i);
      out.append (" &&\n");
      out.indent (indent + 4);
      }
      if (!myPlaces[i]->getType ().
        compileEqual (out, indent + 4, "(*item)", itemname.getString (),
                  false, true, true, false))
      out.append ("0");
      out.append (")\n");
      cexpr.compileError (indent + 2, errComp);
      out.indent (indent -= 2);
      out.append ("}\n");
    }
    else {
      itemname.append ("(");
      myPlaces[i]->getType ().appendMSetName (itemname);
      itemname.append ("*)");
      myPlaces[i]->getInitMarking ()->compileMset
      (cexpr, indent, itemname.getString (), "p", 0);
      out.indent (indent);
      out.append ("if (!equal");
      myPlaces[i]->getType ().appendIndex (out);
      out.append (" (");
      out.append (itemname);
      out.append ("p, ");
      out.append (cexpr.getMultiset ());
      out.append (".p");
      out.append (i);
      out.append ("))\n");
      cexpr.compileError (indent + 2, errComp);
    }
    cexpr.compileCleanup (indent);
    itemname.create (0);
    if (myChildren)
      ::compileNetEnd (out, indent);
    out.append ("# undef ERROR\n"
            "  FREE (p);\n"
            "#endif /* NO_INVARIANT_CHECK */\n");
  }

  cexpr.setFatalError ("return *fatal=1, errFatal;\n");
  out.indent (indent);
  out.append ("FCN (clear) ();\n");

  for (i = myNumPlaces; i--; ) {
    if (myPlaces[i]->isImplicit ())
      continue;
    if (myNumChildren)
      ::compileNetStart (out, indent, myPlaces[i]->getNet ());
    out.append ("#define ERROR(err)return err\n");

    if (myPlaces[i]->getMaxNumTokens () == 1) {
      out.indent (indent);
      out.append ("if (!");
      out.append (cexpr.getMultiset ());
      out.append (".p");
      out.append (i);
      out.append (")\n");
      if (myPlaces[i]->getCapacityBits ()) {
      out.indent (indent + 2);
      out.append ("FCN (enc) (0, 1);\n");
      out.indent (indent);
      out.append ("else {\n");
      out.indent (indent += 2);
      out.append ("FCN (enc) (1, 1);\n");
      }
      else
      cexpr.compileError (indent + 2, errConst);

      itemname.append ("(*");
      itemname.append (cexpr.getMultiset ());
      itemname.append (".p");
      itemname.append (i);
      itemname.append (")");
      myPlaces[i]->getType ().compileEncoder (cexpr, indent, "FCN (enc)",
                                    itemname.getString ());
      itemname.create (0);

      if (myPlaces[i]->getCapacityBits ()) {
      out.indent (indent -= 2);
      out.append ("}\n");
      }

      out.append ("#undef ERROR\n");
      if (myChildren)
      ::compileNetEnd (out, indent);
      continue;
    }

    const char* total = cexpr.getVarTmpCount ();
 
    out.indent (indent);
    out.append (total);
    out.append (" = msort (");
    out.append (cexpr.getMultiset ());
    out.append (".p");
    out.append (i);
    out.append (");\n");

    out.indent (indent);
    out.append ("if (");
    out.append (total);
    out.append (" == CARD_T_MAX)\n");
    cexpr.compileError (indent + 2, errCard);

    if (const class Constraint* c = myPlaces[i]->getCapacity ()) {
      c->compileCheck (cexpr, indent, total);
      if (unsigned cap = myPlaces[i]->getCapacityBits ()) {
      const char* number = cexpr.getVarCount ();
      if (cap > 2 && !myPlaces[i]->isNonempty ()) {
        out.indent (indent);
        out.append ("if ("), out.append (total), out.append (") {\n");
        out.indent (indent + 2);
        out.append ("FCN (enc) (1, 1);\n");
        CardType::compileConv (out, indent, *c, total, number);
        out.indent (indent + 2);
        out.append ("FCN (enc) ("), out.append (number), out.append (", ");
        out.append (cap), out.append (");\n");
        out.indent (indent);
        out.append ("}\n");
        out.indent (indent);
        out.append ("else FCN (enc) (0, 1);\n");
      }
      else {
        CardType::compileConv (out, indent, *c, total, number);
        out.indent (indent);
        out.append ("FCN (enc) (");
        out.append (number);
        out.append (", ");
        out.append (cap);
        out.append (");\n");
      }
      }
    }
    else {
      out.indent (indent);
      out.append ("encc ("), out.append (total), out.append (");\n");
    }

    out.indent (indent);
    out.append ("if ("), out.append (total), out.append (") {\n");
    out.indent (indent + 2);
    out.append ("if ("), out.append (total);
    out.append (" > 1) FCN (enc) (distinct - 1, log2 (");
    out.append (total), out.append ("));\n");
    out.indent (indent + 2), out.append ("while (distinct--) {\n");
    out.indent (indent + 4), out.append ("register card_t low = (");
    out.append (total), out.append (" + distinct) / (distinct + 1);\n");
    out.indent (indent + 4), out.append ("register card_t high = ");
    out.append (total), out.append (" - distinct;\n");
    out.indent (indent + 4), out.append (total);
    out.append (" -= histogram[distinct]->count;\n");
    out.indent (indent + 4), out.append ("if (high != low)\n");
    out.indent (indent + 6);
    out.append ("FCN (enc) (histogram[distinct]->count - low, "
            "log2 (high - low + 1));\n");

    itemname.append ("((");
    myPlaces[i]->getType ().appendMSetName (itemname);
    itemname.append ("*)histogram[distinct])->item");
    myPlaces[i]->getType ().compileEncoder (cexpr, indent + 4, "FCN (enc)",
                                  itemname.getString ());
    itemname.create (0);

    out.indent (indent + 2);
    out.append ("}\n");
    out.indent (indent);
    out.append ("}\n"
            "#undef ERROR\n");
    if (myChildren)
      ::compileNetEnd (out, indent);
  }

  out.append
    ("  if (propBits) {\n"
     "    const unsigned* p = propSucc + *propSucc;\n"
     "    const enum Error err = reject (net);\n"
     "    for (;;) {\n"
     "      FCN (enc) (*p, propBits);\n"
     "      FCN (deflate) ();\n"
     "      (*addstate) (ENCVAR (buf), NUM_BYTES (ENCVAR (bits)),\n"
     "                   err, tr, ftr, hide, ctx);\n"
     "      if (--p <= propSucc || *intr || *fatal) break;\n"
     "      FCN (inflate) (ENCVAR (buf), NUM_BYTES (ENCVAR (bits)));\n"
     "      FCN (del) (propBits);\n"
     "    }\n"
     "  }\n"
     "  else {\n"
     "    FCN (deflate) ();\n"
     "    (*addstate) (ENCVAR (buf), NUM_BYTES (ENCVAR (bits)),\n"
     "                 reject (net), tr, ftr, hide, ctx);\n"
     "  }\n"
     "  return errNone;\n");

  cexpr.setFatalError (0);
}

void
Net::compileDecoder (class CExpression& cexpr) const
{
  unsigned i;
  class StringBuffer& out = cexpr.getOut ();
  unsigned indent = 2;
  /** flag: are there any implicit places? */
  bool hasImplicit = false;
  class StringBuffer itemname;

  out.indent (indent);
  out.append ("FCN (inflate) ((word_t*) buf, size);\n");

  for (i = myNumPlaces; i--; ) {
    if (myPlaces[i]->isImplicit ()) {
      hasImplicit = true;
      continue;
    }
    if (myNumChildren)
      ::compileNetStart (out, indent, myPlaces[i]->getNet ());

    if (myPlaces[i]->getMaxNumTokens () == 1) {
      out.indent (indent);
      out.append ("free (");
      out.append (cexpr.getMultiset ()), out.append (".p"), out.append (i);
      out.append ("); ");
      out.append (cexpr.getMultiset ());
      out.append (".p"), out.append (i), out.append (" = 0;\n");
      out.indent (indent);
      if (myPlaces[i]->getCapacityBits ()) {
      out.append ("if ((numTokens["), out.append (i);
      out.append ("]=FCN (dec) (1))) {\n");
      out.indent (indent += 2);
      }
      else {
      out.append ("numTokens["), out.append (i), out.append ("]=1;\n");
      out.indent (indent);
      }
      out.append (cexpr.getMultiset ());
      out.append (".p");
      out.append (i);
      out.append (" = malloc (sizeof (");
      myPlaces[i]->getType ().appendName (out);
      out.append ("));\n");
      itemname.append ("(*");
      itemname.append (cexpr.getMultiset ());
      itemname.append (".p");
      itemname.append (i);
      itemname.append (")");
      myPlaces[i]->getType ().compileDecoder (cexpr, indent, "FCN (dec)",
                                    itemname.getString ());
      if (myPlaces[i]->getCapacityBits ()) {
      out.indent (indent -= 2);
      out.append ("}\n");
      }
      itemname.create (0);
      if (myChildren)
      ::compileNetEnd (out, indent);
      continue;
    }

    const char* total = cexpr.getVarTmpCount ();

    if (const class Constraint* c = myPlaces[i]->getCapacity ()) {
      if (unsigned cap = myPlaces[i]->getCapacityBits ()) {
      const char* number = cexpr.getVarCount ();
      if (cap > 2 && !myPlaces[i]->isNonempty ()) {
        out.indent (indent), out.append ("if (FCN (dec) (1)) {\n");
        out.indent (indent + 2);
        out.append (number);
        out.append (" = FCN (dec) ("), out.append (cap), out.append (");\n");
        CardType::compileReverseConv (out, indent + 2, *c, number, total);
        out.indent (indent), out.append ("}\n");
        out.indent (indent), out.append ("else\n");
        out.indent (indent + 2), out.append (total), out.append (" = 0;\n");
      }
      else {
        out.indent (indent);
        out.append (number);
        out.append (" = FCN (dec) ("), out.append (cap), out.append (");\n");
        CardType::compileReverseConv (out, indent, *c, number, total);
      }
      }
      else {
      out.indent (indent), out.append (total), out.append (" = ");
      out.append (CardType::convert (0, *c));
      out.append (";\n");
      }
    }
    else
      out.indent (indent), out.append (total), out.append (" = decc ();\n");

    out.indent (indent); out.append ("  FREE (");
    out.append (cexpr.getMultiset ());
    out.append (".p"), out.append (i), out.append (");\n");

    out.indent (indent);
    out.append ("if ((numTokens["), out.append (i);
    out.append ("]="), out.append (total), out.append (")) {\n");
    out.indent (indent + 2);
    out.append ("for (distinct = "), out.append (total);
    out.append (" > 1 ? FCN (dec) (log2 ("), out.append (total);
    out.append (")) + 1 : 1;\n");
    out.indent (indent + 7);
    out.append ("distinct--; ) {\n");
    out.indent (indent + 4);
    myPlaces[i]->getType ().appendName (out);
    out.append (" item;\n");
    out.indent (indent + 4), out.append ("register card_t low = (");
    out.append (total), out.append (" + distinct) / (distinct + 1);\n");
    out.indent (indent + 4), out.append ("register card_t high = ");
    out.append (total), out.append (" - distinct;\n");
    out.indent (indent + 4);
    out.append ("register card_t amount = low != high\n");
    out.indent (indent + 6);
    out.append ("? low + FCN (dec) (log2 (high - low + 1))\n");
    out.indent (indent + 6);
    out.append (": low;\n");
    out.indent (indent + 4), out.append (total), out.append (" -= amount;\n");
    myPlaces[i]->getType ().compileDecoder (cexpr, indent + 4,
                                  "FCN (dec)", "item");
    out.indent (indent + 4), out.append (cexpr.getMultiset ());
    out.append (".p"), out.append (i);
    out.append (" = insert"), myPlaces[i]->getType ().appendIndex (out);
    out.append (" ("), out.append (cexpr.getMultiset ());
    out.append (".p"), out.append (i);
    out.append (", &item, amount);\n");
    out.indent (indent + 2);
    out.append ("}\n");
    out.indent (indent);
    out.append ("}\n");
    if (myChildren)
      ::compileNetEnd (out, indent);
  }

  if (hasImplicit) {
    out.append ("#define ERROR(err) abort ()\n");
    for (i = 0; i < myNumPlaces; i++) {
      if (!myPlaces[i]->isImplicit ())
      continue;
      if (myNumChildren)
      ::compileNetStart (out, indent, myPlaces[i]->getNet ());
      itemname.append (cexpr.getMultiset ());
      itemname.append (".p"), itemname.append (i);
      if (myPlaces[i]->getMaxNumTokens () == 1) {
      myPlaces[i]->getInitMarking ()->
        compileScalarMset (cexpr, indent, itemname.getString (), 0, false);
      out.indent (indent);
      out.append ("if ((numTokens["), out.append (i), out.append ("]=!!");
      out.append (itemname);
      out.append ("))\n");
      out.indent (indent + 2);
      out.append (itemname);
      out.append (" = memcpy (malloc (sizeof *");
      out.append (itemname);
      out.append ("), ");
      out.append (itemname);
      out.append (", sizeof *");
      out.append (itemname);
      out.append (");\n");
      if (!myPlaces[i]->getCapacityBits ()) {
        out.indent (indent);
        out.append ("else\n");
        cexpr.compileError (indent + 2, errConst);
      }
      }
      else {
      myPlaces[i]->getInitMarking ()->
        compileMset (cexpr, indent, 0, itemname.getString (), 0);
      out.indent (indent), out.append ("{\n");
      out.indent (indent + 2), myPlaces[i]->getType ().appendMSetName (out);
      out.append ("* t = "), out.append (itemname), out.append (";\n");
      out.indent (indent + 2);
      out.append ("FIRST (t);\n");
      out.indent (indent + 2);
      out.append ("for (numTokens["), out.append (i), out.append ("]=0; ");
      out.append ("t; ) {\n");
      out.indent (indent + 4);
      out.append ("numTokens["), out.append (i), out.append ("] += ");
      out.append (itemname), out.append ("->count;\n");
      out.indent (indent + 4);
      out.append ("NEXT (t);\n");
      out.indent (indent + 2);
      out.append ("}\n");
      out.indent (indent);
      out.append ("}\n");
      }
      cexpr.compileCleanup (indent);
      itemname.create (0);
      if (myChildren)
      ::compileNetEnd (out, indent);
    }
    out.append ("#undef ERROR\n");
  }

  out.append ("  if (propBits) *propSucc = FCN (dec) (propBits);\n");
}

void
Net::compileProjection (class CExpression& cexpr) const
{
  unsigned i;
  class StringBuffer& out = cexpr.getOut ();
  class StringBuffer itemname;
  unsigned indent = 2;

  out.indent (indent);
  out.append ("FCN (clear) ();\n");

  for (i = myNumPlaces; i--; ) {
    if (myPlaces[i]->isImplicit ())
      continue;
    if (myNumChildren)
      ::compileNetStart (out, indent, myPlaces[i]->getNet ());

    if (myPlaces[i]->getMaxNumTokens () == 1) {
      if (myPlaces[i]->getCapacityBits ()) {
      out.indent (indent);
      out.append ("if (!");
      out.append (cexpr.getMultiset ());
      out.append (".p");
      out.append (i);
      out.append (")\n");
      out.indent (indent + 2);
      out.append ("FCN (enc) (0, 1);\n");
      out.indent (indent);
      out.append ("else {\n");
      out.indent (indent += 2);
      out.append ("FCN (enc) (1, 1);\n");
      }

      itemname.append ("(*");
      itemname.append (cexpr.getMultiset ());
      itemname.append (".p");
      itemname.append (i);
      itemname.append (")");
      myPlaces[i]->getType ().compileEncoder (cexpr, indent, "FCN (enc)",
                                    itemname.getString ());
      itemname.create (0);

      if (myPlaces[i]->getCapacityBits ()) {
      out.indent (indent -= 2);
      out.append ("}\n");
      }

      if (myChildren)
      ::compileNetEnd (out, indent);
      continue;
    }

    const char* total = cexpr.getVarTmpCount ();

    out.indent (indent);
    out.append (total);
    out.append (" = msort (");
    out.append (cexpr.getMultiset ());
    out.append (".p");
    out.append (i);
    out.append (");\n");

    if (const class Constraint* c = myPlaces[i]->getCapacity ()) {
      if (unsigned cap = myPlaces[i]->getCapacityBits ()) {
      const char* number = cexpr.getVarCount ();
      if (cap > 2 && !myPlaces[i]->isNonempty ()) {
        out.indent (indent);
        out.append ("if ("), out.append (total), out.append (") {\n");
        out.indent (indent + 2);
        out.append ("FCN (enc) (1, 1);\n");
        CardType::compileConv (out, indent, *c, total, number);
        out.indent (indent + 2);
        out.append ("FCN (enc) ("), out.append (number), out.append (", ");
        out.append (cap), out.append (");\n");
        out.indent (indent);
        out.append ("}\n");
        out.indent (indent);
        out.append ("else FCN (enc) (0, 1);\n");
      }
      else {
        CardType::compileConv (out, indent, *c, total, number);
        out.indent (indent);
        out.append ("FCN (enc) (");
        out.append (number);
        out.append (", ");
        out.append (cap);
        out.append (");\n");
      }
      }
    }
    else {
      out.indent (indent);
      out.append ("encc ("), out.append (total), out.append (");\n");
    }

    out.indent (indent);
    out.append ("if ("), out.append (total), out.append (") {\n");
    out.indent (indent + 2);
    out.append ("if ("), out.append (total);
    out.append (" > 1) FCN (enc) (distinct - 1, log2 (");
    out.append (total), out.append ("));\n");
    out.indent (indent + 2), out.append ("while (distinct--) {\n");
    out.indent (indent + 4), out.append ("register card_t low = (");
    out.append (total), out.append (" + distinct) / (distinct + 1);\n");
    out.indent (indent + 4), out.append ("register card_t high = ");
    out.append (total), out.append (" - distinct;\n");
    out.indent (indent + 4), out.append (total);
    out.append (" -= histogram[distinct]->count;\n");
    out.indent (indent + 4), out.append ("if (high != low)\n");
    out.indent (indent + 6);
    out.append ("FCN (enc) (histogram[distinct]->count - low, "
            "log2 (high - low + 1));\n");

    itemname.append ("((");
    myPlaces[i]->getType ().appendMSetName (itemname);
    itemname.append ("*)histogram[distinct])->item");
    myPlaces[i]->getType ().compileEncoder (cexpr, indent + 4, "FCN (enc)",
                                  itemname.getString ());
    itemname.create (0);

    out.indent (indent + 2);
    out.append ("}\n");
    out.indent (indent);
    out.append ("}\n");
    if (myChildren)
      ::compileNetEnd (out, indent);
  }

  out.append
    ("  FCN (enc) (d, dbits);\n"
     "  FCN (deflate) ();\n"
     "  *size = NUM_BYTES (ENCVAR (bits));\n"
     "  return ENCVAR (buf);\n");
}

/** Compile a Boolean expression
 * @param cexpr         the compilation
 * @param indent  indentation level
 * @param expr          the expression to be compiled
 */
inline static void
compileExpression (class CExpression& cexpr,
               unsigned indent,
               const class Expression& expr)
{
  class StringBuffer& out = cexpr.getOut ();
  out.append ("#define ERROR(err)return err\n");
  const char* result = cexpr.getFlag ();
  expr.compile (cexpr, indent, result, 0);
  cexpr.compileCleanup (indent);
  out.append ("#undef ERROR\n");
  out.indent (indent);
  out.append ("if (");
  out.append (result);
  out.append (") return errComp;\n");
}

void
Net::compileReject (class CExpression& cexpr) const
{
  class StringBuffer& out = cexpr.getOut ();
  unsigned indent = 2;
  if (myReject) {
    if (myParent || myNumChildren)
      ::compileNetStart (out, indent, *this);
    ::compileExpression (cexpr, indent, *myReject);
    if (myParent || myNumChildren)
      ::compileNetEnd (out, indent);
  }
  for (unsigned i = 0; i < myNumChildren; i++)
    myChildren[i]->compileReject (cexpr);
  if (!myParent)
    out.append ("  return errNone;\n");
}

void
Net::compileDeadlock (class CExpression& cexpr) const
{
  class StringBuffer& out = cexpr.getOut ();
  unsigned indent = 2;
  if (myDeadlock) {
    if (myParent || myNumChildren)
      ::compileNetStart (out, indent, *this);
    ::compileExpression (cexpr, indent, *myDeadlock);
    if (myParent || myNumChildren)
      ::compileNetEnd (out, indent);
  }
  for (unsigned i = 0; i < myNumChildren; i++)
    myChildren[i]->compileDeadlock (cexpr);
  if (!myParent)
    out.append ("  return errNone;\n");
}

void
Net::compileProps (class CExpression& cexpr,
               const char* operation,
               const char* data) const
{
  class StringBuffer& out = cexpr.getOut ();
  if (myNumProps) {
    out.append ("#define ERROR(err) continue\n");
    for (unsigned i = 0; i < myNumProps; i++) {
      out.append ("  do {\n");
      const char* result = cexpr.getFlag ();
      myProps[i]->compile (cexpr, 4, result, 0);
      out.append ("    if (");
      out.append (result);
      out.append (" && !");
      out.append (operation);
      out.append (" (");
      out.append (i);
      out.append (", ");
      out.append (data);
      out.append (")) return 0;\n");
      out.append ("  } while (0);\n");
    }
    cexpr.compileCleanup (2);
    out.append ("#undef ERROR\n");
  }
  out.append ("  return 1;\n");
}

void
Net::compileConstantDecl (class StringBuffer& out,
                    const char* ext) const
{
  class Printer printer;
  printer.setOutput (&out);
  for (unsigned i = 0; i < myNumConstants; i++) {
    if (ext)
      out.append (ext);
    else {
      out.append ("#if 0\n");
      printer.printQuoted (myConstantNames[i]);
      out.append ("\n"
              "#endif\n");
    }
    myConstants[i]->getType ()->appendName (out);
    out.append (" c");
    out.append (i);
    out.append (";\n");
  }
}

void
Net::compileConstantInit (class StringBuffer& out) const
{
  char name[22];
  for (unsigned i = 0; i < myNumConstants; i++) {
    snprintf (name, sizeof name, "c%u", i);
    myConstants[i]->getValue ().compileInit (name, 2, out);
  }
}

#endif // EXPR_COMPILE

void
01654 Net::display (const class Printer& printer) const
{
  if (myName) {
    printer.printRaw ("/* net ");
    printer.printQuoted (myName);
    printer.printRaw ("*/");
    printer.finish ();
  }
  for (TypeList::const_iterator t = myTypeList.begin ();
       t != myTypeList.end (); t++) {
    const class Type& type = **t;
    if (!type.getName ()) continue;
    printer.printRaw ("typedef ");
    type.display (printer);
    printer.delimiter (' ');
    printer.print (type.getName ());
    printer.delimiter (';');
    printer.finish ();
  }

  for (unsigned p = 0; p < myNumPlaces; p++)
    myPlaces[p]->display (printer);

  for (unsigned tr = 0; tr < myNumAllTransitions; tr++)
    myTransitions[tr]->display (printer);

  if (myReject) {
    printer.printRaw ("reject ");
    myReject->display (printer);
    printer.delimiter (';');
    printer.finish ();
  }
  if (myDeadlock) {
    printer.printRaw ("deadlock ");
    myDeadlock->display (printer);
    printer.delimiter (';');
    printer.finish ();
  }

  for (unsigned prop = 0; prop < myNumProps; prop++) {
    printer.printRaw ("prop ");
    printer.print (myPropNames[prop]);
    printer.delimiter (':')++;
    myProps[prop]->display (printer);
    printer--;
    printer.delimiter (';');
    printer.finish ();
  }
}

Generated by  Doxygen 1.6.0   Back to index