Logo Search packages:      
Sourcecode: maria version File versions

void Transition::unfold ( class GlobalMarking cover,
class LNet lnet,
class DummyReporter reporter 
) const

Unfold the transition with the help of a coverable marking

Parameters:
cover (input/output) the coverable marking
lnet the low-level net being generated
reporter the reporting interface

the input marking

processed tokens

tokens removed from the input places

tokens added to the output places

Definition at line 1705 of file Transition.C.

References Marking::add(), TokenList::begin(), slist< T >::begin(), checkGates(), LNet::ltrans::data, LNet::ltrans::datalen, TokenList::empty(), PlaceMarking::empty(), slist< T >::empty(), Net::encode(), TokenList::end(), firstOutput(), BitPacker::getBuf(), Arc::getExpr(), Arc::getIndex(), Place::getIndex(), Value::getKind(), getKind(), Expression::getLvalues(), Marking::getMultiplicity(), GlobalMarking::getNet(), LNet::getNet(), BitPacker::getNumWords(), Arc::getPlace(), GlobalMarking::getSize(), Marking::getToken(), Net::getTransition(), interrupted, TokenList::isCompatible(), StateReporter::isFatal(), StateReporter::isFlattened(), Valuation::isOK(), unif::isSet, unif::m, myGates, myKind, myNumOutputs, myOutputs, myRootIndex, myUnif, unif::next, nextOutput(), LNet::ltrans::out, unif::place, TokenList::pop(), TokenList::push(), LNet::removeTransitions(), Valuation::setGlobalMarking(), Token::setReservedUnfold(), LNet::ltrans::t, unif::varMult, unif::vars, and willDo().

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


Generated by  Doxygen 1.6.0   Back to index