- Added support for more intelligent bounding. Fairly untested at the

moment.

src/arachne.c

@@ -33,6 +33,7 @@
 #include "type.h"
 #include "switches.h"
 #include "specialterm.h"
+#include "cost.h"
 
 extern int *graph;
 extern int nodes;
@@ -40,6 +41,7 @@ extern int graph_uordblks;
 
 static System sys;
 static int attack_length;
+static int attack_leastcost;
 
 Protocol INTRUDER;		// Pointers, to be set by the Init
 Role I_M;			// Same here.
@@ -3194,14 +3196,25 @@ prune_bounds ()
     }
 
   // Limit on exceeding any attack length
-  if (switches.prune == 2 && get_semitrace_length () >= attack_length)
+  if (get_semitrace_length () >= attack_length)
     {
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf ("Pruned: attack length %i.\n", attack_length);
+	}
+      return 1;
+    }
+
+  /* prune for cheaper */
+  if (switches.prune == 2 && attack_leastcost <= attackCost (sys))
+    {
+      // We already had an attack at least this cheap.
       if (switches.output == PROOF)
 	{
 	  indentPrint ();
 	  eprintf
-	    ("Pruned: we already know an attack of length %i.\n",
-	     attack_length);
+	    ("Pruned: attack cost exceeds a previously found attack.\n");
 	}
       return 1;
     }
@@ -3584,7 +3597,7 @@ int
 property_check ()
 {
   int flag;
-  int attack_this;
+  int cost;
 
   flag = 1;
 
@@ -3600,17 +3613,16 @@ property_check ()
     {
       arachneOutputAttack ();
     }
-  // Store attack length if shorter
-  attack_this = get_semitrace_length ();
-  if (attack_this < attack_length)
+  // Store attack cost if cheaper
+  cost = attackCost (sys);
+  if (cost < attack_leastcost)
     {
-      // Shortest attack
-      attack_length = attack_this;
+      // Cheapest attack
+      attack_leastcost = cost;
       if (switches.output == PROOF)
 	{
 	  indentPrint ();
-	  eprintf ("New shortest attack found with trace length %i.\n",
-		   attack_length);
+	  eprintf ("New cheaper attack found with cost %i.\n", cost);
 	}
     }
 
@@ -3855,6 +3867,7 @@ arachne ()
 
 	      sys->current_claim = cl;
 	      attack_length = INT_MAX;
+	      attack_leastcost = INT_MAX;
 	      cl->complete = 1;
 	      p = (Protocol) cl->protocol;
 	      r = (Role) cl->role;

src/cost.c

@@ -0,0 +1,90 @@
+/**
+ *
+ *@file cost.c
+ *
+ * Determine cost of a given semitrace in sys
+ * Constructed for Arachne results, unreliable otherwise.
+ *
+ */
+#include "switches.h"
+
+//************************************************************************
+// Private methods
+//************************************************************************
+
+int selfInitiator(const System sys, const int run)
+{
+  int self_initiator;
+
+  self_initiator = false;
+  if (sys->runs[run].role->initiator)
+    {
+      // An initiator
+      Termlist agents;
+      Termlist seen;
+
+      agents = sys->runs[run].agents;
+      seen = NULL;
+      while (agents != NULL)
+	{
+	  Term agent;
+
+	  agent = agents->term;
+	  if (inTermlist (seen, agent))
+	    {
+	      // This agent was already in the seen list
+	      self_initiator = true;
+	    }
+	  else
+	    {
+	      termlistAdd (seen, agent);
+	    }
+	  agents = agents->next;
+	}
+      termlistDelete (seen);
+    }
+  return self_initiator;
+}
+
+//! Count the number of any self-initiators
+int selfInitiators(const System sys)
+{
+  int count;
+  int run;
+
+  count = 0;
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (selfInitiator (sys, run))
+	{
+	  count++;
+	}
+      run++;
+    }
+  return count;
+}
+
+//************************************************************************
+// Public methods
+//************************************************************************
+
+//! Determine cost of an attack
+/*
+ * This should also work on uncompleted semitraces, and should be monotonous
+ * (i.e. further iterations should increase the cost only) so that it can be
+ * used for branch and bound.
+ *
+ * A lower value (closer to 0) is a more feasible attack.
+ */
+int attackCost(const System sys)
+{
+  int cost;
+
+  cost = 0;
+
+  cost += get_semitrace_length();
+  cost += 5 * selfInitiators(sys);
+
+  return cost;
+}

src/cost.h

@@ -0,0 +1,6 @@
+#ifndef COST
+#define COST
+
+int attackCost(const System sys);
+
+#endif