Logo Search packages:      
Sourcecode: maria version File versions

bool Transition::fuse ( const class Transition callee,
const class Printer printer,
bool  warn 
)

Fuse a callee transition to this one

Parameters:
callee the transition to be fused
printer the printer object for diagnostics
warn flag: issue warnings
Returns:
true if the operation was successful

the return status

variable substitutions

Definition at line 800 of file Transition.C.

References addArc(), addChild(), addConstant(), Net::addConstraint(), addGate(), addOutputVariable(), slist< T >::begin(), QuantifierList::begin(), Expression::copy(), copy(), Expression::cse(), Printer::delimiter(), Expression::destroy(), e, slist< T >::end(), QuantifierList::end(), Printer::finish(), getArc(), Function::getArity(), getConstant(), Arc::getExpr(), Function::getExpr(), getFunction(), Function::getName(), VariableDefinition::getName(), Net::getParent(), Arc::getPlace(), Expression::getType(), VariableDefinition::getType(), getVariable(), VariableDefinition::isAggregate(), Arc::isCopy(), myChildren, myConstantNames, myConstants, myEnabledCond, myFunctions, myGates, myInputs, myKind, myName, myNet, myNumChildren, myNumConstants, myNumEnabled, myNumInputs, myNumOutputs, myNumStronglyFair, myNumWeaklyFair, myOutputMarking, myOutputs, myOutputVariables, myPriority, myStronglyFairCond, myVariables, myWeaklyFairCond, newString(), Printer::printQuoted(), Printer::printRaw(), Substitution::setExpr(), Arc::substitute(), and Expression::substitute().

Referenced by Net::addSyncTrans().

{
  /** 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;
}


Generated by  Doxygen 1.6.0   Back to index