From d8414daf95faddb83713b9d96094d60e7dca9769 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Thu, 23 Nov 2006 10:40:10 +0000
Subject: [PATCH] - Fixed bug in new --max-attacks semantics.

---
 src/prune_bounds.c |  4 ++--
 src/switches.c     | 17 ++++++++++++-----
 src/system.c       | 10 +++++++---
 3 files changed, 21 insertions(+), 10 deletions(-)

diff --git a/src/prune_bounds.c b/src/prune_bounds.c
index 14b0aa5..2b6ceed 100644
--- a/src/prune_bounds.c
+++ b/src/prune_bounds.c
@@ -45,10 +45,10 @@ prune_bounds (const System sys)
       return 1;
     }
 
-  /* prune for number of attacks */
+  /* prune for number of attacks if we are actually outputting them */
   if (enoughAttacks (sys))
     {
-      // Oh no, we ran out of time!
+      // Oh no, we ran out of possible attacks!
       if (switches.output == PROOF)
 	{
 	  indentPrint ();
diff --git a/src/switches.c b/src/switches.c
index e29cb7c..f662104 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -762,6 +762,13 @@ switcher (const int process, int index, int commandline)
 	{
 	  /* not very important
 	     helptext ("    --prune=<int>", "pruning method when an attack is found [2]");
+
+	     Semantics:
+	     0 - Show all attacks (up to the maximum)
+	     1 - Show first attack
+	     2 - Show 'best' attack (use heuristics)
+
+	     Thus, a value of '0' means multiple attacks are output, otherwise just one.
 	   */
 	}
       else
@@ -1179,14 +1186,14 @@ switcher (const int process, int index, int commandline)
 	  printf ("'%s' model checker for security protocols.\n", progname);
 	  printf ("Version %s.\n", RELEASEVERSION);
 	  if (switches.expert)
-	  {
+	    {
 #ifdef DEBUG
-	  printf ("Revision %s, compiled with debugging support.\n",
-		  SVNVERSION);
+	      printf ("Revision %s, compiled with debugging support.\n",
+		      SVNVERSION);
 #else
-	  printf ("Revision %s\n", SVNVERSION);
+	      printf ("Revision %s\n", SVNVERSION);
 #endif
-	  }
+	    }
 	  printf ("Code by Cas Cremers\n");
 	  exit (0);
 	}
diff --git a/src/system.c b/src/system.c
index f4364f5..109ac2d 100644
--- a/src/system.c
+++ b/src/system.c
@@ -1202,11 +1202,15 @@ scenarioPrint (const System sys)
 int
 enoughAttacks (const System sys)
 {
-  if (switches.maxAttacks != 0)
+  // Only if we are outputting more than one
+  if (switches.prune == 0)
     {
-      if (sys->attackid >= switches.maxAttacks)
+      if (switches.maxAttacks != 0)
 	{
-	  return 1;
+	  if (sys->attackid >= switches.maxAttacks)
+	    {
+	      return 1;
+	    }
 	}
     }
   return 0;