- Implemented read symmetries reduction as a switch '--read-symm'. Works with e.g. t8. t10 is also implemented as a test.

src/main.c

@@ -100,6 +100,7 @@ main (int argc, char **argv)
   struct arg_lit *switchS = arg_lit0 (NULL, "no-progress", "suppress progress bar.");
   struct arg_lit *switchSS = arg_lit0 (NULL, "state-space", "output state space graph.");
   struct arg_lit *switchFC = arg_lit0 (NULL, "force-choose", "force only explicit choose events.");
+  struct arg_lit *switchRS = arg_lit0 (NULL, "read-symm", "enable ready symmetry reductions.");
 #ifdef DEBUG
   struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter.");
   struct arg_lit *switchI = arg_lit0 ("I", "debug-indent",
@@ -125,6 +126,7 @@ main (int argc, char **argv)
     switchS, 
     switchSS,
     switchFC,
+    switchRS,
 #ifdef DEBUG
     porparam,
     switchI,
@@ -277,7 +279,10 @@ main (int argc, char **argv)
     {
       /* force explicit chooses */
       sys->switchForceChoose = 1;
-      warning ("Force choose enabled");
+    }
+  if (switchRS->count > 0)
+    {
+      sys->switchReadSymm = 1;
     }
 #ifdef DEBUG
   sys->porparam = porparam->ival[0];

src/modelchecker.c

@@ -91,6 +91,8 @@ traverse (const System sys)
       return traversePOR4 (sys);
     case 9:
       return traversePOR5 (sys);
+    case 10:
+      return traversePOR6 (sys);
     default:
       debug (2, "This is NOT an existing traversal method !");
       exit (1);
@@ -347,6 +349,7 @@ explorify (const System sys, const int run)
 
       roleCap = removeIrrelevant (sys, run, rd);
 
+
       /* Special check x: if all agents in each run send only encrypted stuff, and all agents are trusted,
        * there is no way for the intruder to learn anything else than encrypted terms, so secrecy claims will not
        * be violated anymore if they contain no terms that are encrypted with such keys */
@@ -365,6 +368,63 @@ explorify (const System sys, const int run)
 	*/
     }
 
+  /* 
+   * Special check b1: symmetry reduction part II on similar read events for equal roles.
+   */
+
+  if (sys->switchReadSymm)
+    {
+      if (sys->runs[run].firstNonAgentRead == myStep)
+	{
+	  /* Apparently, we have a possible ordering with our symmetrical friend.
+	   * Check if it has progressed enough, and has the same agents.
+	   */
+	  int ridSymm;
+     
+	  if (rd->type != READ)
+	    {
+	      error ("firstNonAgentRead is not a read?!");
+	    }
+	  ridSymm = sys->runs[run].prevSymmRun;
+	  if (isTermlistEqual (sys->runs[run].agents, sys->runs[ridSymm].agents))
+	    {
+	      /* same agents, so relevant */
+	      if (myStep > 0 && sys->runs[ridSymm].step < myStep)
+		{
+		  // warning ("Symmetrical firstread dependency #%i (for run #%i) has not chosen yet!", ridSymm, run);
+		}
+	      else
+		{
+		  if (sys->runs[ridSymm].step <= myStep)
+		    {
+		      // warning ("Symmetrical firstread dependency #%i (for run #%i) has not read it's firstNonAgentRead %i yet, as it is only at %i!", ridSymm, run, myStep, sys->runs[ridSymm].step);
+		    }
+		  else
+		    {
+		      /* read was done, so we can compare them */
+		      int i;
+		      Roledef rdSymm;
+
+		      rdSymm = sys->runs[ridSymm].start;
+		      i = myStep;
+		      while (i > 0)
+			{
+			  rdSymm = rdSymm->next;
+			  i--;
+			}
+		      /* rdSymm now points to the instance of the symmetrical read */
+		      i = termOrder (rdSymm->message, rd->message);
+		      if (i < 0)
+			{
+			  /* only explore symmetrical variant */
+			  return;
+			}
+		    }
+		}
+	    }
+	}
+    }
+
   /* Apparently, all is well, and we can explore further */
   flag = 0;
   if (roleCap != NULL)
@@ -1140,6 +1200,121 @@ traversePOR5 (const System sys)
   return flag;
 }
 
