- Fixed --disable-intruder: it now also uses no tupling shortcuts.

src/arachne.c

@@ -1193,7 +1193,7 @@ bind_goal_new_m0 (const Binding b)
       Termlist subst;
 
       m0t = tl->term;
-      subst = termMguTerm (b->term, m0t);
+      subst = termMguTerm (b->term, m0t);	//! @todo This needs to be replace by the iterator one, but works for now
       if (subst != MGUFAIL)
 	{
 	  int run;
@@ -1296,7 +1296,7 @@ bind_goal_new_encrypt (const Binding b)
     {
       Term t1, t2;
 
-      if (!realTermEncrypt (term))
+      if (switches.intruder && (!realTermEncrypt (term)))
 	{
 	  // tuple construction
 	  error ("Goal that is a tuple should not occur!");
@@ -1407,20 +1407,21 @@ bind_goal_regular_run (const Binding b)
   int flag;
   int found;
 
-  int test_sub_unification (Termlist substlist, Termlist keylist)
-  {
-    // A unification exists; return the signal
-    return 0;
-  }
   /*
    * This is a local function so we have access to goal
    */
   int bind_this_role_send (Protocol p, Role r, Roledef rd, int index)
   {
+    int test_sub_unification (Termlist substlist, Termlist keylist)
+    {
+      // A unification exists; return the signal
+      return false;
+    }
+
     if (p == INTRUDER)
       {
 	// No intruder roles here
-	return 1;
+	return true;
       }
 
     // Test for interm unification
@@ -1437,9 +1438,8 @@ bind_goal_regular_run (const Binding b)
 	eprintf (", index %i\n", index);
       }
 #endif
-    if (!termMguSubTerm
+    if (!subtermUnify
-	(b->term, rd->message, test_sub_unification, sys->know->inverses,
+	(rd->message, b->term, NULL, NULL, test_sub_unification))
-	 NULL))
       {
 	int sflag;
 
@@ -1482,7 +1482,7 @@ bind_goal_regular_run (const Binding b)
       }
     else
       {
-	return 1;
+	return true;
       }
   }
 
@@ -2004,6 +2004,112 @@ select_tuple_goal ()
 }
 
 
+//! Iterate a binding
+/**
+ * For DY model, we unfold any tuples first, otherwise we skip that.
+ */
+int
+iterateOneBinding (void)
+{
+  Binding btup;
+  int flag;
+
+  // marker
+  flag = true;
+
+  // Are there any tuple goals?
+  if (switches.intruder)
+    {
+      // Maybe... (well, test)
+      btup = select_tuple_goal ();
+    }
+  else
+    {
+      // No, there are non that need to be expanded (no intruder)
+      btup = NULL;
+    }
+  if (btup != NULL)
+    {
+      /* Substitution or something resulted in a tuple goal: we immediately split them into compounds.
+       */
+      Term tuple;
+
+      tuple = deVar (btup->term);
+      if (realTermTuple (tuple))
+	{
+	  int count;
+	  Term tupletermbuffer;
+
+	  tupletermbuffer = btup->term;
+	  /*
+	   * We solve this by replacing the tuple goal by the left term, and adding a goal for the right term.
+	   */
+	  btup->term = TermOp1 (tuple);
+	  count =
+	    goal_add (TermOp2 (tuple), btup->run_to,
+		      btup->ev_to, btup->level);
+
+	  // Show this in output
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf ("Expanding tuple goal ");
+	      termPrint (tupletermbuffer);
+	      eprintf (" into %i subgoals.\n", count);
+	    }
+
+	  // iterate
+	  flag = iterate ();
+
+	  // undo
+	  goal_remove_last (count);
+	  btup->term = tupletermbuffer;
+	}
+    }
+  else
+    {
+      // No tuple goals; good
+      Binding b;
+
+		  /**
+		   * Not pruned: count
+		   */
+
+      sys->states = statesIncrease (sys->states);
+      sys->current_claim->states =
+	statesIncrease (sys->current_claim->states);
+
+		  /**
+		   * Check whether its a final state (i.e. all goals bound)
+		   */
+
+      b = (Binding) select_goal (sys);
+      if (b == NULL)
+	{
+	  /*
+	   * all goals bound, check for property
+	   */
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf ("All goals are now bound.\n");
+	    }
+	  sys->claims = statesIncrease (sys->claims);
+	  sys->current_claim->count =
+	    statesIncrease (sys->current_claim->count);
+	  flag = property_check (sys);
+	}
+      else
+	{
+	  /*
+	   * bind this goal in all possible ways and iterate
+	   */
+	  flag = bind_goal_all_options (b);
+	}
+    }
+  return flag;
+}
+
 //! Main recursive procedure for Arachne
 int
 iterate ()
