- Added term to binding relation.
This commit is contained in:
parent
9ec1bdc8eb
commit
5dd6127e4b
@ -279,7 +279,7 @@ add_intruder_goal_iterate (Goal goal)
|
|||||||
int run;
|
int run;
|
||||||
|
|
||||||
run = create_intruder_goal (goal.rd->message);
|
run = create_intruder_goal (goal.rd->message);
|
||||||
if (binding_add (run, 0, goal.run, goal.index))
|
if (binding_add (run, 0, goal.run, goal.index, goal.rd->message))
|
||||||
{
|
{
|
||||||
flag = iterate ();
|
flag = iterate ();
|
||||||
}
|
}
|
||||||
@ -329,7 +329,7 @@ bind_existing_to_goal (const Goal goal, const int index, const int run,
|
|||||||
int keyrun;
|
int keyrun;
|
||||||
|
|
||||||
keyrun = create_intruder_goal (keylist->term);
|
keyrun = create_intruder_goal (keylist->term);
|
||||||
if (!binding_add (keyrun, 0, goal.run, goal.index))
|
if (!binding_add (keyrun, 0, goal.run, goal.index, keylist->term))
|
||||||
flag = 0;
|
flag = 0;
|
||||||
keylist = keylist->next;
|
keylist = keylist->next;
|
||||||
keycount++;
|
keycount++;
|
||||||
@ -368,7 +368,7 @@ bind_existing_to_goal (const Goal goal, const int index, const int run,
|
|||||||
e_term2 = rd->message;
|
e_term2 = rd->message;
|
||||||
}
|
}
|
||||||
#endif
|
#endif
|
||||||
if (binding_add (run, index, goal.run, goal.index))
|
if (binding_add (run, index, goal.run, goal.index, goal.rd->message))
|
||||||
{
|
{
|
||||||
if (subterm)
|
if (subterm)
|
||||||
{
|
{
|
||||||
@ -729,10 +729,10 @@ bind_intruder_to_construct (const Goal goal)
|
|||||||
}
|
}
|
||||||
|
|
||||||
run = create_intruder_goal (t1);
|
run = create_intruder_goal (t1);
|
||||||
if (binding_add (run, 0, goal.run, goal.index))
|
if (binding_add (run, 0, goal.run, goal.index, t1))
|
||||||
{
|
{
|
||||||
run = create_intruder_goal (t2);
|
run = create_intruder_goal (t2);
|
||||||
if (binding_add (run, 0, goal.run, goal.index))
|
if (binding_add (run, 0, goal.run, goal.index, t2))
|
||||||
{
|
{
|
||||||
flag = flag && iterate ();
|
flag = flag && iterate ();
|
||||||
}
|
}
|
||||||
@ -761,7 +761,7 @@ bind_intruder_to_construct (const Goal goal)
|
|||||||
run = sys->maxruns - 1;
|
run = sys->maxruns - 1;
|
||||||
sys->runs[run].start->message = termDuplicate(term);
|
sys->runs[run].start->message = termDuplicate(term);
|
||||||
sys->runs[run].length = 1;
|
sys->runs[run].length = 1;
|
||||||
if (binding_add (run, 0, goal.run, goal.index))
|
if (binding_add (run, 0, goal.run, goal.index, term))
|
||||||
{
|
{
|
||||||
#ifdef DEBUG
|
#ifdef DEBUG
|
||||||
if (DEBUGL (3))
|
if (DEBUGL (3))
|
||||||
|
@ -8,6 +8,7 @@
|
|||||||
#include "warshall.h"
|
#include "warshall.h"
|
||||||
#include "memory.h"
|
#include "memory.h"
|
||||||
#include "debug.h"
|
#include "debug.h"
|
||||||
|
#include "term.h"
|
||||||
|
|
||||||
/*
|
/*
|
||||||
* Idea is the ev_from *has to* precede the ev_to
|
* Idea is the ev_from *has to* precede the ev_to
|
||||||
@ -22,6 +23,8 @@ struct binding
|
|||||||
|
|
||||||
int *graph;
|
int *graph;
|
||||||
int nodes;
|
int nodes;
|
||||||
|
|
||||||
|
Term term;
|
||||||
};
|
};
|
||||||
|
|
||||||
typedef struct binding *Binding;
|
typedef struct binding *Binding;
|
||||||
@ -36,7 +39,7 @@ static System sys;
|
|||||||
|
|
||||||
//! Create mem for binding
|
//! Create mem for binding
|
||||||
Binding
|
Binding
|
||||||
binding_create (int run_from, int ev_from, int run_to, int ev_to)
|
binding_create (int run_from, int ev_from, int run_to, int ev_to, Term term)
|
||||||
{
|
{
|
||||||
Binding b;
|
Binding b;
|
||||||
|
|
||||||
@ -47,6 +50,7 @@ binding_create (int run_from, int ev_from, int run_to, int ev_to)
|
|||||||
b->ev_to = ev_to;
|
b->ev_to = ev_to;
|
||||||
b->graph = NULL;
|
b->graph = NULL;
|
||||||
b->nodes = 0;
|
b->nodes = 0;
|
||||||
|
b->term = term;
|
||||||
return b;
|
return b;
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -226,7 +230,7 @@ binding_print (void *bindany)
|
|||||||
*@returns True iff is a valid additional binding. False if not.
|
*@returns True iff is a valid additional binding. False if not.
|
||||||
*/
|
*/
|
||||||
int
|
int
|
||||||
binding_add (int run_from, int ev_from, int run_to, int ev_to)
|
binding_add (int run_from, int ev_from, int run_to, int ev_to, Term term)
|
||||||
{
|
{
|
||||||
Binding b;
|
Binding b;
|
||||||
int flag;
|
int flag;
|
||||||
@ -234,7 +238,9 @@ binding_add (int run_from, int ev_from, int run_to, int ev_to)
|
|||||||
#ifdef DEBUG
|
#ifdef DEBUG
|
||||||
if (DEBUGL (5))
|
if (DEBUGL (5))
|
||||||
{
|
{
|
||||||
eprintf ("Adding binding (%i,%i) --->> (%i,%i)\n", run_from, ev_from,
|
eprintf ("Adding binding (%i,%i) --(", run_from, ev_from);
|
||||||
|
termPrint (term);
|
||||||
|
eprintf (")-->> (%i,%i)\n",
|
||||||
run_to, ev_to);
|
run_to, ev_to);
|
||||||
}
|
}
|
||||||
if (ev_from >= sys->runs[run_from].step)
|
if (ev_from >= sys->runs[run_from].step)
|
||||||
@ -246,7 +252,7 @@ binding_add (int run_from, int ev_from, int run_to, int ev_to)
|
|||||||
if (run_to < 0 || run_to >= sys->maxruns)
|
if (run_to < 0 || run_to >= sys->maxruns)
|
||||||
error ("run_to out of scope.");
|
error ("run_to out of scope.");
|
||||||
#endif
|
#endif
|
||||||
b = binding_create (run_from, ev_from, run_to, ev_to);
|
b = binding_create (run_from, ev_from, run_to, ev_to, term);
|
||||||
sys->bindings = list_insert (sys->bindings, b);
|
sys->bindings = list_insert (sys->bindings, b);
|
||||||
|
|
||||||
/*
|
/*
|
||||||
|
@ -1,12 +1,15 @@
|
|||||||
#ifndef BINDINGS
|
#ifndef BINDINGS
|
||||||
#define BINDINGS
|
#define BINDINGS
|
||||||
|
|
||||||
|
#include "term.h"
|
||||||
|
#include "system.h"
|
||||||
|
|
||||||
void bindingInit (const System mysys);
|
void bindingInit (const System mysys);
|
||||||
void bindingDone ();
|
void bindingDone ();
|
||||||
|
|
||||||
int node_count ();
|
int node_count ();
|
||||||
int node_number (int run, int ev);
|
int node_number (int run, int ev);
|
||||||
int binding_add (int run_from, int ev_from, int run_to, int ev_to);
|
int binding_add (int run_from, int ev_from, int run_to, int ev_to, Term term);
|
||||||
void binding_remove_last ();
|
void binding_remove_last ();
|
||||||
int binding_print (void *bindany);
|
int binding_print (void *bindany);
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user