+/*
+ * POR6
+ *
+ * POR5 but has a left-oriented scan instead of working from the current run.
+ */
+
+int
+traversePOR6 (const System sys)
+{
+  Roledef rd;
+  int flag = 0;
+  int run;
+  int i;
+  int offset;
+
+  /* Previously we did the sends first. This does not always improve things,
+   * depending on the protocol.
+   */
+  // if (nonReads (sys)) return 1;
+
+  /* a choice for choose */
+
+  /* The 'choose' implemented here is the following:
+   *
+   * choose ev#rid
+   * where rid = min(r: ev#r in enabled(sys): (r-lastrun) mod maxruns)
+   * and where lastrun is the runid of the previous event 
+   * in the trace, or 0 if there was none.
+   */
+
+  /* First pick out any choose events */
+  for (run = 0; run < sys->maxruns && !flag; run++)
+    {
+      rd = runPointerGet (sys, run);
+
+      if (rd != NULL)
+	{
+	  switch (rd->type)
+	    {
+	    case CLAIM:
+	    case SEND:
+	      break;
+
+	    case READ:
+	      if (rd->internal)
+		{
+		  flag = executeTry (sys, run);
+		}
+	      break;
+
+	    default:
+	      fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
+	      exit (1);
+	    }
+	}
+    }
+
+  /* Try all events (implicitly we only handle enabled ones) starting with our
+   * first choice.  If one was chosen, flag is set, and the loop aborts. */
+  for (run = 0; run < sys->maxruns && !flag; run++)
+    {
+      rd = runPointerGet (sys, run);
+
+      if (rd != NULL)
+	{
+	  switch (rd->type)
+	    {
+	    case CLAIM:
+	    case SEND:
+	      executeTry (sys, run);
+	      flag = 1;
+	      break;
+
+	    case READ:
+	      /* the sendsdone check only prevent
+	       * some unneccessary inKnowledge tests,
+	       * and branch tests, still improves
+	       * about 15% */
+	      if (sys->knowPhase > rd->knowPhase)
+		{
+		  /* apparently there has been a new knowledge item since the
+		   * previous check */
+
+		  /* implicit check for enabledness */
+		  flag = executeTry (sys, run);
+
+		  /* if it was enabled (flag) we postpone it if it makes sense
+		   * to do so (hasVariable, non internal) */
+		  if (flag && hasTermVariable (rd->message) && !rd->internal)
+		    {
+		      int stackKnowPhase = rd->knowPhase;
+
+		      rd->knowPhase = sys->knowPhase;
+		      if (sys->clp)
+			{
+			  block_clp (sys, run);
+			}
+		      else
+			{
+			  block_basic (sys, run);
+			}
+		      rd->knowPhase = stackKnowPhase;
+		    }
+		}
+	      break;
+
+	    default:
+	      fprintf (stderr, "Encountered unknown event type %i.\n", rd->type);
+	      exit (1);
+	    }
+	}
+    }
+  return flag;
+}
+
 
 int
 propertyCheck (const System sys)

src/runs.c

@@ -65,6 +65,7 @@ systemInit ()
   sys->latex = 0;		// latex output?
   sys->switchStatespace = 0;
   sys->switchForceChoose = 0;	// don't force explicit chooses by default
+  sys->switchReadSymm = 0;	// don't force read symmetries by default:w
 
   /* set illegal traversal by default, to make sure it is set
      later */
@@ -255,6 +256,7 @@ ensureValidRun (System sys, int run)
       myrun.start = NULL;
       myrun.know = knowledgeDuplicate (sys->know);
       myrun.prevSymmRun = -1;
+      myrun.firstNonAgentRead = -1;
     }
 }
 
@@ -521,6 +523,36 @@ int staticRunSymmetry (const System sys,const int rid)
   return -1;	// signal that no symmetrical run was found
 }
 
