- Added switch '--max-of-role' to further restrict state space. Added for comparison testing.

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;
+}

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
    */

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