From 1ee77472a05343d03f8f5b060c88a8be6da7dc1e Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 15 Aug 2005 12:49:32 +0000
Subject: [PATCH] - --max-attacks=AnyGijsNumber.

---
 src/arachne.c      |  8 ++++++++
 src/modelchecker.c | 16 ++++++++++++----
 src/switches.c     | 16 ++++++++++++++++
 src/switches.h     |  1 +
 src/system.c       | 20 ++++++++++++++++++--
 5 files changed, 55 insertions(+), 6 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index c8e7c4c..35a8757 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -3094,6 +3094,10 @@ prune_bounds ()
       return 1;
     }
 
+  // Limit on attack count
+  if (enoughAttacks (sys))
+    return 1;
+
   // No pruning because of bounds
   return 0;
 }
@@ -3192,6 +3196,10 @@ property_check ()
 
   flag = 1;
 
+  /* Do we need any? */
+  if (enoughAttacks (sys))
+    return flag;
+
   /**
    * By the way the claim is handled, this automatically means a flaw.
    */
diff --git a/src/modelchecker.c b/src/modelchecker.c
index 612f61c..09dd446 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -177,6 +177,10 @@ executeStep (const System sys, const int run)
   if (!sys->explore)
     return 0;
 
+  /* prune (exit) if enough attacks found */
+  if (enoughAttacks (sys))
+    return 0;
+
   /* we want to explore it, but are we allowed by pruning? */
   if (sys->step >= sys->maxtracelength)
     {
@@ -260,7 +264,7 @@ removeDangling (Roledef rd, const int killclaims)
 Roledef
 removeIrrelevant (const System sys, const int run, Roledef rd)
 {
-  if (!isRunTrusted (sys,run))
+  if (!isRunTrusted (sys, run))
     {
       // untrusted, so also remove claims
       return removeDangling (rd, 1);
@@ -384,7 +388,7 @@ explorify (const System sys, const int run)
 	  while (rid < sys->maxruns)
 	    {
 	      /* are claims in this run evaluated anyway? */
-	      if (isRunTrusted(sys, rid))
+	      if (isRunTrusted (sys, rid))
 		{		/* possibly claims to be checked in this run */
 		  rdscan = runPointerGet (sys, rid);
 		  while (rdscan != NULL)
@@ -1207,7 +1211,7 @@ claimViolationDetails (const System sys, const int run, const Roledef rd,
     {
       /* secrecy claim */
 
-      if (!isRunTrusted (sys,run))
+      if (!isRunTrusted (sys, run))
 	{
 	  /* claim was skipped */
 	  return (Termlist) - 1;
@@ -1236,6 +1240,10 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
   /* default = no adaption of pruning, continue search */
   flag = 1;
 
+  /* enough? */
+  if (enoughAttacks (sys))
+    return flag;
+
   /* Count the violations */
   sys->attackid++;
   sys->failed = statesIncrease (sys->failed);
@@ -1328,7 +1336,7 @@ executeTry (const System sys, int run)
       if (runPoint->type == CLAIM)
 	{
 	  /* first we might dynamically determine whether the claim is valid */
-	  if (!isRunTrusted (sys,run))
+	  if (!isRunTrusted (sys, run))
 	    {
 	      /* for untrusted agents we check no claim violations at all
 	       * so: we know it's okay. */
diff --git a/src/switches.c b/src/switches.c
index b6ef9a3..be1b581 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -47,6 +47,7 @@ switchesInit (int argc, char **argv)
   switches.maxtracelength = INT_MAX;
   switches.runs = INT_MAX;
   switches.filterClaim = NULL;	// default check all claims
+  switches.maxAttacks = 0;	// no maximum default
 
   // Modelchecker
   switches.traverse = 12;	// default traversal method
@@ -350,6 +351,21 @@ switcher (const int process, int index)
 	}
     }
 
+  if (detect (' ', "max-attacks", 1))
+    {
+      if (!process)
+	{
+	  /* not very important
+	     helptext ("--max-attacks=<int>", "when not 0, maximum number of attacks [0]");
+	   */
+	}
+      else
+	{
+	  switches.maxAttacks = integer_argument ();
+	  return index;
+	}
+    }
+
   if (detect ('p', "prune", 1))
     {
       if (!process)
diff --git a/src/switches.h b/src/switches.h
index 22a895d..bd994b3 100644
--- a/src/switches.h
+++ b/src/switches.h
@@ -26,6 +26,7 @@ struct switchdata
   int maxtracelength;		//!< Maximum trace length allowed
   int runs;			//!< The number of runs as in the switch
   Term filterClaim;		//!< Which claim should be checked?
+  int maxAttacks;		//!< When not 0, maximum number of attacks
 
   // Modelchecker
   int traverse;			//!< Traversal method
diff --git a/src/system.c b/src/system.c
index 0bda593..de0bb3c 100644
--- a/src/system.c
+++ b/src/system.c
@@ -69,7 +69,7 @@ systemInit ()
   sys->untrusted = NULL;
   sys->secrets = NULL;		// list of claimed secrets
   sys->synchronising_labels = NULL;
-  sys->attack = NULL;
+  sys->attack = NULL;		// clash with prev. attack declaration TODO
   /* no protocols => no protocol preprocessed */
   sys->rolecount = 0;
   sys->roleeventmax = 0;
@@ -1216,7 +1216,7 @@ protocolsPrint (Protocol p)
 /**
  * 1 (True) means trusted, 0 is untrusted
  */
-int 
+int
 isAgentTrusted (const System sys, Term agent)
 {
   agent = deVar (agent);
@@ -1463,3 +1463,19 @@ system_iterate_roles (const System sys, int (*func) ())
   return 1;
 }
 
+//! Determine whether we don't need any more attacks
+/**
+ * Returns 1 (true) iff no more attacks are needed.
+ */
+int
+enoughAttacks (const System sys)
+{
+  if (switches.maxAttacks != 0)
+    {
+      if (sys->attackid >= switches.maxAttacks)
+	{
+	  return 1;
+	}
+    }
+  return 0;
+}