- Integrated new binding relation. No closure as yet.

src/arachne.c

@@ -17,6 +17,7 @@
 #include "error.h"
 #include "claim.h"
 #include "debug.h"
+#include "binding.h"
 
 extern CLAIM_Secret;
 extern CLAIM_Nisynch;
@@ -121,7 +122,7 @@ arachneDone ()
  */
 #define INVALID		-1
 #define isGoal(rd)	(rd->type == READ && !rd->internal)
-#define isBound(rd)	(rd->bind_run != INVALID)
+#define isBound(rd)	(rd->bound)
 #define length		step
 
 //! Indent print
@@ -274,13 +275,17 @@ add_intruder_goal_iterate (Goal goal)
   int run;
 
   run = create_intruder_goal (goal.rd->message);
-  goal.rd->bind_run = run;
-  goal.rd->bind_index = 0;
-
+  if (binding_add (run, 0, goal.run, goal.index))
+    {
       flag = iterate ();
+      binding_remove_last ();
+    }
+  else
+    {
+      flag = 1;
+    }
 
   roleInstanceDestroy (sys);	// destroy the created run
-  goal.rd->bind_run = INVALID;
   return flag;
 }
 
@@ -305,7 +310,6 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
     }
 #endif
   flag = 1;
-  goal.rd->bind_index = index;
   for (run = 0; run < sys->maxruns; run++)
     {
       if (forced_run == -2 || forced_run == run)
@@ -330,16 +334,17 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
 		  e_term1 = goal.rd->message;
 		}
 #endif
-	      goal.rd->bind_run = run;
-
+	      if (binding_add (run, index, goal.run, goal.index))
+		{
 		  flag = (flag
 			  && termMguInTerm (goal.rd->message, rd->message,
 					    mgu_iterate));
+		  binding_remove_last ();
+		}
 	      sys->runs[run].length = old_length;
 	    }
 	}
     }
-  goal.rd->bind_run = -1;
   return flag;
 }
 
@@ -354,13 +359,12 @@ bind_new_run (const Goal goal, const Protocol p, const Role r,
   int old_run;
   int old_index;
 
+  //!@todo if binding_add does not require the roleinstance to be done, move roleInstance into if of binding add (more efficient)
   roleInstance (sys, p, r, NULL);
   run = sys->maxruns - 1;
   sys->runs[run].length = index + 1;
-  old_run = goal.rd->bind_run;
-  old_index = goal.rd->bind_index;
-  goal.rd->bind_run = run;
-  goal.rd->bind_index = index;
+  if (binding_add (run, index, goal.run, goal.index))
+    {
 #ifdef DEBUG
       if (DEBUGL (3))
 	{
@@ -374,8 +378,12 @@ bind_new_run (const Goal goal, const Protocol p, const Role r,
 
       flag = iterate ();
 
-  goal.rd->bind_run = old_run;
-  goal.rd->bind_index = old_index;
+      binding_remove_last ();
+    }
+  else
+    {
+      flag = 1;
+    }
 
   roleInstanceDestroy (sys);
   return flag;
@@ -675,13 +683,24 @@ bind_goal_intruder (const Goal goal)
 int
 bind_goal (const Goal goal)
 {
+  if (!goal.rd->bound)
+    {
+      int flag;
+      goal.rd->bound = 1;
       if (sys->runs[goal.run].protocol == INTRUDER)
 	{
-      return bind_goal_intruder (goal);
+	  flag = bind_goal_intruder (goal);
 	}
       else
 	{
-      return bind_goal_regular (goal);
+	  flag = bind_goal_regular (goal);
+	}
+      goal.rd->bound = 0;
+      return flag;
+    }
+  else
+    {
+      return 1;
     }
 }
 

src/binding.c

@@ -7,6 +7,9 @@
 #include "binding.h"
 #include "memory.h"
 
+/*
+ * Idea is the ev_from *has to* precede the ev_to
+ */
 struct binding
 {
   int run_from;
@@ -112,7 +115,7 @@ binding_remove_last ()
   manual = 0;
   list = sys->bindings;
 
-  while (!manual && list != NULL);
+  while (list != NULL && !manual)
     {
       Binding b;
 

src/role.c

@@ -157,8 +157,10 @@ roledefInit (int type, Term label, Term from, Term to, Term msg, Claimlist cl)
   newEvent->forbidden = NULL;	// no forbidden stuff
   newEvent->knowPhase = -1;	// we haven't explored any knowledge yet
   newEvent->claiminfo = cl;	// only for claims
-  newEvent->bind_run = -1;	// unbound goal
-  newEvent->bind_index = -1;	// unbound goal
+  if (type == READ)
+    newEvent->bound = 0;	// bound goal (Used for arachne only). Technically involves choose events as well.
+  else
+    newEvent->bound = 1;	// other stuff does not need to be bound
   newEvent->next = NULL;
   return newEvent;
 }

src/role.h

@@ -89,8 +89,7 @@ struct roledef
   /*
    * Bindings for Arachne engine
    */
-  int bind_run;			//!< -1 for unbound
-  int bind_index;
+  int bound;
 
   /* evt runid for synchronisation, but that is implied in the
      base array */