- Implemented cycle detection. Untested.

src/arachne.c

@@ -19,9 +19,9 @@
 #include "debug.h"
 #include "binding.h"
 
-extern CLAIM_Secret;
-extern CLAIM_Nisynch;
-extern CLAIM_Niagree;
+extern Term CLAIM_Secret;
+extern Term CLAIM_Nisynch;
+extern Term CLAIM_Niagree;
 
 static System sys;
 Protocol INTRUDER;		// Pointers, to be set by the Init
@@ -278,13 +278,14 @@ add_intruder_goal_iterate (Goal goal)
   if (binding_add (run, 0, goal.run, goal.index))
     {
       flag = iterate ();
-      binding_remove_last ();
     }
   else
     {
+      indentPrint ();
+      eprintf ("Aborted adding intruder goal because of cycle.\n");
       flag = 1;
     }
-
+  binding_remove_last ();
   roleInstanceDestroy (sys);	// destroy the created run
   return flag;
 }
@@ -339,8 +340,14 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
 		  flag = (flag
 			  && termMguInTerm (goal.rd->message, rd->message,
 					    mgu_iterate));
-		  binding_remove_last ();
 		}
+	      else
+		{
+		  indentPrint ();
+		  eprintf
+		    ("Aborted binding existing run because of cycle.\n");
+		}
+	      binding_remove_last ();
 	      sys->runs[run].length = old_length;
 	    }
 	}
@@ -359,7 +366,6 @@ 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;
@@ -377,14 +383,14 @@ bind_new_run (const Goal goal, const Protocol p, const Role r,
 #endif
 
       flag = iterate ();
-
-      binding_remove_last ();
     }
   else
     {
+      indentPrint ();
+      eprintf ("Aborted binding new run because of cycle.\n");
       flag = 1;
     }
-
+  binding_remove_last ();
   roleInstanceDestroy (sys);
   return flag;
 }
@@ -741,7 +747,7 @@ prune ()
 //! Setup system for specific claim test
 add_claim_specifics (Claimlist cl, Roledef rd)
 {
-  if (isTermEqual (cl->type, CLAIM_Secret))
+  if (cl->type == CLAIM_Secret)
     {
       /**
        * Secrecy claim

src/binding.c

@@ -18,7 +18,8 @@ struct binding
   int run_to;
   int ev_to;
 
-  int manual;
+  int *graph;
+  int nodes;
 };
 
 typedef struct binding *Binding;
@@ -42,7 +43,8 @@ binding_create (int run_from, int ev_from, int run_to, int ev_to, int manual)
   b->ev_from = ev_from;
   b->run_to = run_to;
   b->ev_to = ev_to;
-  b->manual = manual;
+  b->graph = NULL;
+  b->nodes = 0;
   return b;
 }
 
@@ -50,6 +52,10 @@ binding_create (int run_from, int ev_from, int run_to, int ev_to, int manual)
 void
 binding_destroy (Binding b)
 {
+  if (b->graph != NULL)
+    {
+      memFree (b->graph, (b->nodes * b->nodes) * sizeof (int));
+    }
   memFree (b, sizeof (struct binding));
 }
 
@@ -80,17 +86,116 @@ bindingDone ()
   list_destroy (sys->bindings);
 }
 
-
 /**
  *
  * Externally available functions
  *
  */
 
+//! Yield node count
+int
+node_count ()
+{
+  int count;
+  int run;
+
+  count = 0;
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      //!@todo This now reference to step, but we intend "length" as in Arachne.
+      count = count + sys->runs[run].step;
+    }
+  return count;
+}
+
+//! Yield node number given run, ev
+__inline__ int
+node_number (int run, int ev)
+{
+  int node;
+
+  node = ev;
+  while (run > 0)
+    {
+      //!@todo This now reference to step, but we intend "length" as in Arachne.
+      node = node + sys->runs[run].step;
+      run--;
+    }
+  return node;
+}
+
+//! Yield graph index, given node1, node2 numbers
+__inline__ int
+graph_index (const int nodes, const int node1, const int node2)
+{
+  return ((node1 * nodes) + node2);
+}
+
+//! Yield graph index, given (node1), (node2) tuples
+__inline__ int
+graph_nodes (const int nodes, const int run1, const int ev1, const int run2,
+	     const int ev2)
+{
+  int node1;
+  int node2;
+
+  node1 = node_number (run1, ev1);
+  node2 = node_number (run2, ev2);
+  return graph_index (nodes, node1, node2);
+}
+
+//! Compute closure graph
+/**
+ *@returns 0 iff there is a cycle, 1 otherwise
+ */
+int
+closure_graph (Binding b)
+{
+  int nodes;
+  int *graph;
+  int run, ev;
+  List bl;
+
+  // Setup graph
+  nodes = node_count ();
+  graph = memAlloc (nodes * nodes * sizeof (int));
+  graph_fill (graph, nodes, 0);
+  b->nodes = nodes;
+  b->graph = graph;
+
+  // Setup run order
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      ev = 1;
+      //!@todo This now reference to step, but we intend "length" as in Arachne.
+      while (ev < sys->runs[run].step)
+	{
+	  graph[graph_nodes (nodes, run, ev - 1, run, ev)] = 1;
+	  ev++;
+	}
+      run++;
+    }
+  // Setup bindings order
+  bl = sys->bindings;
+  while (bl != NULL)
+    {
+      Binding b;
+
+      b = (Binding) bl->data;
+      graph[graph_nodes (nodes, b->run_from, b->ev_from, b->run_to, b->ev_to)]
+	= 1;
+      bl = bl->next;
+    }
+
+  return warshall (graph, nodes);
+}
+
+
 //! Add a binding
 /**
  * Note that bindings are added to the head of the list.
- *@returns True iff is a valid additional binding. False if not. If false, nothing needs to be destroyed.
+ *@returns True iff is a valid additional binding. False if not.
  */
 int
 binding_add (int run_from, int ev_from, int run_to, int ev_to)
