From 81c6be826e74ebafe671bf109a1324553ccdea19 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 14 Jul 2004 08:17:49 +0000
Subject: [PATCH] - Initial symmetry reduction. Gives a lot of warnings
 currently.

---
 src/modelchecker.c | 29 ++++++++++++++++++++++++++++-
 src/runs.c         |  1 +
 src/termlists.c    | 23 +++++++++++++++++++++++
 src/termlists.h    |  1 +
 src/terms.c        | 35 +++++++++++++++++++++++++++++++++++
 src/terms.h        |  1 +
 6 files changed, 89 insertions(+), 1 deletion(-)

diff --git a/src/modelchecker.c b/src/modelchecker.c
index 2f7786f..e3e80a5 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -266,7 +266,34 @@ explorify (const System sys, const int run)
 	      return 0;
 	    }
 	}
-      /* Special check 2: if all agents in each run send only encrypted stuff, and all agents are trusted,
+
+      /* Special check 2: Symmetry reduction.
+       * If the run we depend upon has already been activated (otherwise warn!) check for instance ordering
+       */
+
+      if (sys->runs[run].prevSymmRun != -1)
+	{
+	  /* there is such a run on which we depend */
+	  int ridSymm;
+
+	  ridSymm = sys->runs[run].prevSymmRun;
+	  if (sys->runs[ridSymm].step == 0)
+	    {
+	      warning ("Symmetrical run dependency #%i (for run #%i) has not chosen yet!", ridSymm, run);
+	    }
+	  else
+	    {
+	      /* dependent run has chosen, so we can compare */
+	      if (termlistOrder (sys->runs[run].agents,
+				   sys->runs[ridSymm].agents) < 0)
+		{
+		  /* we only explore the other half */
+		  return 0;
+		}
+	    }
+	}
+
+      /* Special check 3: 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 */
 
diff --git a/src/runs.c b/src/runs.c
index 69a9979..b23d536 100644
--- a/src/runs.c
+++ b/src/runs.c
@@ -605,6 +605,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
   runs[rid].agents = termlistDuplicate (tolist);
   runs[rid].start = rd;
   runs[rid].index = rd;
+  runs[rid].step = 0;
 
   /* duplicate all locals form this run */
   scanto = role->locals;
diff --git a/src/termlists.c b/src/termlists.c
index df6bb39..838fc6f 100644
--- a/src/termlists.c
+++ b/src/termlists.c
@@ -736,3 +736,26 @@ termlistForward (Termlist tl)
     }
 }
 
+/**
+ * Compare two termlists containing only basic terms, and yield ordering.
+ */
+int termlistOrder (Termlist tl1, Termlist tl2)
+{
+  int order;
+
+  order = 0;
+  while (order == 0 && tl1 != NULL && tl2 != NULL)
+    {
+      order = termOrder (tl1->term, tl2->term);
+      tl1 = tl1->next;
+      tl2 = tl2->next;
+    }
+  if (order != 0)
+      return order;
+  if (tl1 == NULL && tl2 == NULL) 
+      return order;
+  if (tl1 == NULL)
+      return -1;
+  else
+      return 1;
+}
diff --git a/src/termlists.h b/src/termlists.h
index 40303a4..1a2c7cf 100644
--- a/src/termlists.h
+++ b/src/termlists.h
@@ -53,5 +53,6 @@ int termlistContained (const Termlist tlbig, Termlist tlsmall);
 int validSubst (const int matchmode, const Term term);
 Term termFunction (Termlist fromlist, Termlist tolist, Term tx);
 Termlist termlistForward (Termlist tl);
+int termlistOrder (Termlist tl1, Termlist tl2);
 
 #endif
diff --git a/src/terms.c b/src/terms.c
index 0fe6365..0a5974b 100644
--- a/src/terms.c
+++ b/src/terms.c
@@ -5,6 +5,7 @@
  * Intended to be a standalone file, however during development it turned out that a termlist structure was needed
  * to define term types, so there is now a dependency loop with termlists.c.
  */
+#include <strings.h>
 #include <stdlib.h>
 #include <stdio.h>
 #include <limits.h>
@@ -758,3 +759,37 @@ termDistance(Term t1, Term t2)
 	}
     }
 }
+
+/**
+ * Enforce a (arbitrary) ordering on basic terms
+ * <0 means a<b, 0 means a=b, >0 means a>b.
+ */
+int termOrder (Term t1, Term t2)
+{
+  char* name1;
+  char* name2;
+
+  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;
+    }
+  if (t1->type != t2->type)
+    {
+      /* unequal types (can this even occur?) */
+      if (t1->type < t2->type)
+	  return -1;
+      else
+	  return 1;
+    }
+  /* same type, compare names */
+  name1 = t1->left.symb->text;
+  name2 = t2->left.symb->text;
+  return strcmp (name1,name2);
+}
diff --git a/src/terms.h b/src/terms.h
index 84d21fd..bfdada4 100644
--- a/src/terms.h
+++ b/src/terms.h
@@ -112,5 +112,6 @@ int tupleCount (Term tt);
 Term tupleProject (Term tt, int n);
 int termSize(Term t);
 float termDistance(Term t1, Term t2);
+int termOrder (Term t1, Term t2);
 
 #endif