+//! Determine first read with variables besides agents
+/**
+ *@todo For now, we assume it is simply the first read after the choose, if there is one.
+ */
+int firstNonAgentRead (const System sys, int rid)
+{
+  int step;
+  Roledef rd;
+
+  if (sys->runs[rid].prevSymmRun == -1)
+    {
+      /* if there is no symmetrical run, then this doesn't apply at all */
+      return -1;
+    }
+  rd = sys->runs[rid].start;
+  step = 0;
+  while (rd != NULL && rd->internal && rd->type == READ)	// assumes lazy LR eval
+    {
+      rd = rd->next;
+      step++;
+    }
+  if (rd != NULL && !rd->internal && rd->type == READ)		// assumes lazy LR eval
+    {
+      warning ("First read %i with dependency on symmetrical found in run %i.", step, rid);
+      return step;
+    }
+  /* no such read */
+  return -1;
+}
+
 
 //! Instantiate a role by making a new run.
 /**
@@ -647,7 +679,11 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
   termlistDelete (fromlist);
   runs[rid].locals = tolist;
 
+  /* Determine symmetric run */
   runs[rid].prevSymmRun = staticRunSymmetry (sys, rid);		// symmetry reduction static analysis
+
+  /* Determine first read with variables besides agents */
+  runs[rid].firstNonAgentRead = firstNonAgentRead (sys, rid);	// symmetry reduction type II
 }
 
 //! Make a new role event with the specified parameters.

src/runs.h

@@ -134,6 +134,7 @@ struct run
   Knowledge know;	//!< Current knowledge of the run.
   Termlist locals;	//!< Locals of the run.
   int prevSymmRun;	//!< Used for symmetry reduction. Either -1, or the previous run with the same role def and at least a single parameter.
+  int firstNonAgentRead; //!< Used for symmetry reductions for equal agents runs; -1 if there is no candidate.
 };
 
 //! Shorthand for run pointer.
@@ -208,6 +209,7 @@ struct system
   int porparam;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
   int switchStatespace;		//!< Output statespace for dot package
   int switchForceChoose;	//!< Force chooses for each run, even if involved in first read
+  int switchReadSymm;		//!< Enable read symmetry reduction
   //! Latex output switch.
   /**
    * Obsolete. Use globalLatex instead.

src/terms.c

@@ -761,7 +761,7 @@ termDistance(Term t1, Term t2)
 }
 
 /**
- * Enforce a (arbitrary) ordering on basic terms
+ * Enforce a (arbitrary) ordering on terms
  * <0 means a<b, 0 means a=b, >0 means a>b.
  */
 int termOrder (Term t1, Term t2)
@@ -771,25 +771,72 @@ int termOrder (Term t1, Term t2)
 
   t1 = deVar (t1);
   t2 = deVar (t2);
-  if (!(realTermLeaf (t1) && realTermLeaf (t2)))
-    {
-      error ("'termOrder' can only be applied to two basic terms.");
-    }
   if (isTermEqual (t1,t2))
     {
       /* equal terms */
       return 0;
     }
+
+  /* differ */
   if (t1->type != t2->type)
     {
-      /* unequal types (can this even occur?) */
+      /* different types, so ordering on types first */
       if (t1->type < t2->type)
 	  return -1;
       else
 	  return 1;
     }
-  /* same type, compare names */
+
-  name1 = t1->left.symb->text;
+  /* same type
-  name2 = t2->left.symb->text;
+   * distinguish cases
-  return strcmp (name1,name2);
+   */
+  if (realTermLeaf (t1))
+    {
+      /* compare names */
+      int comp;
+
+      name1 = t1->left.symb->text;
+      name2 = t2->left.symb->text;
+      comp = strcmp (name1,name2);
+      if (comp != 0)
+	{
+	  /* names differ */
+	  return comp;
+	}
+      else
+	{
+	  /* equal names, compare run identifiers */
+	  if (t1->right.runid == t2->right.runid)
+	    {
+	      error ("termOrder: two terms seem to be identical although local precondition says they aren't.");
+	    }
+	  else
+	    {
+	      if (t1->right.runid < t2->right.runid)
+		  return -1;
+	      else
+		  return 1;
+	    }
+	}
+    }
+  else
+    {
+      /* non-leaf */
+      int compL,compR;
+
+      if (isTermEncrypt (t1))
+	{
+	  compL = termOrder (t1->left.op,   t2->left.op);
+	  compR = termOrder (t1->right.key, t2->right.key);
+	}
+      else
+	{
+	  compL = termOrder (t1->left.op1,  t2->left.op1);
+	  compR = termOrder (t1->right.op2, t2->right.op2);
+	}
+      if (compL != 0)
+	  return compL;
+      else
+	  return compR;
+    }
 }