Logo Search packages:      
Sourcecode: maria version File versions

void GraphReporter::analyzeModular ( enum SearchKind  kind  )  [virtual]

Search the state space in a modular way

Parameters:
kind Type of search

Reimplemented from StateReporter.

Definition at line 355 of file GraphReporter.C.

References Graph::add(), addEvents(), Transition::analyze(), StateReporter::analyze(), analyzeModular(), StateReporter::Breadth, BitVector::clear(), BitPacker::deflate(), GlobalMarking::encode(), BitVector::extend(), BitPacker::getBuf(), Net::getChild(), BitPacker::getNumBytes(), Net::getNumChildren(), Transition::getNumChildren(), StateReporter::getNumErrors(), Net::getNumTransitions(), BitPacker::getNumWords(), Transition::getPriority(), Net::getTransition(), BitPacker::inflate(), init(), interrupted, Net::isDeadlock(), StateReporter::isFlattened(), Graph::isProcessed(), myChildren, StateReporter::myFatal, myGraph, StateReporter::myPriority, myProcessed, StateReporter::mySrcDeadlock, StateReporter::myStateBuf, myStateNum, myVisited, Graph::AddStatus::number, pop(), reportError(), StateReporter::Single, and StateReporter::suppress().

Referenced by analyzeModular().

{
  assert (!isFlattened ());
  const unsigned numTr = net.getNumTransitions ();
  extern bool interrupted;
#ifdef EXPR_COMPILE
  if (myCompilation) {
    while (!interrupted && !myFatal) {
      if (!popCompiled (kind == Breadth))
      break;
      myProcessed = myGraph.isProcessed (myStateNum);
      mySrcDeadlock = true, myPriority = 0;
      unsigned i;
      for (i = 0; !interrupted && !myFatal && i < numTr; i++) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
          !t.getNumChildren ())
        analyze (t);
      // synchronisation transitions (which have children) are analysed
      // by SyncStates::sync (), called below
      }

      if (myChildren) {
      i = net.getNumChildren ();
      word_t** srcs = new word_t*[i];
      // analyze child state spaces
      for (; !interrupted && !myFatal && i--; ) {
        const class Net& child = net.getChild (i);
        unsigned bytes;
        const void* buf =
          myCompilation->stateProject (child.getIndex (), 0, 0, bytes);
        unsigned numWords = bytes ? (bytes - 1) / sizeof (word_t) + 1 : 0;
        /* back up the source state */
        srcs[i] = bytes ? new word_t[numWords] : 0;
        memcpy (srcs[i], buf, numWords * sizeof (word_t));
        BitPacker::inflate (srcs[i][numWords - 1],
                        (-bytes) % sizeof (word_t));
#ifdef SYNC_CACHE
        if ((*myChildren)->mySync->lookup (i, srcs[i], numWords))
          continue; // the modular state has already been analyzed
#endif // SYNC_CACHE
        class GraphReporter& reporter = *myChildren[i];
        class Graph::AddStatus src = reporter.myGraph.add (buf, bytes);
        reporter.init (src.number);
        reporter.myVisited->clear ();
        reporter.myVisited->extend (src.number, true);

        unsigned numErrors = reporter.getNumErrors ();
        reporter.analyzeModular (Breadth);
        /* restore the source state */
        myCompilation->stateDecode (child.getIndex (), srcs[i], 0);
        if (reporter.myFatal)
          myFatal = true;
        if (reporter.getNumErrors () > numErrors)
          reportError (false);
      }

      // find out enabled synchronisation transitions and synchronise
      for (i = net.getNumTransitions (); i--; ) {
        const class Transition& t = net.getTransition (i);
        if ((!myPriority || t.getPriority () == myPriority) &&
            t.getNumChildren ())
          (*myChildren)->mySync->sync (t, *this, srcs);
      }

      for (i = net.getNumChildren (); i--; )
        delete[] srcs[i];
      delete[] srcs;

#ifndef SYNC_CACHE
      (*myChildren)->mySync->cleanup ();
#endif // !SYNC_CACHE
      }

      if (mySrcDeadlock && !interrupted && !myFatal) {
      switch (myCompilation->stateDeadlock (net.getIndex ())) {
      case errNone:
        break;
      default:
        myFatal = true;
        // fall through
      case errComp:
        reportError (true);
      }
      }

      if (suppress ())
      continue;
      addEvents ();
      if (kind >= Single)
      break;
    }
    return;
  }
  else
#endif // EXPR_COMPILE
  while (!interrupted && !myFatal) {
    class GlobalMarking* m = pop (kind == Breadth);
    if (!m)
      break;
    myProcessed = myGraph.isProcessed (myStateNum);
    mySrcDeadlock = true, myPriority = 0;
    unsigned i;
    for (i = 0; !interrupted && !myFatal && i < numTr; i++) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
        !t.getNumChildren ())
      t.analyze (*m, *this);
      // synchronisation transitions (which have children) are analysed
      // by SyncStates::sync (), called below
    }

    if (myChildren) {
      // analyze child state spaces
      for (i = net.getNumChildren (); !interrupted && !myFatal && i--; ) {
      const class Net& child = net.getChild (i);
      m->encode (myStateBuf, child);
#ifdef SYNC_CACHE
      if ((*myChildren)->mySync->lookup (i, myStateBuf.getBuf (),
                                 myStateBuf.getNumWords ()))
        continue; // the modular state has already been analyzed
#endif // SYNC_CACHE
      myStateBuf.deflate ();
      class GraphReporter& reporter = *myChildren[i];
      class Graph::AddStatus src =
        reporter.myGraph.add (myStateBuf.getBuf (),
                        myStateBuf.getNumBytes ());
      reporter.init (src.number);
      reporter.myVisited->clear ();
      reporter.myVisited->extend (src.number, true);

      unsigned numErrors = reporter.getNumErrors ();
      reporter.analyzeModular (Breadth);
      if (reporter.myFatal)
        myFatal = true;
      if (reporter.getNumErrors () > numErrors)
        reportError (false);
      }

      // find out enabled synchronisation transitions and synchronise
      for (i = net.getNumTransitions (); i--; ) {
      const class Transition& t = net.getTransition (i);
      if ((!myPriority || t.getPriority () == myPriority) &&
          t.getNumChildren ())
        (*myChildren)->mySync->sync (*m, t, *this);
      }

#ifndef SYNC_CACHE
      (*myChildren)->mySync->cleanup ();
#endif // !SYNC_CACHE
    }

    if (mySrcDeadlock && !interrupted && !myFatal) {
      switch (net.isDeadlock (*m, false)) {
      case Net::OK:
      break;
      case Net::Fatal:
      myFatal = true;
      // fall through
      case Net::Error:
      reportError (true);
      }
    }

    delete m;
    if (suppress ())
      continue;
    addEvents ();
    if (kind >= Single)
      break;
  }
}


Generated by  Doxygen 1.6.0   Back to index