Logo Search packages:      
Sourcecode: maria version File versions

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

Unfold the transition by iterating the variable domains

Parameters:
lnet the low-level net being generated
reporter the reporting interface

Dummy empty marking for diagnostics

tokens removed from the input places

transition variable iterator

tokens added to the output places

Definition at line 1915 of file Transition.C.

References Marking::add(), VariableSet::begin(), slist< T >::begin(), checkGates(), Valuation::clearErrors(), cont, LNet::ltrans::data, LNet::ltrans::datalen, slist< T >::empty(), Net::encode(), VariableSet::end(), firstOutput(), BitPacker::getBuf(), Valuation::getError(), Arc::getExpr(), Type::getFirstValue(), Arc::getIndex(), Place::getIndex(), Value::getKind(), getKind(), Marking::getMultiplicity(), GlobalMarking::getNet(), LNet::getNet(), BitPacker::getNumWords(), Arc::getPlace(), GlobalMarking::getSize(), Net::getTransition(), VariableDefinition::getType(), Valuation::getValue(), Valuation::increment(), interrupted, VariableDefinition::isAggregate(), isFirst(), Valuation::isOK(), VariableDefinition::isReferenced(), VariableDefinition::isUndefined(), unif::m, myGates, myInputs, myKind, myNumInputs, myNumOutputs, myOutputs, myRootIndex, myUnif, myVariables, unif::next, nextOutput(), LNet::ltrans::out, Valuation::setGlobalMarking(), Valuation::setValue(), LNet::ltrans::t, Valuation::undefine(), 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, *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;
  }
}


Generated by  Doxygen 1.6.0   Back to index