Logo Search packages:      
Sourcecode: maria version File versions

bool Transition::isUnifiable ( enum Unif  action,
const class Printer printer 
)

Determine whether the transition can be unified

Parameters:
action additional actions to take
printer the printer object for diagnostics
Returns:
true if the transition can be unified

number of split input arcs

best primary cost found so far

primary cost of the combination being considered

best secondary cost found so far

secondary cost of the combination being considered

the split input arcs

split arcs whose multiplicity depends on variables

best combination found so far

combination being considered

number of variable-multiplicity unifiers in the best combination

number of variable-multiplicity unifiers in current combination

variable sets unified from each arc in the best solution

variable sets unified from each arc in current combination

all variables that could be unified

all variables that can definitely be unified

total secondary costs

flag: is everything ok?

Definition at line 1137 of file Transition.C.

References arcs, BitVector::assign(), slist< T >::begin(), CARD_T_MAX, VariableSet::clear(), VariableSet::contains(), VariableSet::empty(), slist< T >::end(), VariableSet::end(), slist< T >::erase(), findVariable(), Printer::finish(), VariableDefinition::flagUndefined(), Place::getIndex(), Expression::getLvalues(), Place::getMaxNumTokens(), VariableDefinition::getName(), Type::getNumValues(), Marking::getParent(), Marking::getPlace(), Marking::getToken(), Expression::getType(), heapify(), VariableSet::insert(), VariableDefinition::isAggregate(), isInput(), Expression::isSet(), unif::isSet, unif::m, myGates, myInputs, myKind, myNumInputs, myUnif, Marking::next(), unif::next, unif::place, Printer::print(), Printer::printRaw(), VariableSet::size(), unif::varMult, and unif::vars.

Referenced by Net::addSyncTrans().

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


Generated by  Doxygen 1.6.0   Back to index