From e104dddbfbb9463eaebd1ca8c97201a694b590e8 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Sun, 21 Aug 2005 21:38:32 +0000
Subject: [PATCH] - Added a switch to number the limit of intruder actions.  
 Initial testing suggests it does not influence the number of states   much
 for values of 2 and higher.

---
 src/arachne.c  | 42 ++++++++++++++++++++++++++++++++++++++++++
 src/switches.c | 14 ++++++++++++++
 src/switches.h |  1 +
 3 files changed, 57 insertions(+)

diff --git a/src/arachne.c b/src/arachne.c
index 35a8757..b931846 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -549,6 +549,31 @@ first_selectable_goal (List bl)
   return bl;
 }
 
+//! Count intruder events
+int
+countIntruderActions ()
+{
+  int count;
+  int run;
+
+  count = 0;
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (sys->runs[run].protocol == INTRUDER)
+	{
+	  // Only intruder roles
+	  if (sys->runs[run].role != I_M)
+	    {
+	      // The M_0 (initial knowledge) events don't count.
+	      count++;
+	    }
+	}
+      run++;
+    }
+  return count;
+}
+
 //------------------------------------------------------------------------
 // Proof reporting
 //------------------------------------------------------------------------
@@ -3098,6 +3123,23 @@ prune_bounds ()
   if (enoughAttacks (sys))
     return 1;
 
+  // Limit on intruder events count
+  if (switches.maxIntruderActions < INT_MAX)
+    {
+      // Only check if actually used
+      if (countIntruderActions () > switches.maxIntruderActions)
+	{
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned: more than %i encrypt/decrypt events in the semitrace.\n",
+		 switches.maxIntruderActions);
+	    }
+	  return 1;
+	}
+    }
+
   // No pruning because of bounds
   return 0;
 }
diff --git a/src/switches.c b/src/switches.c
index be1b581..ada0167 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -65,6 +65,7 @@ switchesInit (int argc, char **argv)
 
   // Arachne
   switches.arachneSelector = 3;	// default goal selection method
+  switches.maxIntruderActions = INT_MAX;	// max number of encrypt/decrypt events
 
   // Misc
   switches.switchP = 0;		// multi-purpose parameter
@@ -543,6 +544,19 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect (' ', "intruder-actions", 1))
+    {
+      if (!process)
+	{
+	  /* fairly technical, untested pruning */
+	}
+      else
+	{
+	  switches.maxIntruderActions = integer_argument ();
+	  return index;
+	}
+    }
+
   /* ==================
    *  External options
    */
diff --git a/src/switches.h b/src/switches.h
index bd994b3..ecd5764 100644
--- a/src/switches.h
+++ b/src/switches.h
@@ -44,6 +44,7 @@ struct switchdata
 
   // Arachne
   int arachneSelector;		//!< Goal selection method for Arachne engine
+  int maxIntruderActions;	//!< Maximum number of intruder actions in the semitrace (encrypt/decrypt)
 
   // Misc
   int switchP;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.