@@ -99,7 +204,11 @@ binding_add (int run_from, int ev_from, int run_to, int ev_to)
 
   b = binding_create (run_from, ev_from, run_to, ev_to, 1);
   sys->bindings = list_insert (sys->bindings, b);
-  return 1;
+
+  /*
+   * Compute closure graph etc.
+   */
+  return closure_graph (b);
 }
 
 //! Remove last additions, including last manual addition
@@ -109,20 +218,12 @@ binding_add (int run_from, int ev_from, int run_to, int ev_to)
 void
 binding_remove_last ()
 {
-  List list;
-  int manual;
-
-  manual = 0;
-  list = sys->bindings;
-
-  while (list != NULL && !manual)
-    {
   Binding b;
 
-      b = (Binding) list->data;
-      manual = b->manual;
+  if (sys->bindings != NULL)
+    {
+      b = (Binding) sys->bindings->data;
       binding_destroy (b);
-      list = list_delete (list);
+      sys->bindings = list_delete (sys->bindings);
     }
-  sys->bindings = list;
 }

src/binding.h

@@ -4,6 +4,8 @@
 void bindingInit (const System mysys);
 void bindingDone ();
 
+int node_count ();
+int node_number (int run, int ev);
 int binding_add (int run_from, int ev_from, int run_to, int ev_to);
 void binding_remove_last ();
 

src/compiler.c

@@ -103,9 +103,10 @@ compilerInit (const System mysys)
 }
 
 //! Make a global constant
-Term makeGlobalConstant (const char *s)
+Term
+makeGlobalConstant (const char *s)
 {
-  return levelDeclare (symbolSysConst(s), 0, 0);
+  return levelDeclare (symbolSysConst (s), 0, 0);
 }
 
 //! Clean up afterwards
@@ -1045,33 +1046,9 @@ compute_prec_sets (const System sys)
 
   /*
    * Compute transitive closure (Warshall).
-   * If j<i and k<j, then k<i.
-   * Could be done more efficiently but that is irrelevant here.
    */
-  i = 0;
-  while (i < size)
-    {
-      j = 0;
-      while (j < size)
-	{
-	  if (prec[index2 (j, i)] == 1)
-	    {
-	      int k;
+  warshall (prec, size);
 
-	      k = 0;
-	      while (k < size)
-		{
-		  if (prec[index2 (k, j)] == 1)
-		    {
-		      prec[index2 (k, i)] = 1;
-		    }
-		  k++;
-		}
-	    }
-	  j++;
-	}
-      i++;
-    }
   // [x] show_matrix ();
 
   /*