From 139f93746da60877219f8d7997320dadc812e6b4 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Fri, 26 Jan 2007 15:31:49 +0000
Subject: [PATCH] - Added switch '--max-of-role' to further restrict state
 space. Added for comparison testing.

---
 src/prune_bounds.c | 56 ++++++++++++++++++++++++++++++++++++++++++++++
 src/switches.c     | 27 ++++++++++++++++++++++
 src/switches.h     |  1 +
 3 files changed, 84 insertions(+)

diff --git a/src/prune_bounds.c b/src/prune_bounds.c
index 0e7e93d..0d933bc 100644
--- a/src/prune_bounds.c
+++ b/src/prune_bounds.c
@@ -14,6 +14,7 @@
 #include "timer.h"
 #include "arachne.h"
 #include "system.h"
+#include "termmap.h"
 #include "cost.h"
 
 extern int attack_length;
@@ -22,6 +23,9 @@ extern Protocol INTRUDER;
 extern int proofDepth;
 extern int max_encryption_level;
 
+//! Forward declarations
+int tooManyOfRole (const System sys);
+
 //! Prune determination for bounds
 /**
  * When something is pruned here, the state space is not complete anymore.
@@ -104,6 +108,7 @@ prune_bounds (const System sys)
 	}
     }
 
+  /* prune for runs */
   if (sys->num_regular_runs > switches.runs)
     {
       // Hardcoded limit on runs
@@ -116,6 +121,17 @@ prune_bounds (const System sys)
       return 1;
     }
 
+  /* prune for role instances max */
+  if (tooManyOfRole (sys))
+    {
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf ("Pruned: too many instances of a particular role.\n");
+	}
+      return 1;
+    }
+
   // This needs some foundation. Probably * 2^max_encryption_level
   //!@todo Remove later
   /**
@@ -207,3 +223,43 @@ prune_bounds (const System sys)
   // No pruning because of bounds
   return 0;
 }
+
+//! Detect when there are too many instances of a certain role
+int
+tooManyOfRole (const System sys)
+{
+  int toomany;
+
+  toomany = false;
+  if (switches.maxOfRole > 0)
+    {
+      Termmap f;
+      int run;
+
+      f = NULL;
+      for (run = 0; run < sys->maxruns; run++)
+	{
+	  if (sys->runs[run].protocol != INTRUDER)
+	    {
+	      // maybe this conflicts with equal protocols...? TODO
+	      Term role;
+	      int count;
+
+	      role = sys->runs[run].role->nameterm;
+	      count = termmapGet (f, role);
+	      if (count == -1)
+		count = 1;
+	      else
+		count++;
+	      f = termmapSet (f, role, count);
+	      if (count > switches.maxOfRole)
+		{
+		  toomany = true;
+		  break;
+		}
+	    }
+	}
+      termmapDelete (f);
+    }
+  return toomany;
+}
diff --git a/src/switches.c b/src/switches.c
index ad8c86b..7f3eae1 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -53,6 +53,7 @@ switchesInit (int argc, char **argv)
   switches.filterProtocol = NULL;	// default check all claims
   switches.filterLabel = NULL;	// default check all claims
   switches.maxAttacks = 0;	// no maximum default
+  switches.maxOfRole = 0;	// no maximum default
 
   // Arachne
   switches.heuristic = 162;	// default goal selection method
@@ -1084,6 +1085,32 @@ switcher (const int process, int index, int commandline)
 	}
     }
 
+  if (detect (' ', "max-of-role", 1))
+    {
+      if (!process)
+	{
+	  if (switches.expert)
+	    {
+	      helptext ("    --max-of-role=<int>",
+			"maximum number of instances of each role [inf]");
+	    }
+	}
+      else
+	{
+	  int arg = integer_argument ();
+	  if (arg == 0)
+	    {
+	      switches.maxOfRole = 0;
+	    }
+	  else
+	    {
+	      switches.maxOfRole = arg;
+	    }
+	  return index;
+	}
+    }
+
+
   /* ==================
    *  Misc switches
    */
diff --git a/src/switches.h b/src/switches.h
index 0ec61ef..a7730a6 100644
--- a/src/switches.h
+++ b/src/switches.h
@@ -26,6 +26,7 @@ struct switchdata
   char *filterProtocol;		//!< Which claim should be checked?
   char *filterLabel;		//!< Which claim should be checked?
   int maxAttacks;		//!< When not 0, maximum number of attacks
+  int maxOfRole;		//!< When not 0, maximum number of instances of each unique (non intruder) role
 
   // Arachne
   int heuristic;		//!< Goal selection method for Arachne engine