andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Fixed a bug in the pruning algorithm, where intruder runs were also

Browse Source 
checked for agent lists, which is false.
This commit is contained in:
ccremers 2004-08-30 22:08:44 +00:00
parent b04bc86185
commit 5c90522c55
2 changed files with 33 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
src/arachne.c
View File

@ -1253,6 +1253,9 @@ bind_goal_new_intruder_run (const Binding b)
}
//! Bind a regular goal
/**
* Problem child. Valgrind does not like it.
*/
int
bind_goal_regular_run (const Binding b)
{
@ -1292,7 +1295,7 @@ bind_goal_regular_run (const Binding b)
if (!termMguSubTerm
(b->term, rd->message, test_sub_unification, sys->know->inverses, NULL))
{
int flag;
int sflag;
// A good candidate
found++;
@ -1317,11 +1320,11 @@ bind_goal_regular_run (const Binding b)
}
indentDepth++;
// Bind to existing run
flag = bind_existing_run (b, p, r, index);
sflag = bind_existing_run (b, p, r, index);
// bind to new run
flag = flag && bind_new_run (b, p, r, index);
sflag = sflag && bind_new_run (b, p, r, index);
indentDepth--;
return flag;
return sflag;
}
else
{
@ -1506,12 +1509,21 @@ prune_theorems ()
run = 1;
while (run < sys->maxruns)
{
if (inTermlist (sys->untrusted, agentOfRun (sys, run)))
if (sys->runs[run].protocol != INTRUDER)
{
if (sys->output == PROOF)
Term actor;
actor = agentOfRun(sys, run);
eprintf ("Bla %i ", run);
termPrint (actor);
eprintf ("\n");
if (inTermlist (sys->untrusted, actor))
{
indentPrint ();
eprintf ("Pruned because the actor of run %i is untrusted.\n", run);
if (sys->output == PROOF)
{
indentPrint ();
eprintf ("Pruned because the actor of run %i is untrusted.\n", run);
}
}
}
run++;

19
src/system.c
View File

@ -339,15 +339,22 @@ agentOfRunRole (const System sys, const int run, const Term role)
Termlist agents = sys->runs[run].agents;
/* TODO stupid reversed order, lose that soon */
agents = termlistForward (agents);
while (agents != NULL && roles != NULL)
if (agents != NULL)
{
if (isTermEqual (roles->term, role))
agents = termlistForward (agents);
while (agents != NULL && roles != NULL)
{
return agents->term;
if (isTermEqual (roles->term, role))
{
return agents->term;
}
agents = agents->prev;
roles = roles->next;
}
agents = agents->prev;
roles = roles->next;
}
else
{
error ("Agent list for run %i is empty, so agentOfRunRole is not usable.", run);
}
return NULL;
}