Commit 6b873b1c authored by EXT Iulian Ober's avatar EXT Iulian Ober
Browse files

support for bounding the number of messages from env in DFS

parent 088b42c9
......@@ -446,8 +446,10 @@ define(`end_instance_impl', `')
define(`fire_external_signal',
`ifelse($1,,,` if (input(signal_name($1)) && !save(signal_name($1))) {
message_name($1) x;
iterate($1_par,x.m_par)
iterate($1_par,x.m_par) {
ITERATOR->trace(IfEvent::FEED, m_pid, x.string(), m_pid, x.store());
dispatch(&x,unstable);
}
}
fire_external_signal(shift($@))')')
......
......@@ -63,6 +63,7 @@ int opt_txml = 0;
int opt_limit_time = -1;
int opt_limit_states = -1;
int opt_limit_scn = -1;
int opt_limit_env = -1;
/*
*
......@@ -441,6 +442,7 @@ 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);
......@@ -455,15 +457,23 @@ void IfDfsExplorator::run(IfConfig* start) {
st = dfs.stack;
su = st->pending;
if (su != NULL) {
if (su != NULL) {
if (! (su->state->getMark() & REACHED)) {
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)
{
tt = new Stack;
tt->tail = st;
tt->pending = NULL;
tt->state = su->state;
tt->label = su->label->copy();
tt->state->setMark((q_count++) | REACHED | STACKED);
tt->cnt_env = st->cnt_env + from_env;
dfs.depth++;
dfs.stack = tt;
......@@ -501,6 +511,7 @@ try {
}
visit(tt->state);
}
}
visit(st->state, su->label, su->state);
......@@ -1179,6 +1190,7 @@ int main(int argc, char* argv[]) {
[-npf] : do not use dynamic priority functions \n\
[-ls integer] : exploration stops when number of states is above this limit (tested every 1s) \n\
[-lt integer] : exploration stops when time in seconds is reached \n\
[-le integer] : in DFS mode, exploration stops when number of signals from env is above this limit \n\
.observer options \n\
[-cs|-ce] : cut on observer success|error \n\
[-ms] [-me] : mark transitions entering success/error states \n\
......@@ -1312,6 +1324,11 @@ int main(int argc, char* argv[]) {
fprintf(stderr, "option %s not followed by an integer\n", argv[i]);
return 1;
}
} else if (!strcmp(argv[i], "-le")) {
if(i+1 >= argc || 0==sscanf(argv[i+1],"%d",&opt_limit_env)) {
fprintf(stderr, "option %s not followed by an integer\n", argv[i]);
return 1;
}
} else if (!strcmp(argv[i], "-ld")) {
if(i+1 >= argc || 0==sscanf(argv[i+1],"%d",&opt_limit_scn)) {
fprintf(stderr, "option %s not followed by an integer\n", argv[i]);
......
......@@ -185,6 +185,7 @@ class IfDfsExplorator : public IfExplorator {
IfLabel* label;
Successor* pending;
Stack* tail;
int cnt_env;
};
protected:
......
......@@ -70,7 +70,8 @@ const char* IfEvent::SYMBOL[] = {
"V",
"i",
"d",
"x-"
"x-",
"f"
};
const char* IfEvent::NAME[] = {
......@@ -94,6 +95,7 @@ const char* IfEvent::NAME[] = {
"DELTA",
"DEBUG",
"DISCARD",
"FEED",
};
IfEvent::IfEvent(const unsigned data,
......
......@@ -85,6 +85,7 @@ class IfEvent : public IfObject {
DELTA = 17,
DEBUG = 18,
DISCARD = 19,
FEED = 20,
};
enum Flag {
OWN = 0x00010000
......@@ -134,6 +135,7 @@ class IfEvent : public IfObject {
getKind() == SET ||
getKind() == RESET ||
getKind() == INPUT ||
getKind() == FEED ||
getKind() == RELEASE ||
getKind() == CALL ||
(getKind() == IMPORT && (ind_flags & (1 << getKind()))) ||
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment