- Added '--extravert' switch, which avoids initiator Alice to talk to

Alice.

src/arachne.c

@@ -2888,6 +2888,50 @@ prune_theorems ()
       run++;
     }
 
+  // Prune if any initiator run talks to itself
+  /**
+   * This effectively disallows Alice from talking to Alice, for all
+   * initiators. We still allow it for responder runs, because we assume the
+   * responder is not checking this.
+   */
+  if (switches.extravert)
+    {
+      int run;
+
+      run = 0;
+      while (run < sys->maxruns)
+	{
+	  // Check this run only if it is an initiator role
+	  if (sys->runs[run].role->initiator)
+	    {
+	      // Check this initiator run
+	      Termlist tl;
+
+	      tl = sys->runs[run].agents;
+	      while (tl != NULL)
+		{
+		  Termlist tlscan;
+
+		  tlscan = tl->next;
+		  while (tlscan != NULL)
+		    {
+		      if (isTermEqual (tl->term, tlscan->term))
+			{
+			  // XXX TODO
+			  // Still need to fix proof output for this
+			  //
+			  // Pruning because some agents are equal for this role.
+			  return 1;
+			}
+		      tlscan = tlscan->next;
+		    }
+		  tl = tl->next;
+		}
+	      run++;
+	    }
+	}
+    }
+
   // Prune wrong agents type for initators
   if (!initiatorAgentsType ())
     {

src/switches.c

@@ -68,6 +68,7 @@ switchesInit (int argc, char **argv)
   switches.maxIntruderActions = INT_MAX;	// max number of encrypt/decrypt events
   switches.agentTypecheck = 1;	// default do check agent types
   switches.concrete = true;	// default removes symbols, and makes traces concrete
+  switches.extravert = false;	// default allows also initiator Alice to talk to Alice
 
   // Misc
   switches.switchP = 0;		// multi-purpose parameter
@@ -560,6 +561,22 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect (' ', "extravert", 0))
+    {
+      if (!process)
+	{
+	  /* discourage: hide
+	   *
+	   * Finds only attacks which exclude initiator Alice talking to Alice
+	   */
+	}
+      else
+	{
+	  switches.extravert = true;
+	  return index;
+	}
+    }
+
   if (detect (' ', "extend-trivial", 0))
     {
       if (!process)

src/switches.h

@@ -47,6 +47,7 @@ struct switchdata
   int maxIntruderActions;	//!< Maximum number of intruder actions in the semitrace (encrypt/decrypt)
   int agentTypecheck;		//!< Check type of agent variables in all matching modes
   int concrete;			//!< Swap out variables at the end.
+  int extravert;		//!< Disallow Alice talking to Alice
 
   // Misc
   int switchP;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.