andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Some cleanup.

Browse Source 
- Added iteration limit, just enough to show the error.
This commit is contained in:
ccremers 2004-08-13 13:25:25 +00:00
parent eb55dbe35d
commit ff224fee8a
3 changed files with 44 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
src/arachne.c
View File

@ -187,7 +187,6 @@ create_intruder_goal (Term t)
run = sys->maxruns - 1; run = sys->maxruns - 1;
rd = sys->runs[run].start; rd = sys->runs[run].start;
sys->runs[run].length = 1; sys->runs[run].length = 1;
termDelete (rd->message);
rd->message = termDuplicate (t); rd->message = termDuplicate (t);
#ifdef DEBUG #ifdef DEBUG
explanation = "Adding intruder goal for message "; explanation = "Adding intruder goal for message ";
@ -261,10 +260,14 @@ bind_new_run (const Goal goal, const Protocol p, const Role r,
int run; int run;
int flag; int flag;
Roledef rd; Roledef rd;
int old_run;
int old_index;
roleInstance (sys, p, r, NULL); roleInstance (sys, p, r, NULL);
run = sys->maxruns - 1; run = sys->maxruns - 1;
sys->runs[run].length = index + 1; sys->runs[run].length = index + 1;
old_run = goal.rd->bind_run;
old_index = goal.rd->bind_index;
goal.rd->bind_run = run; goal.rd->bind_run = run;
goal.rd->bind_index = index; goal.rd->bind_index = index;
#ifdef DEBUG #ifdef DEBUG
@ -277,7 +280,8 @@ bind_new_run (const Goal goal, const Protocol p, const Role r,
iterate (); iterate ();
goal.rd->bind_run = INVALID; goal.rd->bind_run = old_run;
goal.rd->bind_index = old_index;
roleInstanceDestroy (sys); roleInstanceDestroy (sys);
return flag; return flag;
} }
@ -499,6 +503,15 @@ bind_goal (const Goal goal)
int int
prune () prune ()
{ {
if (indentDepth > 2)
{
// Hardcoded limit on iterations
#ifdef DEBUG
indentPrint ();
eprintf ("Pruned because too many iteration levels.\n");
#endif
return 1;
}
if (sys->maxruns > 5) if (sys->maxruns > 5)
{ {
// Hardcoded limit on runs // Hardcoded limit on runs

29
src/mgu.c
View File

@ -173,20 +173,23 @@ termMguInTerm (Term t1, Term t2, int (*iterator) ())
flag = 1; flag = 1;
t2 = deVar (t2); t2 = deVar (t2);
if (t2 != NULL && isTermTuple (t2)) if (t2 != NULL)
{ {
// t2 is a tuple, consider interm options as well. if (isTermTuple (t2))
flag = flag && termMguInTerm (t1, t2->left.op1, iterator); {
flag = flag && termMguInTerm (t1, t2->right.op2, iterator); // t2 is a tuple, consider interm options as well.
} flag = flag && termMguInTerm (t1, t2->left.op1, iterator);
// simple clause or combined flag = flag && termMguInTerm (t1, t2->right.op2, iterator);
tl = termMguTerm (t1, t2); }
if (tl != MGUFAIL) // simple clause or combined
{ tl = termMguTerm (t1, t2);
// Iterate if (tl != MGUFAIL)
flag = flag && iterator (tl); {
// Reset variables // Iterate
termlistSubstReset (tl); flag = flag && iterator (tl);
// Reset variables
termlistSubstReset (tl);
}
} }
return flag; return flag;
} }

16
src/system.c
View File

@ -269,9 +269,19 @@ ensureValidRun (const System sys, int run)
myrun.step = 0; myrun.step = 0;
myrun.index = NULL; myrun.index = NULL;
myrun.start = NULL; myrun.start = NULL;
myrun.know = knowledgeDuplicate (sys->know); if (sys->engine == POR_ENGINE)
myrun.prevSymmRun = -1; {
myrun.firstNonAgentRead = -1; myrun.know = knowledgeDuplicate (sys->know);
myrun.prevSymmRun = -1;
myrun.firstNonAgentRead = -1;
}
else
{
// Arachne etc.
myrun.know = NULL;
myrun.prevSymmRun = -1;
myrun.firstNonAgentRead = -1;
}
} }
} }