From c95630f93bd2a60cb3035bfa723677658914a955 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 18 Aug 2004 19:43:58 +0000 Subject: [PATCH] - Improved pruning. --- src/arachne.c | 55 ++++++++++++++++++++++++++++++++++----------------- src/binding.c | 23 ++++++++++++++++++--- 2 files changed, 57 insertions(+), 21 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index 44c2d48..0972221 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -25,6 +25,7 @@ extern Term CLAIM_Secret; extern Term CLAIM_Nisynch; extern Term CLAIM_Niagree; extern Term TERM_Agent; +extern Term TERM_Hidden; static System sys; Protocol INTRUDER; // Pointers, to be set by the Init @@ -303,8 +304,7 @@ iterate_role_sends (int (*func) ()) *@param subterm determines whether it is a subterm unification or not. */ int -bind_existing_to_goal (const Binding b, const int index, const int run, - const int subterm) +bind_existing_to_goal (const Binding b, const int run, const int index) { Roledef rd; int flag; @@ -395,7 +395,7 @@ bind_existing_to_goal (const Binding b, const int index, const int run, //! Bind a goal to an existing regular run, if possible int bind_existing_run (const Binding b, const Protocol p, const Role r, - const int index, const int subterm) + const int index) { int run, flag; @@ -409,7 +409,7 @@ bind_existing_run (const Binding b, const Protocol p, const Role r, termPrint (p->nameterm); eprintf (", "); termPrint (r->nameterm); - eprintf (" (%i)\n", subterm); + eprintf ("\n"); } #endif flag = 1; @@ -417,7 +417,7 @@ bind_existing_run (const Binding b, const Protocol p, const Role r, { if (sys->runs[run].protocol == p && sys->runs[run].role == r) { - flag = flag && bind_existing_to_goal (b, index, run, subterm); + flag = flag && bind_existing_to_goal (b, run, index); } } return flag; @@ -426,7 +426,7 @@ bind_existing_run (const Binding b, const Protocol p, const Role r, //! Bind a goal to a new run int bind_new_run (const Binding b, const Protocol p, const Role r, - const int index, const int subterm) + const int index) { int run; int flag; @@ -445,10 +445,10 @@ bind_new_run (const Binding b, const Protocol p, const Role r, termPrint (p->nameterm); eprintf (", "); termPrint (r->nameterm); - eprintf (", run %i (subterm:%i)\n", run, subterm); + eprintf (", run %i\n", run); } #endif - flag = bind_existing_to_goal (b, index, run, 1); + flag = bind_existing_to_goal (b, run, index); remove_read_goals (newgoals); roleInstanceDestroy (sys); return flag; @@ -548,7 +548,9 @@ select_goal () if (!b->done) { // We don't care about singular agent variables, so... - if (! (isTermVariable (b->term) && inTermlist (b->term->stype, TERM_Agent))) + if (! + (isTermVariable (b->term) + && inTermlist (b->term->stype, TERM_Agent))) { float cons; @@ -657,7 +659,7 @@ bind_goal_new_encrypt (const Binding b) rd->next->message = termDuplicate (t2); rd->next->next->message = termDuplicate (term); index = 2; - newgoals = add_read_goals (run, 0, index+1); + newgoals = add_read_goals (run, 0, index + 1); #ifdef DEBUG if (DEBUGL (3)) { @@ -673,7 +675,7 @@ bind_goal_new_encrypt (const Binding b) #endif if (goal_bind (b, run, index)) { - flag = flag && iterate (); + flag = flag && iterate (); } goal_unbind (b); remove_read_goals (newgoals); @@ -689,7 +691,7 @@ bind_goal_new_encrypt (const Binding b) int bind_goal_new_intruder_run (const Binding b) { - return (bind_goal_new_m0(b) && bind_goal_new_encrypt(b)); + return (bind_goal_new_m0 (b) && bind_goal_new_encrypt (b)); } //! Bind a regular goal @@ -747,9 +749,9 @@ bind_goal_regular_run (const Binding b) } #endif // Bind to existing run - flag = bind_existing_run (b, p, r, index, 1); + flag = bind_existing_run (b, p, r, index); // bind to new run - flag = flag && bind_new_run (b, p, r, index, 1); + flag = flag && bind_new_run (b, p, r, index); return flag; } else @@ -772,7 +774,8 @@ bind_goal_regular_run (const Binding b) // Bind to all possible sends of intruder runs -int bind_goal_old_intruder_run (Binding b) +int +bind_goal_old_intruder_run (Binding b) { int run; int flag; @@ -781,7 +784,7 @@ int bind_goal_old_intruder_run (Binding b) if (DEBUGL (5)) { indentPrint (); - eprintf ("Try regular intruder send.\n"); + eprintf ("Try existing intruder send.\n"); } #endif @@ -793,13 +796,13 @@ int bind_goal_old_intruder_run (Binding b) int ev; Roledef rd; - rd = sys->runs[run].start; + rd = sys->runs[run].start; ev = 0; while (ev < sys->runs[run].length) { if (rd->type == SEND) { - flag = flag && bind_existing_to_goal (b, ev, run, 1); + flag = flag && bind_existing_to_goal (b, run, ev); } rd = rd->next; ev++; @@ -836,6 +839,7 @@ int prune () { Termlist tl; + List bl; if (indentDepth > 20) { @@ -919,6 +923,21 @@ prune () return 1; } + // Check for "Hidden" interm goals + bl = sys->bindings; + while (bl != NULL) + { + Binding b; + + b = bl->data; + if (termInTerm (b->term, TERM_Hidden)) + { + // Prune the state: we can never meet this + return 1; + } + bl = bl->next; + } + return 0; } diff --git a/src/binding.c b/src/binding.c index a8c98be..712f797 100644 --- a/src/binding.c +++ b/src/binding.c @@ -3,6 +3,7 @@ */ #include "list.h" +#include "role.h" #include "system.h" #include "binding.h" #include "warshall.h" @@ -14,6 +15,9 @@ static System sys; static int *graph; static int nodes; +extern Protocol INTRUDER; // The intruder protocol +extern Role I_M; // special role; precedes all other events always + /* * * Assist stuff @@ -93,6 +97,7 @@ void goal_graph_create () { int run, ev; + int last_m; List bl; goal_graph_destroy (); @@ -104,6 +109,7 @@ goal_graph_create () // Setup run order run = 0; + last_m = -1; // last I_M run while (run < sys->maxruns) { ev = 1; @@ -113,6 +119,16 @@ goal_graph_create () graph[graph_nodes (nodes, run, ev - 1, run, ev)] = 1; ev++; } + // Enforce I_M ordering + if (sys->runs[run].protocol == INTRUDER && sys->runs[run].role == I_M) + { + if (last_m != -1) + { + graph[graph_nodes (nodes, last_m, 0, run, 0)] = 1; + } + last_m = run; + } + // Next run++; } // Setup bindings order @@ -228,11 +244,12 @@ goal_add (Term term, const int run, const int ev) term = deVar (term); #ifdef DEBUG if (term == NULL) - error ("Trying to add an emtpy goal term"); + error ("Trying to add an emtpy goal term"); if (run >= sys->maxruns) - error ("Trying to add a goal for a run that does not exist."); + error ("Trying to add a goal for a run that does not exist."); if (ev >= sys->runs[run].step) - error ("Trying to add a goal for an event that is not in the semistate yet."); + error + ("Trying to add a goal for an event that is not in the semistate yet."); #endif if (realTermTuple (term)) {