From c518e688813b3a8dcd7bb31b585540d3dc9832aa Mon Sep 17 00:00:00 2001 From: ccremers Date: Sun, 15 Aug 2004 19:58:26 +0000 Subject: [PATCH] BROKEN - Added broken attempt to solve to problem, where a new instance has to be bound, but older variables point to role terms, e.g. RV#1->RV. What should happen, is that it becomes RV#1->RV#new. I thought of a solution, but it is still somewhat broken. Maybe I should ignore any mappings of variables such as RV, which might be included. --- src/arachne.c | 43 +++++++++++++++++++++++++------------------ src/compiler.c | 2 +- src/system.c | 35 ++++++++++++++++++++++++++++++++++- src/system.h | 3 ++- 4 files changed, 62 insertions(+), 21 deletions(-) diff --git a/src/arachne.c b/src/arachne.c index e1600b6..d56e249 100644 --- a/src/arachne.c +++ b/src/arachne.c @@ -258,7 +258,7 @@ create_intruder_goal (Term t) int run; Roledef rd; - roleInstance (sys, INTRUDER, I_GOAL, NULL); + roleInstance (sys, INTRUDER, I_GOAL, NULL, NULL); run = sys->maxruns - 1; rd = sys->runs[run].start; sys->runs[run].length = 1; @@ -300,9 +300,12 @@ add_intruder_goal_iterate (Goal goal) } //! Bind a goal to an existing regular run, if possible +/** + *@todo Currently we don't use subterm. This interm binds, which is much different from subterm binding. + */ int bind_existing_run (const Goal goal, const Protocol p, const Role r, - const int index, const int forced_run) + const int index, const int forced_run, const int subterm) { int run, flag; @@ -342,13 +345,16 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, explanation = "Bind existing run"; e_run = run; e_term1 = goal.rd->message; + e_term2 = rd->message; } #endif if (binding_add (run, index, goal.run, goal.index)) { - flag = (flag - && termMguInTerm (goal.rd->message, rd->message, - mgu_iterate)); + { + flag = (flag + && termMguInTerm (goal.rd->message, rd->message, + mgu_iterate)); + } } else { @@ -367,13 +373,13 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r, //! Bind a goal to a new run int bind_new_run (const Goal goal, const Protocol p, const Role r, - const int index) + const int index, Termlist substlist) { int run; int flag; Roledef rd; - roleInstance (sys, p, r, NULL); + roleInstance (sys, p, r, NULL, substlist); run = sys->maxruns - 1; sys->runs[run].length = index + 1; if (binding_add (run, index, goal.run, goal.index)) @@ -386,6 +392,7 @@ bind_new_run (const Goal goal, const Protocol p, const Role r, e_term1 = r->nameterm; rd = roledef_shift (sys->runs[run].start, index); e_term2 = rd->message; + e_term3 = goal.rd->message; } #endif @@ -411,12 +418,12 @@ printSemiState () List bl; int binding_indent_print (void *data) - { - indentPrint (); - eprintf ("!! "); - binding_print (data); - return 1; - } + { + indentPrint (); + eprintf ("!! "); + binding_print (data); + return 1; + } indentPrint (); eprintf ("!! --=[ Semistate ]=--\n"); @@ -547,9 +554,9 @@ bind_goal_regular (const Goal goal) flag = 1; if (run == -2) { - flag = flag && bind_new_run (goal, p, r, index); + flag = flag && bind_new_run (goal, p, r, index, substlist); } - return (flag && bind_existing_run (goal, p, r, index, run)); + return (flag && bind_existing_run (goal, p, r, index, run, 0)); } if (p == INTRUDER) @@ -635,9 +642,9 @@ bind_intruder_to_regular (Goal goal) flag = 1; if (run == -2) { - flag = flag && bind_new_run (goal, p, r, index); + flag = flag && bind_new_run (goal, p, r, index, substlist); } - flag = flag && bind_existing_run (goal, p, r, index, run); + flag = flag && bind_existing_run (goal, p, r, index, run, 1); /** * deconstruct key list goals @@ -1030,7 +1037,7 @@ arachne () } #endif - roleInstance (sys, p, r, NULL); + roleInstance (sys, p, r, NULL, NULL); sys->runs[0].length = cl->ev + 1; /** diff --git a/src/compiler.c b/src/compiler.c index fd3fbee..594652a 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -652,7 +652,7 @@ runInstanceCreate (Tac tc) } /* equal numbers, so it seems to be safe */ - roleInstance (sys, p, r, instParams); // technically, we don't need to do this for Arachne [fix later] + roleInstance (sys, p, r, instParams, NULL); // technically, we don't need to do this for Arachne [fix later] /* after creation analysis */ /* AC1: untrusted agents */ diff --git a/src/system.c b/src/system.c index f71f14f..ce3186f 100644 --- a/src/system.c +++ b/src/system.c @@ -485,7 +485,7 @@ firstNonAgentRead (const System sys, int rid) void roleInstance (const System sys, const Protocol protocol, const Role role, - const Termlist paramlist) + const Termlist paramlist, Termlist substlist) { int rid; Run runs; @@ -671,6 +671,20 @@ roleInstance (const System sys, const Protocol protocol, const Role role, rd->message = termLocal (rd->message, fromlist, tolist, rid); rd = rd->next; } + + runs[rid].substitutions = NULL; + while (substlist != NULL) + { + Term t; + + t = substlist->term; + if (t->subst != NULL) + { + t->subst = termLocal (t->subst, fromlist, tolist, rid); + runs[rid].substitutions = termlistAdd (runs[rid].substitutions, t); + } + substlist = substlist->next; + } termlistDelete (fromlist); runs[rid].locals = tolist; runs[rid].artefacts = artefacts; @@ -700,6 +714,7 @@ roleInstanceDestroy (const System sys) { int runid; struct run myrun; + Termlist substlist; runid = sys->maxruns - 1; myrun = sys->runs[runid]; @@ -723,6 +738,24 @@ roleInstanceDestroy (const System sys) artefacts = artefacts->next; } } + + /** + * Undo the local copies of the substitutions. We cannot restore them however, so this might + * prove a problem. We assume that the substlist fixes this at roleInstance time; it should be exact. + */ + substlist = myrun.substitutions; + while (substlist != NULL) + { + Term t; + + t = substlist->term; + if (t->subst != NULL) + { + termDelete (t->subst); + t->subst = NULL; + } + substlist = substlist->next; + } termlistDelete (myrun.artefacts); termlistDelete (myrun.locals); termlistDelete (myrun.agents); diff --git a/src/system.h b/src/system.h index cf4b3fc..49a728b 100644 --- a/src/system.h +++ b/src/system.h @@ -49,6 +49,7 @@ struct run Knowledge know; //!< Current knowledge of the run. Termlist locals; //!< Locals of the run. Termlist artefacts; //!< Stuff created especially for this run. + Termlist substitutions; //!< The substitutions as they came from the roledef unifier int prevSymmRun; //!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter. int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate. int firstReal; //!< 1 if a choose was inserted, otherwise 0 @@ -214,7 +215,7 @@ void runsPrint (const System sys); Term agentOfRunRole (const System sys, const int run, const Term role); Term agentOfRun (const System sys, const int run); void roleInstance (const System sys, const Protocol protocol, const Role role, - const Termlist tolist); + const Termlist paramlist, Termlist substlist); void roleInstanceDestroy (const System sys); void systemStart (const System sys); void indentActivate ();