refactor dfs loop

src/simulator-t/explorator.C

@@ -442,9 +442,9 @@ void IfDfsExplorator::run(IfConfig* start) {
   tt->tail = NULL;
   tt->pending = NULL;
   tt->label = NULL;
-  tt->cnt_env = 0;
   tt->state = start ? start : m_engine->start();
   tt->state->setMark((q_count++) | REACHED | STACKED);
+  tt->feeds = 0;
 
   dfs.depth++;
   dfs.stack = tt;
@@ -457,15 +457,8 @@ void IfDfsExplorator::run(IfConfig* start) {
     st = dfs.stack;
     su = st->pending;
 
-    if (su != NULL) {      
-      int from_env = 0;
-      if(opt_limit_env >= 0) 
-          for(int ec = su->label->getLength()-1; ec>=0;ec--)
-              if(su->label->getAt(ec)->getKind() == IfEvent::FEED) {
-                  from_env++;
-              }
-if(opt_limit_env == -1 || st->cnt_env + from_env <= opt_limit_env)
-{
+    if (su != NULL) {
+
       if (! (su->state->getMark() & REACHED)) {
         tt = new Stack;
         tt->tail = st;
@@ -473,53 +466,36 @@ if(opt_limit_env == -1 || st->cnt_env + from_env <= opt_limit_env)
         tt->state = su->state;
         tt->label = su->label->copy();
         tt->state->setMark((q_count++) | REACHED | STACKED);
-        tt->cnt_env = st->cnt_env + from_env;
+        tt->feeds = st->feeds + su->label->count(IfEvent::FEED);
         
         dfs.depth++;
         dfs.stack = tt;
-try {
-        m_engine->run(tt->state);
-} catch(IfDynamicError d) {
-        // catch Instance Addressing Faults 
-        std::ofstream file("dump.scn");
-        file << "<scenario>";
-        printStackScn(file);
-        file << "</scenario>";
-        file.close();     
-        exit(1);
-}
+        
+        try {
+          m_engine->run(tt->state);
+        } catch(IfDynamicError d) { // instance addressing fault
+          printScn("dump.scn");
+          exit(1);
+        }
+        
         if (m_flags & PO) restrict();
-
-        if (m_flags & FB) {
-          int bCnt = 0;
-          for(Successor* fbs = dfs.stack->pending; fbs != NULL; fbs = fbs->next) bCnt++;
-          if(bCnt >= FIND_BRANCH_MIN) {
-                cout << "-- More than " << FIND_BRANCH_MIN << " dependent branches found in state. Scenario saved in fb.scn.\n";
-                cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n";
-                for(Successor* fbs = dfs.stack->pending; fbs != NULL; fbs = fbs->next) {
-                        cout << "-----------------------\n";
-                        fbs->label->printXML(cout);
-                }
-                cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n";
-                std::ofstream file("fb.scn");
-                file << "<scenario>";
-                printStackScn(file);
-                file << "</scenario>";
-                file.close(); 
-                m_flags &= ~FB;
-          }
+        
+        if (m_flags & FB && length(dfs.stack->pending) >= FIND_BRANCH_MIN) {
+          dumpBranches();
+          m_flags &= ~FB;
         }
-
+        
+        if (opt_limit_env != -1) restrictFeeds();
+        
         visit(tt->state);
       }
       
       visit(st->state, su->label, su->state);
-} 
+      t_count++;
+      
       st->pending = su->next;
       delete su->label;
       delete su;
-
-      t_count++;
     }
     
     else {
@@ -587,6 +563,26 @@ void IfDfsExplorator::restrict() {
   }
 }
 
+void IfDfsExplorator::restrictFeeds() {
+  if (opt_limit_env < 0)
+    return;
+
+  // remove successors exceeding the number of allowed feeds ...
+  Successor* su = dfs.stack->pending, *st;
+  dfs.stack->pending = NULL;
+  for(; su != NULL; su = st) {
+    st = su->next;
+    if (dfs.stack->feeds + su->label->count(IfEvent::FEED) <= opt_limit_env) {
+      su->next = dfs.stack->pending;
+      dfs.stack->pending = su;
+    }
+    else {
+      delete su->label;
+      delete su;
+    }
+  }
+}
+
 void IfDfsExplorator::status() const {
   IfExplorator::status();
 #ifndef win32native
@@ -604,32 +600,50 @@ void IfDfsExplorator::visit(const IfConfig* source) {
 
   IfExplorator::visit(source);
 
-  if(opt_limit_scn > 0 && (errorScnCnt+successScnCnt)>=opt_limit_scn) 
+  if (opt_limit_scn > 0 && (errorScnCnt+successScnCnt)>=opt_limit_scn) 
     return;
 
   if (((m_flags & MS) && source->isObsSuccess()) ||
-       ((m_flags & ME) && source->isObsError())) {
+      ((m_flags & ME) && source->isObsError())) {
     char fileName[64];
-
-    if ( source->isObsSuccess() ) sprintf(fileName, "s%d.scn", ++successScnCnt);
-    if ( source->isObsError() ) sprintf(fileName, "e%d.scn", ++errorScnCnt);
-
-    std::ofstream file(fileName);
-    file << "<scenario>";
-    printStackScn(file);
-    file << "</scenario>";
-    file.close();
+    if (source->isObsSuccess()) sprintf(fileName, "s%d.scn", ++successScnCnt);
+    if (source->isObsError()) sprintf(fileName, "e%d.scn", ++errorScnCnt);
+    printScn(fileName);
   }
 }
 
-void IfDfsExplorator::printStackScn(std::ostream &out, Stack* left) {
-  if(left == NULL) left = dfs.stack;
-  if(left == NULL) return;
-  if(left->tail && left->tail->label)
-    printStackScn(out, left->tail);
-  if(left->label) {
+void IfDfsExplorator::printScn(const char* filename) const {
+  std::ofstream file(filename);
+  file << "<scenario>";
+  printStackRec(file, dfs.stack);
+  file << "</scenario>";
+  file.close();
+}
+
+void IfDfsExplorator::printStackRec(std::ostream &out, const Stack* left) const {
+  if (left == NULL) return;
+  if (left->tail && left->tail->label)
+    printStackRec(out, left->tail);
+  if (left->label)
     left->label->printXML(out);
+}
+
+void IfDfsExplorator::dumpBranches() const {
+  cout << "-- More than " << FIND_BRANCH_MIN << " dependent branches found in state. Scenario saved in fb.scn.\n";
+  cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n";
+  for(Successor* fbs = dfs.stack->pending; fbs != NULL; fbs = fbs->next) {
+    cout << "-----------------------\n";
+    fbs->label->printXML(cout);
   }
+  cout << "XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX\n";
+  printScn("fb.scn");
+}
+
+unsigned IfDfsExplorator::length(const Successor* list) const {
+  unsigned count = 0;
+  for(Successor* su = (Successor*) list; su != NULL; su = su->next)
+    count++;
+  return count;
 }
 
 /*

src/simulator-t/explorator.h

@@ -168,6 +168,7 @@ class IfDfsExplorator : public IfExplorator {
 
   unsigned m_ind_flags;
   void restrict(); // partial order reduction
+  void restrictFeeds(); // feeds limit reduction
   
   virtual void visit(const IfConfig* source);
   virtual void visit(const IfConfig* source, const IfLabel* label, const IfConfig* target) // C++ bug
@@ -181,11 +182,11 @@ class IfDfsExplorator : public IfExplorator {
   };
   
   struct Stack {
+    unsigned feeds;
     IfConfig* state;
     IfLabel* label;
     Successor* pending;
     Stack* tail;
-    int cnt_env;
   };
 
  protected:
@@ -195,7 +196,10 @@ class IfDfsExplorator : public IfExplorator {
   } dfs;
 
  private:
-  virtual void printStackScn(std::ostream& file, Stack* left = NULL);
+  void printScn(const char*) const;
+  void printStackRec(std::ostream&, const Stack*) const;
+  void dumpBranches() const;
+  unsigned length(const Successor*) const;
 
 };
 

src/simulator/label.C

@@ -298,6 +298,14 @@ void IfLabel::strip(int (*Visible)(const IfEvent*)) {
   setAt(k++, NULL);
 }
 
+unsigned IfLabel::count(const IfEvent::Kind kind) const {
+  int k = 0;
+  for(int i = 0; getAt(i); i++)
+    if (getAt(i)->getKind() == kind)
+      k++;
+  return k;
+}
+
 int IfLabel::compare(const IfLabel* label) const {
   return m_events.compare(&label->m_events);
 }

src/simulator/label.h

@@ -216,6 +216,7 @@ class IfLabel : public IfObject {
 
  public:
   void strip(int (*Visible)(const IfEvent*));
+  unsigned count(const IfEvent::Kind) const;
 
  public:
   DECLARE_STORABLE(IfLabel);