From afda4f355e4f13a4304fcae5afcc4afe3b5bf37d Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Fri, 13 Aug 2004 20:56:51 +0000
Subject: [PATCH] - Added much debug info, so we can see send iteration is
 going wrong.   But why?

---
 src/arachne.c | 86 ++++++++++++++++++++++++++++++++++++++++++---------
 src/system.c  |  2 ++
 2 files changed, 74 insertions(+), 14 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index 0fb9fbb..a5128f0 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -202,6 +202,10 @@ create_intruder_goal (Term t)
 int
 add_intruder_goal_iterate (Goal goal)
 {
+  // [x][todo][cc] remove debug you know the drill
+  //!@debug Remove this
+  return 1;
+
   int flag;
   int run;
 
@@ -223,6 +227,16 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
 {
   int run, flag;
 
+#ifdef DEBUG
+  indentPrint ();
+  eprintf ("Trying to bind ");
+  termPrint (goal.rd->message);
+  eprintf (" to an existing instance of ");
+  termPrint (p->nameterm);
+  eprintf (", ");
+  termPrint (r->nameterm);
+  eprintf ("\n");
+#endif
   flag = 1;
   for (run = 0; run < sys->maxruns; run++)
     {
@@ -361,39 +375,67 @@ select_goal ()
 int
 bind_goal_regular (const Goal goal)
 {
+  int flag;
   /*
    * This is a local function so we have access to goal
    */
-  int bind_this (Protocol p, Role r, Roledef rd, int index)
+  int bind_this_role_send (Protocol p, Role r, Roledef rd, int index)
   {
-    int element_f1 (Termlist substlist)
+    int bind_this_unification (Termlist substlist)
     {
+#ifdef DEBUG
+      indentPrint ();
+      eprintf ("Term ");
+      termPrint (goal.rd->message);
+      eprintf (" can possibly be bound by role ");
+      termPrint (r->nameterm);
+      eprintf (", index %i.\n", index);
+#endif
       /**
        * Two options; as this, it is from an existing run,
        * or from a new one.
-       *
-       * Note that we only bind to regular runs here
        */
-      if (p == INTRUDER)
-	{
-	  return 1;		// don't abort scans
-	}
       return (bind_existing_run (goal, p, r, index)
 	      && bind_new_run (goal, p, r, index));
     }
 
-    // Test for interm unification
-    return termMguInTerm (goal.rd->message, rd->message, element_f1);
+    if (p == INTRUDER)
+      {
+	/* only bind to regular runs */
+	return 1;
+      }
+    else
+      {
+	// Test for interm unification
+#ifdef DEBUG
+	indentPrint ();
+	eprintf ("Checking send candidate with message ");
+	termPrint (rd->message);
+	eprintf (" from ");
+	termPrint (p->nameterm);
+	eprintf (", ");
+	termPrint (r->nameterm);
+	eprintf (", index%i\n");
+#endif
+	return termMguInTerm (goal.rd->message, rd->message,
+			      bind_this_unification);
+      }
   }
 
   // Bind to all possible sends or intruder node;
-  return (iterate_role_sends (bind_this) && add_intruder_goal_iterate (goal));
+#ifdef DEBUG
+  indentPrint ();
+  eprintf ("Try regular role send.\n");
+#endif
+  flag = iterate_role_sends (bind_this_role_send);
+#ifdef DEBUG
+  indentPrint ();
+  eprintf ("Try intruder send.\n");
+#endif
+  return (flag && add_intruder_goal_iterate (goal));
 }
 
 //! Bind an intruder goal to a regular run
-/**
- * A bit of a problem child, this one.
- */
 int
 bind_intruder_to_regular (Goal goal)
 {
@@ -458,6 +500,9 @@ bind_intruder_to_regular (Goal goal)
 }
 
 //! Bind an intruder goal by intruder construction
+/**
+ * Handles the case where the intruder constructs a composed term himself.
+ */
 int
 bind_intruder_to_construct (const Goal goal)
 {
@@ -655,6 +700,19 @@ arachne ()
     }
 
 #ifdef DEBUG
+  int print_send (Protocol p, Role r, Roledef rd, int index)
+  {
+    eprintf ("IRS: ");
+    termPrint (p->nameterm);
+    eprintf (", ");
+    termPrint (r->nameterm);
+    eprintf (", %i, ", index);
+    roledefPrint (rd);
+    eprintf ("\n");
+  }
+
+  iterate_role_sends (print_send);
+
   explanation = NULL;
   e_run = INVALID;
   e_term1 = NULL;
diff --git a/src/system.c b/src/system.c
index 23b0d86..ba7f622 100644
--- a/src/system.c
+++ b/src/system.c
@@ -599,6 +599,8 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 	      artefacts = termlistAdd (artefacts, newt);
 	      // Copy substitution
 	      newt->subst = oldt->subst;
+	      // Remove any old substitution! It is now propagated!
+	      oldt->subst = NULL;
 	    }
 	  // Add to agent list, possibly
 	  if (inTermlist (protocol->rolenames, oldt))