From a5efc6106a59eb35043cc2b5ca3dfc5311e7d2ab Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 14 Jul 2004 07:31:01 +0000
Subject: [PATCH] - Static run symmetry detection seems to work just fine. -
 Added 'warning' call to error.h

---
 src/error.c | 16 +++++++++++
 src/error.h |  1 +
 src/runs.c  | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/runs.h  |  1 +
 4 files changed, 100 insertions(+)

diff --git a/src/error.c b/src/error.c
index aa6c03d..913e00e 100644
--- a/src/error.c
+++ b/src/error.c
@@ -54,3 +54,19 @@ error (char *fmt, ... )
   va_end (args);
   error_die ();
 }
+
+//! Print warning
+/**
+ * Input is comparable to printf, only end of line is not required.
+ */
+void
+warning (char *fmt, ... )
+{
+  va_list args;
+
+  va_start (args, fmt);
+  fprintf (stderr, "warning: ");
+  vfprintf (stderr, fmt, args);
+  fprintf (stderr, "\n");
+  va_end (args);
+}
diff --git a/src/error.h b/src/error.h
index c6f3c45..85216de 100644
--- a/src/error.h
+++ b/src/error.h
@@ -5,5 +5,6 @@ void error_die (void);
 void error_pre (void);
 void error_post (char *fmt, ... );
 void error (char *fmt, ... );
+void warning (char *fmt, ... );
 
 #endif
diff --git a/src/runs.c b/src/runs.c
index f613a18..69a9979 100644
--- a/src/runs.c
+++ b/src/runs.c
@@ -253,6 +253,7 @@ ensureValidRun (System sys, int run)
       myrun.index = NULL;
       myrun.start = NULL;
       myrun.know = knowledgeDuplicate (sys->know);
+      myrun.prevSymmRun = -1;
     }
 }
 
@@ -441,6 +442,85 @@ roledefDestroy (Roledef rd)
   return;
 }
 
+/**
+ * A new run is created; now we want to know if it depends on any previous run.
+ * This occurs when there is a smaller runid with an identical protocol role, with the 
+ * same agent pattern. However, there must be at least a variable in the pattern or no
+ * symmetry gains are to be made.
+ *
+ * Return -1 if there is no such symmetry.
+ */
+int staticRunSymmetry (const System sys,const int rid)
+{
+  int ridSymm;		// previous symmetrical run
+  Termlist agents;	// list of agents for rid
+  Run runs;		// shortcut usage
+
+  ridSymm = -1;
+  runs = sys->runs;
+  agents = runs[rid].agents;
+  while (agents != NULL)
+    {
+      if (isTermVariable(agents->term))
+          ridSymm = rid - 1;
+      agents = agents->next;
+    }
+  /* there is no variable in this roledef, abort */
+  if (ridSymm == -1)
+      return -1;
+
+  agents = runs[rid].agents;
+  while (ridSymm >= 0)
+    {
+      /* compare protocol name, role name */
+      if (runs[ridSymm].protocol == runs[rid].protocol &&
+	  runs[ridSymm].role     == runs[rid].role)
+	{
+	  /* same stuff */
+	  int isEqual;
+	  Termlist al, alSymm;	// agent lists
+
+	  isEqual = 1;
+	  al = agents;
+	  alSymm = runs[ridSymm].agents;
+	  while (isEqual && al != NULL)
+	    {
+	      /* determine equality */
+	      if (isTermVariable (al->term))
+		{
+		  /* case 1: variable, should match type */
+		  if (isTermVariable (alSymm->term))
+		    {
+		      if (!isTermlistEqual (al->term->stype, alSymm->term->stype))
+			  isEqual = 0;
+		    }
+		  else
+		    {
+		      isEqual = 0;
+		    }
+		}
+	      else
+		{
+		  /* case 2: constant, should match */
+		  if (!isTermEqual (al->term, alSymm->term))
+		      isEqual = 0;
+		}
+	      alSymm = alSymm->next;
+	      al = al->next;
+	    }
+	  if (al == NULL && isEqual)
+	    {
+	      /* this candidate is allright */
+  	      warning ("Symmetry detection. #%i can depend on #%i.",rid,ridSymm);
+	      return ridSymm;
+	    }
+	}
+      ridSymm--;
+    }
+  return -1;	// signal that no symmetrical run was found
+}
+
+
 //! Instantiate a role by making a new run.
 /**
  * This involves creation of a new run(id).
@@ -565,6 +645,8 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
     }
   termlistDelete (fromlist);
   runs[rid].locals = tolist;
+
+  runs[rid].prevSymmRun = staticRunSymmetry (sys, rid);		// symmetry reduction static analysis
 }
 
 //! Make a new role event with the specified parameters.
diff --git a/src/runs.h b/src/runs.h
index 356f4d0..aa5dced 100644
--- a/src/runs.h
+++ b/src/runs.h
@@ -133,6 +133,7 @@ struct run
   Roledef start;	//!< Head of the run definition.
   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.
 };
 
 //! Shorthand for run pointer.