@@ -2018,89 +2124,8 @@ iterate ()
 	{
 	  if (!prune_bounds (sys))
 	    {
-	      Binding btup;
+	      // Go and pick a binding for iteration
-
+	      flag = iterateOneBinding ();
-	      // Are there any tuple goals?
-	      btup = select_tuple_goal ();
-	      if (btup != NULL)
-		{
-		  /* Substitution or something resulted in a tuple goal: we immediately split them into compounds.
-		   */
-		  Term tuple;
-
-		  tuple = deVar (btup->term);
-		  if (realTermTuple (tuple))
-		    {
-		      int count;
-		      Term tupletermbuffer;
-
-		      tupletermbuffer = btup->term;
-		      /*
-		       * We solve this by replacing the tuple goal by the left term, and adding a goal for the right term.
-		       */
-		      btup->term = TermOp1 (tuple);
-		      count =
-			goal_add (TermOp2 (tuple), btup->run_to,
-				  btup->ev_to, btup->level);
-
-		      // Show this in output
-		      if (switches.output == PROOF)
-			{
-			  indentPrint ();
-			  eprintf ("Expanding tuple goal ");
-			  termPrint (tupletermbuffer);
-			  eprintf (" into %i subgoals.\n", count);
-			}
-
-		      // iterate
-		      flag = iterate ();
-
-		      // undo
-		      goal_remove_last (count);
-		      btup->term = tupletermbuffer;
-		    }
-		}
-	      else
-		{
-		  // No tuple goals; good
-		  Binding b;
-
-		  /**
-		   * Not pruned: count
-		   */
-
-		  sys->states = statesIncrease (sys->states);
-		  sys->current_claim->states =
-		    statesIncrease (sys->current_claim->states);
-
-		  /**
-		   * Check whether its a final state (i.e. all goals bound)
-		   */
-
-		  b = (Binding) select_goal (sys);
-		  if (b == NULL)
-		    {
-		      /*
-		       * all goals bound, check for property
-		       */
-		      if (switches.output == PROOF)
-			{
-			  indentPrint ();
-			  eprintf ("All goals are now bound.\n");
-			}
-		      sys->claims = statesIncrease (sys->claims);
-		      sys->current_claim->count =
-			statesIncrease (sys->current_claim->count);
-		      flag = property_check (sys);
-		    }
-		  else
-		    {
-		      /*
-		       * bind this goal in all possible ways and iterate
-		       */
-		      flag = bind_goal_all_options (b);
-		    }
-		}
 	    }
 	  else
 	    {

src/binding.c

@@ -234,8 +234,9 @@ goal_add (Term term, const int run, const int ev, const int level)
     error
       ("Trying to add a goal for an event that is not in the semistate yet.");
 #endif
-  if (realTermTuple (term))
+  if (switches.intruder && realTermTuple (term))
     {
+      // Only split if there is an intruder
       return goal_add (TermOp1 (term), run, ev, level) +
 	goal_add (TermOp2 (term), run, ev, level);
     }
@@ -459,7 +460,16 @@ unique_origination ()
 		    {
 		      Termlist terms2, sharedterms;
 
-		      terms2 = tuple_to_termlist (b2->term);
+		      if (switches.intruder)
+			{
+			  // For intruder we work with sets here
+			  terms2 = tuple_to_termlist (b2->term);
+			}
+		      else
+			{
+			  // For regular agents we use terms
+			  terms2 = termlistAdd (NULL, b2->term);
+			}
 		      sharedterms = termlistConjunct (terms, terms2);
 
 		      // Compare terms
@@ -529,11 +539,22 @@ bindings_c_minimal ()
 		      {
 			// this node is *before* the from node
 			Roledef rd;
+			int occursthere;
 
 			rd = roledef_shift (sys->runs[run].start, ev);
-			if (termInTerm (rd->message, b->term))
+			if (switches.intruder)
 			  {
-			    // This term already occurs as interm in a previous node!
+			    // intruder: interm bindings should cater for the first occurrence
+			    occursthere = termInTerm (rd->message, b->term);
+			  }
+			else
+			  {
+			    // no intruder, then simple test
+			    occursthere = isTermEqual (rd->message, b->term);
+			  }
+			if (occursthere)
+			  {
+			    // This term already occurs in a previous node!
 #ifdef DEBUG
 			    if (DEBUGL (4))
 			      {

src/mgu.c

@@ -7,6 +7,7 @@
 #include "type.h"
 #include "debug.h"
 #include "specialterm.h"
+#include "switches.h"
 
 /*
    Most General Unifier
@@ -123,15 +124,12 @@ termlistSubstReset (Termlist tl)
 int
 unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
 {
-  int proceed;
-
-  proceed = true;
   /* added for speed */
   t1 = deVar (t1);
   t2 = deVar (t2);
   if (t1 == t2)
     {
-      return proceed && callback (tl);
+      return callback (tl);
     }
 
   int callsubst (Termlist tl, Term t, Term tsubst)
@@ -155,12 +153,12 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
       if (isTermEqual (t1, t2))
 	{
 	  // Equal!
-	  return proceed && callback (tl);
+	  return callback (tl);
 	}
       else
 	{
 	  // Can never be fixed, no variables
-	  return proceed;
+	  return true;
 	}
     }
 
@@ -188,7 +186,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
 	  t1 = t2;
 	  t2 = t3;
 	}
-      return proceed && callsubst (tl, t1, t2);
+      return callsubst (tl, t1, t2);
     }
 
   /* symmetrical tests for single variable.
@@ -197,25 +195,25 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
   if (realTermVariable (t2))
     {
       if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
-	return proceed;
+	return true;
       else
 	{
-	  return proceed && callsubst (tl, t2, t1);
+	  return callsubst (tl, t2, t1);
 	}
     }
   if (realTermVariable (t1))
     {
       if (termSubTerm (t2, t1) || !goodsubst (t1, t2))
-	return proceed;
+	return true;
       else
 	{
-	  return proceed && callsubst (tl, t1, t2);
+	  return callsubst (tl, t1, t2);
 	}
     }
 
   /* left & right are compounds with variables */
   if (t1->type != t2->type)
-    return proceed;
+    return true;
 
   /* identical compound types */
 
@@ -229,8 +227,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
 	return unify (TermOp (t1), TermOp (t2), tl, callback);
       }
 
-      return proceed
+      return unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
-	&& unify (TermKey (t1), TermKey (t2), tl, unify_combined_enc);
     }
 
   /* tupling second
@@ -243,11 +240,10 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist))
 	// and we try the inner terms
 	return unify (TermOp2 (t1), TermOp2 (t2), tl, callback);
       }
-      return proceed
+      return unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
-	&& unify (TermOp1 (t1), TermOp1 (t2), tl, unify_combined_tup);
     }
 
-  return proceed;
+  return true;
 }
 
 
@@ -286,24 +282,28 @@ subtermUnify (Term tbig, Term tsmall, Termlist tl, Termlist keylist,
   proceed = proceed && unify (tbig, tsmall, tl, keycallback);
 
   // [2/3]: complex
-  // 2. interm unification
+  if (switches.intruder)
-  if (realTermTuple (tbig))
     {
-      proceed = proceed
+      // 2. interm unification
-	&& subtermUnify (TermOp1 (tbig), tsmall, tl, keylist, callback);
+      // Only if there is an intruder
-      proceed = proceed
+      if (realTermTuple (tbig))
-	&& subtermUnify (TermOp2 (tbig), tsmall, tl, keylist, callback);
+	{
-    }
+	  proceed = proceed
+	    && subtermUnify (TermOp1 (tbig), tsmall, tl, keylist, callback);
+	  proceed = proceed
+	    && subtermUnify (TermOp2 (tbig), tsmall, tl, keylist, callback);
+	}
 
-  // 3. unification with encryption needed
+      // 3. unification with encryption needed
-  if (realTermEncrypt (tbig))
+      if (realTermEncrypt (tbig))
-    {
+	{
-      // extend the keylist
+	  // extend the keylist
-      keylist = termlistAdd (keylist, tbig);
+	  keylist = termlistAdd (keylist, tbig);
-      proceed = proceed
+	  proceed = proceed
-	&& subtermUnify (TermOp (tbig), tsmall, tl, keylist, callback);
+	    && subtermUnify (TermOp (tbig), tsmall, tl, keylist, callback);
-      // remove last item again
+	  // remove last item again
-      keylist = termlistDelTerm (keylist);
+	  keylist = termlistDelTerm (keylist);
+	}
     }
   return proceed;
 }