From 6cf65f068fe972378c1a1f0de6cc867386357bb3 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Thu, 15 Jul 2004 13:32:09 +0000
Subject: [PATCH] - Implemented --symm-order reduction. This clashes with
 --read-symm, but   it actually faster.

---
 src/main.c         | 13 ++++++++++++-
 src/modelchecker.c | 32 +++++++++++++++++++++++++++++++-
 src/runs.c         |  8 +++++++-
 src/runs.h         |  3 +++
 4 files changed, 53 insertions(+), 3 deletions(-)

diff --git a/src/main.c b/src/main.c
index 116b64d..91a4d2e 100644
--- a/src/main.c
+++ b/src/main.c
@@ -100,7 +100,8 @@ 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.");
+  struct arg_lit *switchRS = arg_lit0 (NULL, "read-symm", "enable read symmetry reductions.");
+  struct arg_lit *switchSO = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions.");
 #ifdef DEBUG
   struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter.");
   struct arg_lit *switchI = arg_lit0 ("I", "debug-indent",
@@ -127,6 +128,7 @@ main (int argc, char **argv)
     switchSS,
     switchFC,
     switchRS,
+    switchSO,
 #ifdef DEBUG
     porparam,
     switchI,
@@ -282,8 +284,17 @@ main (int argc, char **argv)
     }
   if (switchRS->count > 0)
     {
+      if (switchSO->count > 0)
+	{
+	  exit ("--read-symm and --symm-order cannot be used at the same time.");
+	}
       sys->switchReadSymm = 1;
     }
+  if (switchSO->count > 0)
+    {
+      /* enable symmetry order */
+      sys->switchSymmOrder = 1;
+    }
 #ifdef DEBUG
   sys->porparam = porparam->ival[0];
 #endif
diff --git a/src/modelchecker.c b/src/modelchecker.c
index 14b1a4f..36f03de 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -417,7 +417,7 @@ explorify (const System sys, const int run)
 		      if (i < 0)
 			{
 			  /* only explore symmetrical variant */
-			  return;
+			  return 0;
 			}
 		    }
 		}
@@ -425,6 +425,36 @@ explorify (const System sys, const int run)
 	}
     }
 
+  /* Special check b2: symmetry order reduction.
+   *
+   * Concept: when there are two identical runs w.r.t. agents, we can make sure one goes before the other.
+   * Depends on prevSymm, skipping chooses even.
+   */
+
+  if (sys->switchSymmOrder && myStep == sys->runs[run].firstReal)
+    {
+      if (sys->runs[run].prevSymmRun != -1)
+	{
+	  /* there is such a run on which we depend */
+	  int ridSymm;
+
+	  ridSymm = sys->runs[run].prevSymmRun;
+	  /* equal runs? */
+
+	  if (isTermlistEqual (sys->runs[run].agents, sys->runs[ridSymm].agents))
+	    {
+	      /* so, we have an identical partner */
+	      /* is our partner there already? */
+	      if (sys->runs[ridSymm].step <= myStep)
+		{
+		  /* not yet there, this is not a valid exploration */
+		  /* verify !! */
+		  return 0;
+		}
+	    }
+	}
+    }
+
   /* Apparently, all is well, and we can explore further */
   flag = 0;
   if (roleCap != NULL)
diff --git a/src/runs.c b/src/runs.c
index 9910d3c..7e3559f 100644
--- a/src/runs.c
+++ b/src/runs.c
@@ -65,7 +65,8 @@ 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
+  sys->switchReadSymm = 0;	// don't force read symmetries by default
+  sys->switchSymmOrder = 0;	// don't force symmetry order reduction by default
 
   /* set illegal traversal by default, to make sure it is set
      later */
@@ -629,6 +630,11 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
       rdnew->internal = 1;
       rdnew->next = rd;
       rd = rdnew;
+      runs[rid].firstReal = 1;
+    }
+  else
+    {
+      runs[rid].firstReal = 0;
     }
 
   /* set parameters */
diff --git a/src/runs.h b/src/runs.h
index 989028a..bdceb51 100644
--- a/src/runs.h
+++ b/src/runs.h
@@ -135,6 +135,7 @@ struct 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.
+  int firstReal;	//!< 1 if a choose was inserted, otherwise 0
 };
 
 //! Shorthand for run pointer.
@@ -210,6 +211,8 @@ struct system
   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
+  int switchSymmOrder;		//!< Enable symmetry order reduction
+
   //! Latex output switch.
   /**
    * Obsolete. Use globalLatex instead.