- Added support for different attack heuristics. Disable with --prune=2.

src/arachne.c

@@ -1916,7 +1916,7 @@ makeTraceClass (const System sys, Termlist varlist)
 void
 attackOutputStart (void)
 {
-  if (switches.prune == 2)
+  if (switches.prune != 0)
     {
       FILE *fd;
 
@@ -2181,7 +2181,7 @@ iterate ()
 int
 iterate_buffer_attacks (void)
 {
-  if (switches.prune != 2)
+  if (switches.prune == 0)
     {
       return iterate ();
     }

src/cost.c

@@ -8,6 +8,7 @@
  */
 #include "switches.h"
 #include "system.h"
+#include <limits.h>
 
 //************************************************************************
 // Private methods
@@ -28,18 +29,43 @@
 int
 attackCost (const System sys)
 {
-  int cost;
+  if (switches.prune == 0)
+    {
+      return 0;
+    }
+  if (switches.prune == 1)
+    {
+      // Use nice heuristic cf. work of Gijs Hollestelle. Hand-picked parameters.
+      int cost;
 
-  cost = 0;
+      cost = 0;
 
-  //cost += get_semitrace_length ();
+      //cost += get_semitrace_length ();
 
-  cost += 10 * selfInitiators (sys);
+      cost += 10 * selfInitiators (sys);
-  cost += 7 * selfResponders (sys);
+      cost += 7 * selfResponders (sys);
-  cost += 10 * sys->num_regular_runs;
+      cost += 10 * sys->num_regular_runs;
-  cost += 3 * countInitiators (sys);
+      cost += 3 * countInitiators (sys);
-  cost += 2 * countBindingsDone ();
+      cost += 2 * countBindingsDone ();
-  cost += 1 * sys->num_intruder_runs;
+      cost += 1 * sys->num_intruder_runs;
 
-  return cost;
+      return cost;
+    }
+  if (switches.prune == 2)
+    {
+      // Select the first attack.
+      // Implied by having the cost of traces after finding an attack to be always higher.
+      //
+      if (sys->current_claim->failed > 0)
+	{
+	  // we already have an attack
+	  return INT_MAX;
+	}
+      else
+	{
+	  // return some value relating to the cost (anything less than int_max will do)
+	  return 1;
+	}
+    }
+  error ("Unknown pruning method (cost function not found)");
 }

src/prune_bounds.c

@@ -137,7 +137,7 @@ prune_bounds (const System sys)
     }
 
   /* prune for cheaper */
-  if (switches.prune == 2 && attack_leastcost <= attackCost (sys))
+  if (switches.prune != 0 && attack_leastcost <= attackCost (sys))
     {
       // We already had an attack at least this cheap.
       if (switches.output == PROOF)

src/switches.c

@@ -41,7 +41,7 @@ switchesInit (int argc, char **argv)
   switches.tupling = 0;
 
   // Pruning and Bounding
-  switches.prune = 2;		// default pruning method (just output a single one)
+  switches.prune = 1;		// default pruning method (use heuristic)
   switches.maxproofdepth = INT_MAX;
   switches.maxtracelength = INT_MAX;
   switches.runs = 5;		// default is 5 for usability, but -r 0 or --maxruns=0 will set it back to INT_MAX
@@ -711,7 +711,7 @@ switcher (const int process, int index, int commandline)
       if (!process)
 	{
 	  /* not very important
-	     helptext ("    --prune=<int>", "pruning method when an attack is found [2]");
+	     helptext ("    --prune=<int>", "pruning method when an attack is found [1]");
 	   */
 	}
       else