From 74851e03936686b847d21eb896dda969d8e75907 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sat, 14 Aug 2004 14:27:46 +0000 Subject: [PATCH] - Consistency improvements. --- src/arachne.c | 43 +++++++++++++++++++++++-------------------- src/term.h | 2 +- 2 files changed, 24 insertions(+), 21 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 1922771..738684d 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -277,7 +277,7 @@ add_intruder_goal_iterate (Goal goal) //! Bind a goal to an existing regular run, if possible int bind_existing_run (const Goal goal, const Protocol p, const Role r, - const int index) + const int index, const int forced_run) { int run, flag; @@ -295,29 +295,32 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, goal.rd->bind_index = index; for (run = 0; run < sys->maxruns; run++) { - if (sys->runs[run].protocol == p && sys->runs[run].role == r) + if (forced_run >= 0 && forced_run == run) { - int old_length; - Roledef rd; + if (sys->runs[run].protocol == p && sys->runs[run].role == r) + { + int old_length; + Roledef rd; - // Roledef entry - rd = roledef_shift (sys->runs[run].start, index); + // Roledef entry + rd = roledef_shift (sys->runs[run].start, index); - // mgu and iterate - old_length = sys->runs[run].length; - if (index >= old_length) - sys->runs[run].length = index + 1; + // mgu and iterate + old_length = sys->runs[run].length; + if (index >= old_length) + sys->runs[run].length = index + 1; #ifdef DEBUG - explanation = "Bind existing run"; - e_run = run; - e_term1 = goal.rd->message; + explanation = "Bind existing run"; + e_run = run; + e_term1 = goal.rd->message; #endif - goal.rd->bind_run = run; + goal.rd->bind_run = run; - flag = (flag - && termMguInTerm (goal.rd->message, rd->message, - mgu_iterate)); - sys->runs[run].length = old_length; + flag = (flag + && termMguInTerm (goal.rd->message, rd->message, + mgu_iterate)); + sys->runs[run].length = old_length; + } } } goal.rd->bind_run = -1; @@ -463,7 +466,7 @@ bind_goal_regular (const Goal goal) { flag = flag && bind_new_run (goal, p, r, index); } - return (flag && bind_existing_run (goal, p, r, index)); + return (flag && bind_existing_run (goal, p, r, index, run)); } if (p == INTRUDER) @@ -542,7 +545,7 @@ bind_intruder_to_regular (Goal goal) { flag = flag && bind_new_run (goal, p, r, index); } - flag = flag && bind_existing_run (goal, p, r, index); + flag = flag && bind_existing_run (goal, p, r, index, run); /** * deconstruct key list goals diff --git a/src/term.h b/src/term.h index b3ea1de..f687a35 100644 --- a/src/term.h +++ b/src/term.h @@ -68,7 +68,7 @@ __inline__ Term deVarScan (Term t); #define realTermLeaf(t) (t != NULL && t->type <= LEAF) #define realTermTuple(t) (t != NULL && t->type == TUPLE) #define realTermEncrypt(t) (t != NULL && t->type == ENCRYPT) -#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (rolelocal_variable && t->right.runid == -3))) +#define realTermVariable(t) (t != NULL && (t->type == VARIABLE || (t->type <= LEAF && rolelocal_variable && t->right.runid == -3))) #define substVar(t) ((realTermVariable (t) && t->subst != NULL) ? 1 : 0) #define deVar(t) ( substVar(t) ? deVarScan(t->subst) : t) #define isTermLeaf(t) realTermLeaf(deVar(t))