- Added '--max-depth=X' switch (which is equal to the old '-l X -a')

- Modified semantics of -l with -a : this corresponds more to the
  intuition and introduces the new option to prune proofs based on trace
  length.

src/arachne.c

@@ -1876,18 +1876,51 @@ prune_bounds ()
   Termlist tl;
   List bl;
 
-  if (proofDepth > sys->switch_maxtracelength)
+  /* prune for proof depth */
+  if (proofDepth > sys->switch_maxproofdepth)
     {
       // Hardcoded limit on proof tree depth
       if (sys->output == PROOF)
 	{
 	  indentPrint ();
-	  eprintf ("Pruned: proof tree too deep: %i (-l %i switch)\n",
-		   proofDepth, sys->switch_maxtracelength);
+	  eprintf ("Pruned: proof tree too deep: %i (--max-depth %i switch)\n",
+		   proofDepth, sys->switch_maxproofdepth);
 	}
       return 1;
     }
 
+  /* prune for trace length */
+  if (sys->switch_maxtracelength < INT_MAX)
+    {
+      int tracelength;
+      int run;
+
+      /* compute trace length of current semistate */
+      tracelength = 0;
+      run = 0;
+      while (run < sys->maxruns)
+	{
+	  /* ignore intruder actions */
+	  if (sys->runs[run].protocol != INTRUDER)
+	    {
+	      tracelength = tracelength + sys->runs[run].step;
+	    }
+	  run++;
+	}
+      /* test */
+      if (tracelength > sys->switch_maxtracelength)
+	{
+	  // Hardcoded limit on proof tree depth
+	  if (sys->output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf ("Pruned: trace too long: %i (-l %i switch)\n",
+		       tracelength, sys->switch_maxtracelength);
+	    }
+	  return 1;
+	}
+    }
+
   if (num_regular_runs > sys->switchRuns)
     {
       // Hardcoded limit on runs

src/main.c

@@ -117,7 +117,10 @@ main (int argc, char **argv)
 						    "pruning method (default is 2)");
   struct arg_int *switch_prune_trace_length =
     arg_int0 ("l", "max-length", NULL,
-	      "prune traces longer than <int> events, prune proof deeper than <int> splits.");
+	      "prune traces longer than <int> events.");
+  struct arg_int *switch_prune_proof_depth =
+    arg_int0 (NULL, "max-depth", NULL,
+	      "prune proof deeper than <int> splits.");
   struct arg_lit *switch_incremental_trace_length =
     arg_lit0 (NULL, "increment-traces",
 	      "incremental search using the length of the traces.");
@@ -187,6 +190,7 @@ main (int argc, char **argv)
     switch_match_method,
     switch_clp,
     switch_pruning_method,
+    switch_prune_proof_depth,
     switch_prune_trace_length, switch_incremental_trace_length,
     switch_maximum_runs, switch_incremental_runs,
 
@@ -229,6 +233,7 @@ main (int argc, char **argv)
   switch_traversal_method->ival[0] = 12;
   switch_match_method->ival[0] = 0;
   switch_prune_trace_length->ival[0] = -1;
+  switch_prune_proof_depth->ival[0] = -1;
   switch_maximum_runs->ival[0] = INT_MAX;
   switch_pruning_method->ival[0] = 2;
 
@@ -524,6 +529,8 @@ main (int argc, char **argv)
     }
   if (switch_empty->count > 0)
     sys->output = EMPTY;
+  if (switch_prune_proof_depth->ival[0] >= 0)
+    sys->switch_maxproofdepth = switch_prune_proof_depth->ival[0];
   if (switch_prune_trace_length->ival[0] >= 0)
     sys->switch_maxtracelength = switch_prune_trace_length->ival[0];
 #ifdef DEBUG

src/system.c

@@ -78,6 +78,7 @@ systemInit ()
   /* set illegal traversal by default, to make sure it is set
      later */
   sys->traverse = 0;
+  sys->switch_maxproofdepth = INT_MAX;
   sys->switch_maxtracelength = INT_MAX;
   sys->maxtracelength = INT_MAX;
 

src/system.h

@@ -122,7 +122,8 @@ struct system
   int output;			//!< From enum outputs: what should be produced. Default ATTACK.
   int report;
   int prune;			//!< Type of pruning.
-  int switch_maxtracelength;	//!< Helps to remember the length of the last trace.
+  int switch_maxproofdepth;	//!< Maximum proof depth
+  int switch_maxtracelength;	//!< Maximum trace length allowed
   int maxtracelength;		//!< helps to remember the length of the last trace.
   int switchM;			//!< Memory display switch.
   int switchT;			//!< Time display switch.