- Revisited type matching conditions.

- Introduced tuple unfolding stuff for Arachne. -m2 should work now.

src/arachne.c

@@ -1298,7 +1298,7 @@ select_tuple_goal()
 
       b = (Binding) bl->data;
       // Ignore done stuff
-      if (!b->done)
+      if (!b->blocked && !b->done)
 	{
 	  if (isTermTuple (b->term))
 	    {
@@ -1352,8 +1352,8 @@ select_goal ()
 
       b = (Binding) bl->data;
 
-      // Ignore singular variables
+      // Only if not done and not blocked
-      if (!b->done)
+      if (!b->blocked && !b->done)
 	{
 	  int allow;
 	  Term gterm;
@@ -1773,6 +1773,10 @@ bind_goal_old_intruder_run (Binding b)
 int
 bind_goal (const Binding b)
 {
+  if (b->blocked)
+    {
+      error ("Trying to bind a blocked goal!");
+    }
   if (!b->done)
     {
       int flag;
@@ -1861,6 +1865,7 @@ prune_theorems ()
 	      error ("Agent of run %i is NULL", run);
 	    }
 	  if (!realTermLeaf (agent)
+	      || agent->stype == NULL
 	      || (agent->stype != NULL
 		  && !inTermlist (agent->stype, TERM_Agent)))
 	    {
@@ -1988,8 +1993,10 @@ prune_theorems ()
 	}
 
       // Check for encryption levels
-      if (sys->match < 2
+      /*
-	  && (term_encryption_level (b->term) > max_encryption_level))
+       * if (sys->match < 2
+       */
+      if (term_encryption_level (b->term) > max_encryption_level)
 	{
 	  // Prune: we do not need to construct such terms
 	  if (sys->output == PROOF)
@@ -2274,29 +2281,27 @@ iterate ()
 		{
 		  // Expand tuple goal
 		  int count;
-		  Term tt;
 	
+		  // mark as blocked for iteration
+		  binding_block (b);
+		  // simply adding will detect the tuple and add the new subgoals
+		  count = goal_add (b->term, b->run_to, b->ev_to, b->level);
+
 		  // Show this in output
 		  if (sys->output == PROOF)
 		    {
 		      indentPrint ();
 		      eprintf ("Expanding tuple goal ");
 		      termPrint (b->term);
-		      eprintf ("\n");
+		      eprintf (" into %i subgoals.\n", count);
 		    }
 
-		  // mark as done for iteration
-		  b->done = 1;
-
-		  // simply adding will detect the tuple and add the new subgoals
-		  count = goal_add (b->term, b->run_to, b->ev_to, b->level);
-
 		  // iterate
 		  flag = iterate ();
 
 		  // undo
   		  goal_remove_last (count);
-		  b->done = 0;
+		  binding_unblock (b);
 		}
 	      else
 		{

src/binding.c

@@ -42,6 +42,7 @@ binding_create (Term term, int run_to, int ev_to)
 
   b = memAlloc (sizeof (struct binding));
   b->done = 0;
+  b->blocked = 0;
   b->run_from = -1;
   b->ev_from = -1;
   b->run_to = run_to;
@@ -179,7 +180,7 @@ goal_graph_create ()
 	  Binding b;
 
 	  b = (Binding) bl->data;
-	  if (b->done)
+	  if (valid_binding (b))
 	    {
 #ifdef DEBUG
 	      if (graph_nodes
@@ -417,6 +418,8 @@ binding_print (const Binding b)
     eprintf ("Unbound --( ");
   termPrint (b->term);
   eprintf (" )->> (%i,%i)", b->run_to, b->ev_to);
+  if (b->blocked)
+    eprintf ("[blocked]");
   return 1;
 }
 
@@ -444,24 +447,9 @@ goal_add (Term term, const int run, const int ev, const int level)
 #endif
   if (realTermTuple (term))
     {
-      int width;
+      sum = sum + 
-      int flag;
+	  goal_add (TermOp1 (term), run, ev, level) + 
-      int i;
+	  goal_add (TermOp2 (term), run, ev, level);
-
-      flag = 1;
-      width = tupleCount (term);
-      i = 0;
-      while (i < width)
-	{
-	  sum = sum + goal_add (tupleProject (term, i), run, ev, level);
-	  if (i > 0)
-	    {
-	      Binding b;
-
-	      b = (Binding) sys->bindings->data;
-	    }
-	  i++;
-	}
     }
   else
     {
@@ -516,6 +504,10 @@ goal_remove_last (int n)
 int
 goal_bind (const Binding b, const int run, const int ev)
 {
+  if (b->blocked)
+    {
+      error ("Trying to bind a blocked goal.");
+    }
   if (!b->done)
     {
 #ifdef DEBUG
@@ -525,7 +517,7 @@ goal_bind (const Binding b, const int run, const int ev)
       b->done = 1;
       b->run_from = run;
       b->ev_from = ev;
-      goal_graph_create (b);
+      goal_graph_create ();
       return warshall (graph, nodes);
     }
   else
@@ -549,6 +541,37 @@ goal_unbind (const Binding b)
     }
 }
 
+//! Bind a goal as a dummy (block)
+/**
+ * Especially made for tuple expansion
+ */
+int binding_block (Binding b)
+{
+  if (!b->blocked)
+    {
+      b->blocked = 1;
+      return 1;
+    }
+  else
+    {
+      error ("Trying to block a goal again.");
+    }
+}
+
+//! Unblock a binding
+int binding_unblock (Binding b)
+{
+  if (b->blocked)
+    {
+      b->blocked = 0;
+      return 1;
+    }
+  else
+    {
+      error ("Trying to unblock a non-blocked goal.");
+    }
+}
+
 //! Determine whether some label set is ordered w.r.t. send/read order.
 /**
  * Assumes all these labels exist in the system, within length etc, and that the run mappings are valid.
@@ -606,6 +629,15 @@ labels_ordered (Termmap runs, Termlist labels)
   return 1;
 }
 
+//! Check whether the binding denotes a sensible thing such that we can use run_from and ev_from
+int valid_binding (Binding b)
+{
+  if (b->done && !b->blocked)
+      return 1;
+  else
+      return 0;
+}
+
 //! Prune invalid state w.r.t. <=C minimal requirement
 /**
  * Intuition says this can be done a lot more efficient. Luckily this is the prototype.
@@ -636,7 +668,8 @@ bindings_c_minimal ()
       Binding b;
 
       b = (Binding) bl->data;
-      if (b->done)
+      // Check for a valid binding; it has to be 'done' and sensibly bound (not as in tuple expanded stuff)
+      if (valid_binding(b))
 	{
 	  int run;
 	  int node_from;

src/binding.h

@@ -11,6 +11,7 @@
 struct binding
 {
   int done;			//!< Iff true, it is bound
+  int blocked;			//!< Iff true, ignore it
 
   int run_from;
   int ev_from;
@@ -39,11 +40,14 @@ void goal_graph_create ();
 
 
 int binding_print (Binding b);
+int valid_binding (Binding b);
 
 int goal_add (Term term, const int run, const int ev, const int level);
 void goal_remove_last (int n);
 int goal_bind (const Binding b, const int run, const int ev);
 void goal_unbind (const Binding b);
+int binding_block (Binding b);
+int binding_unblock (Binding b);
 int labels_ordered (Termmap runs, Termlist labels);
 
 int bindings_c_minimal ();

src/compiler.c

@@ -57,7 +57,6 @@ Term TERM_Function;
 Term TERM_Hidden;
 Term TERM_Type;
 Term TERM_Nonce;
-Term TERM_Agent;
 
 Term TERM_Claim;
 Term CLAIM_Secret;

src/mgu.c

@@ -58,7 +58,36 @@ showSubst (Term t)
 __inline__ int
 goodsubst (Term tvar, Term tsubst)
 {
-  if (tvar->stype == NULL || (mgu_match == 2))
+  // function to test compatibility
+  __inline__ int compatibleTypes ()
+    {
+      if (tvar->stype == NULL)
+	{
+	  // If the variable type is unspecified, anything goes
+	  return 1;
+	}
+      else
+	{
+	  // There are variable types.
+	  // At least one of them should match a type of the constant.
+	  Termlist tl;
+
+	  tl = tvar->stype;
+	  while (tl != NULL)
+	    {
+	      if (inTermlist (tsubst->stype, tl->term))
+		{
+		  // One type matches
+		  return 1;
+		}
+	      tl = tl->next;
+	    }
+	  // No matches
+	  return 0;
+	}
+    }
+
+  if (mgu_match == 2)
     {
       return 1;
     }
@@ -76,7 +105,7 @@ goodsubst (Term tvar, Term tsubst)
 	{
 	  // It's a leaf, but what type?
 	  if (mgu_match == 1
-	      || termlistContained (tvar->stype, tsubst->stype))
+	      || compatibleTypes ())
 	    {
 	      return 1;
 	    }

src/system.c

@@ -18,6 +18,7 @@
 
 /* from compiler.o */
 extern Term TERM_Type;
+extern Term TERM_Agent;
 
 //! Global flag that signals LaTeX output.
 /**
@@ -708,11 +709,17 @@ roleInstanceArachne (const System sys, const Protocol protocol,
 	      
 	      // Flag this
 	      newt->roleVar = 1;
+	      newt->stype = termlistAddNew (newt->stype, TERM_Agent);
 
 	      // maybe add choose?
 	      // Note that for anything but full type flaws, this is not an issue.
 	      // In the POR reduction, force choose was the default. Here it is not.
-	      if (not_read_first (rd, oldt) && sys->match == 2)
+	      /*
+	       * [x]
+	       * TODO currently disabled: something weird was goind on causing weird prunes,
+	       * for match=2. Investigate later.
+	       */
+	      if (0 && not_read_first (rd, oldt) && sys->match == 2)
 		{
 		  /* this term is forced as a choose, or it does not occur in the (first) read event */
 		  if (extterm == NULL)

src/term.h

@@ -26,7 +26,7 @@ struct term
   int type;
   //! Data Type termlist (e.g. agent or nonce)
   /** Only for leaves. */
-  void *stype;
+  void *stype;			// list of types
   int roleVar;			// only for leaf, arachne engine: role variable flag
 
   //! Substitution term.