diff --git a/src/arachne.c b/src/arachne.c index 36ebf6b..824080d 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -187,7 +187,6 @@ create_intruder_goal (Term t) run = sys->maxruns - 1; rd = sys->runs[run].start; sys->runs[run].length = 1; - termDelete (rd->message); rd->message = termDuplicate (t); #ifdef DEBUG 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 flag; Roledef rd; + int old_run; + int old_index; roleInstance (sys, p, r, NULL); run = sys->maxruns - 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_index = index; #ifdef DEBUG @@ -277,7 +280,8 @@ bind_new_run (const Goal goal, const Protocol p, const Role r, iterate (); - goal.rd->bind_run = INVALID; + goal.rd->bind_run = old_run; + goal.rd->bind_index = old_index; roleInstanceDestroy (sys); return flag; } @@ -499,6 +503,15 @@ bind_goal (const Goal goal) int 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) { // Hardcoded limit on runs diff --git a/src/mgu.c b/src/mgu.c index a6e3900..8afcc63 100644 --- a/src/mgu.c +++ b/src/mgu.c @@ -173,20 +173,23 @@ termMguInTerm (Term t1, Term t2, int (*iterator) ()) flag = 1; t2 = deVar (t2); - if (t2 != NULL && isTermTuple (t2)) + if (t2 != NULL) { - // t2 is a tuple, consider interm options as well. - flag = flag && termMguInTerm (t1, t2->left.op1, iterator); - flag = flag && termMguInTerm (t1, t2->right.op2, iterator); - } - // simple clause or combined - tl = termMguTerm (t1, t2); - if (tl != MGUFAIL) - { - // Iterate - flag = flag && iterator (tl); - // Reset variables - termlistSubstReset (tl); + if (isTermTuple (t2)) + { + // t2 is a tuple, consider interm options as well. + flag = flag && termMguInTerm (t1, t2->left.op1, iterator); + flag = flag && termMguInTerm (t1, t2->right.op2, iterator); + } + // simple clause or combined + tl = termMguTerm (t1, t2); + if (tl != MGUFAIL) + { + // Iterate + flag = flag && iterator (tl); + // Reset variables + termlistSubstReset (tl); + } } return flag; } diff --git a/src/system.c b/src/system.c index e5299ca..445fbe8 100644 --- a/src/system.c +++ b/src/system.c @@ -269,9 +269,19 @@ ensureValidRun (const System sys, int run) myrun.step = 0; myrun.index = NULL; myrun.start = NULL; - myrun.know = knowledgeDuplicate (sys->know); - myrun.prevSymmRun = -1; - myrun.firstNonAgentRead = -1; + if (sys->engine == POR_ENGINE) + { + myrun.know = knowledgeDuplicate (sys->know); + myrun.prevSymmRun = -1; + myrun.firstNonAgentRead = -1; + } + else + { + // Arachne etc. + myrun.know = NULL; + myrun.prevSymmRun = -1; + myrun.firstNonAgentRead = -1; + } } }