- Improved pruning.
This commit is contained in:
ccremers
parent
0f75efc787
commit
c95630f93b
@ -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;
|
||||
}
|
||||
|
||||
|
||||
@ -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))
|
||||
{
|
||||
|
||||
Loading…
Reference in New Issue
Block a user