From dd3f21e9242981e0bbfc95f4f8fc2aa8f90f3d9a Mon Sep 17 00:00:00 2001
From: Marius Bozga <Marius.Bozga@univ-grenoble-alpes.fr>
Date: Mon, 31 Jan 2022 09:46:06 +0100
Subject: [PATCH] refactor dfs loop
---
src/simulator-t/explorator.C | 138 +++++++++++++++++++----------------
src/simulator-t/explorator.h | 8 +-
src/simulator/label.C | 8 ++
src/simulator/label.h | 1 +
4 files changed, 91 insertions(+), 64 deletions(-)
diff --git a/src/simulator-t/explorator.C b/src/simulator-t/explorator.C
index 378e9b4..78d7329 100644
--- a/src/simulator-t/explorator.C
+++ b/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;
}
/*
diff --git a/src/simulator-t/explorator.h b/src/simulator-t/explorator.h
index 0eadd2e..5ddeb3f 100644
--- a/src/simulator-t/explorator.h
+++ b/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;
};
diff --git a/src/simulator/label.C b/src/simulator/label.C
index 42cc3a2..8402039 100644
--- a/src/simulator/label.C
+++ b/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);
}
diff --git a/src/simulator/label.h b/src/simulator/label.h
index bdb2727..c0c2730 100644
--- a/src/simulator/label.h
+++ b/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);
--
GitLab