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.
This commit is contained in:
ccremers
parent
91a679a129
commit
c518e68881
@ -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;
|
||||
|
||||
/**
|
||||
|
||||
@ -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 */
|
||||
|
||||
35
src/system.c
35
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);
|
||||
|
||||
@ -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 ();
|
||||
|
||||
Loading…
Reference in New Issue
Block a user