- Some more work on hidelevel backbone.

- Added '--count-states' switch for the Arachne engine.

src/arachne.c

@@ -38,6 +38,7 @@
 #include "prune_bounds.h"
 #include "prune_theorems.h"
 #include "arachne.h"
+#include "hidelevel.h"
 
 extern int *graph;
 extern int nodes;
@@ -1934,6 +1935,8 @@ iterate ()
 		   */
 
 		  sys->states = statesIncrease (sys->states);
+		  sys->current_claim->states =
+		    statesIncrease (sys->current_claim->states);
 
 		  /**
 		   * Check whether its a final state (i.e. all goals bound)

src/compiler.c

@@ -449,6 +449,7 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
   cl->complete = 0;
   cl->timebound = 0;
   cl->failed = 0;
+  cl->states = 0;
   cl->prec = NULL;
   cl->roles = NULL;
   cl->alwaystrue = false;

src/hidelevel.c

@@ -123,6 +123,40 @@ hidelevelCompute (const System sys)
     }
 }
 
+//! Determine flag from parameters
+unsigned int
+hidelevelParamFlag (unsigned int l, unsigned int lmin, unsigned int lprot,
+		    unsigned int lknow)
+{
+  // Given the parameters, determine where the term with hidelevel l could be generated from.
+  if (l < lmin)
+    {
+      return HLFLAG_NONE;
+    }
+  else
+    {
+      // One should work (at least)
+      if (l < lprot)
+	{
+	  // Know should be possible
+	  return HLFLAG_KNOW;
+	}
+      else
+	{
+	  // Prot can, know also?
+	  if (l < lknow)
+	    {
+	      // Nope, just prot
+	      return HLFLAG_PROT;
+	    }
+	  else
+	    {
+	      // Both
+	      return HLFLAG_BOTH;
+	    }
+	}
+    }
+}
 
 //! Given a term, iterate over all factors
 int
@@ -185,3 +219,29 @@ hidelevelImpossible (const System sys, const Term goalterm)
 
   return !iterate_interesting (sys, goalterm, possible);
 }
+
+//! Return flag on the basis of the Hidelevel lemma
+int
+hidelevelFlag (const System sys, const Term goalterm)
+{
+  unsigned int flag;
+
+  int getflag (unsigned int l, unsigned int lmin, unsigned int lprot,
+	       unsigned int lknow)
+  {
+    // Determine new flag
+    flag = flag | hidelevelParamFlag (l, lmin, lprot, lknow);
+
+    // Should we proceed?
+    if (flag == HLFLAG_NONE)
+      {
+	// abort iteration: it cannot get worse
+	return false;
+      }
+    return true;
+  }
+
+  flag = HLFLAG_BOTH;
+  iterate_interesting (sys, goalterm, getflag);
+  return flag;
+}

src/hidelevel.h

@@ -4,6 +4,17 @@
 #include "term.h"
 #include "system.h"
 
+/*
+ * Flags for hidelevel lemma
+ *
+ * Use binary or (|) to compose results: by default, a term can be satisfied by
+ * both the protocol and the initial knowledge.
+ */
+#define HLFLAG_BOTH 0
+#define HLFLAG_KNOW 1
+#define HLFLAG_PROT 2
+#define HLFLAG_NONE 3
+
 /*
  * The structure hiddenterm/Hiddenterm is defined in system.h
  */

src/main.c

@@ -559,6 +559,16 @@ timersPrint (const System sys)
 		}
 	    }
 
+	  /* states (if asked) */
+	  if (switches.engine == ARACHNE_ENGINE)
+	    {
+	      if (switches.countStates)
+		{
+		  eprintf ("\tstates=");
+		  statesFormat (cl_scan->states);
+		}
+	    }
+
 	  /* any warnings */
 	  if (cl_scan->warnings)
 	    {

src/prune_bounds.c

@@ -104,7 +104,10 @@ prune_bounds (const System sys)
     }
 
   // This needs some foundation. Probably * 2^max_encryption_level
-  //!@todo Fix this bound
+  //!@todo Remove later
+  /**
+   * This should be removed once the hidelevel lemma works correctly
+   */
   if ((switches.match < 2)
       && (num_intruder_runs >
 	  ((double) switches.runs * max_encryption_level * 8)))

src/prune_theorems.c

@@ -243,6 +243,7 @@ prune_theorems (const System sys)
       b = bl->data;
 
       // Check for "Hidden" interm goals
+      //!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs
       if (termInTerm (b->term, TERM_Hidden))
 	{
 	  // Prune the state: we can never meet this
@@ -259,7 +260,7 @@ prune_theorems (const System sys)
       // Check for encryption levels
       /*
        * if (switches.match < 2
-       *!@todo Doesn't work yet as desired for Tickets. Prove lemma first.
+       *!@TODO Doesn't work yet as desired for Tickets. Prove lemma first.
        */
       if (switches.experimental)
 	{
@@ -283,6 +284,7 @@ prune_theorems (const System sys)
       // Check for SK-type function occurrences
       //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove.
       // The idea is that functions are never sent as a whole, but only used in applications.
+      //!@TODO Subsumed by hidelevel lemma later
       if (isTermFunctionName (b->term))
 	{
 	  if (!inKnowledge (sys->know, b->term))

src/role.h

@@ -12,6 +12,9 @@ enum eventtype
 { READ, SEND, CLAIM };
 
 //! The container for the claim info list
+/**
+ * Defaults are set in compiler.c (claimCreate)
+ */
 struct claimlist
 {
   //! The type of claim
@@ -33,6 +36,8 @@ struct claimlist
   states_t count;
   //! Number of occurrences that failed.
   states_t failed;
+  //! Number of iterations traversed for this claim.
+  states_t states;
   //! Whether the result is complete or not (failings always are!)
   int complete;
   //! If we ran into the time bound (incomplete, and bad for results)

src/switches.c

@@ -89,6 +89,7 @@ switchesInit (int argc, char **argv)
   switches.reportMemory = 0;
   switches.reportTime = 0;
   switches.reportStates = 0;
+  switches.countStates = false;	// default off
   switches.extendNonReads = 0;	// default off
   switches.extendTrivial = 0;	// default off
   switches.plain = false;	// default colors
@@ -940,6 +941,21 @@ switcher (const int process, int index, int commandline)
   /* ==================
    *  External options
    */
+  if (detect (' ', "count-states", 0))
+    {
+      if (!process)
+	{
+	  /* not very important
+	     helptext ("    --count-states", "report on states (per claim)");
+	   */
+	}
+      else
+	{
+	  switches.countStates = true;
+	  return index;
+	}
+    }
+
   if (!process)
     printf ("Misc. switches:\n");
 

src/switches.h

@@ -67,6 +67,7 @@ struct switchdata
   int reportMemory;		//!< Memory display switch.
   int reportTime;		//!< Time display switch.
   int reportStates;		//!< Progress display switch. (traversed states)
+  int countStates;		//!< Count states
   int extendNonReads;		//!< Show further events in arachne xml output.
   int extendTrivial;		//!< Show further events in arachne xml output, based on knowledge underapproximation. (Includes at least the events of the nonreads extension)
   int plain;			//!< Disable color output