From 7ad99f977c2123e06f81977082de796afde9f647 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 19 Jul 2004 09:32:12 +0000
Subject: [PATCH] - Fixed weird behaviour of executeStep restoration.

---
 src/main.c         | 12 ++++++------
 src/modelchecker.c | 10 ++++++----
 src/runs.c         |  1 +
 src/runs.h         |  1 +
 4 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/src/main.c b/src/main.c
index 49b9702..5a6db41 100644
--- a/src/main.c
+++ b/src/main.c
@@ -101,6 +101,7 @@ main (int argc, char **argv)
   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 read symmetry reductions.");
+  struct arg_lit *switchAS = arg_lit0 (NULL, "no-agent-symm", "disable agent 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.");
@@ -128,6 +129,7 @@ main (int argc, char **argv)
     switchSS,
     switchFC,
     switchRS,
+    switchAS,
     switchSO,
 #ifdef DEBUG
     porparam,
@@ -278,23 +280,21 @@ main (int argc, char **argv)
   /* generate system */
   sys = systemInit ();
   if (switchFC->count > 0)
-    {
       /* force explicit chooses */
       sys->switchForceChoose = 1;
-    }
   if (switchRS->count > 0)
     {
       if (switchSO->count > 0)
-	{
 	  error ("--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;
-    }
+  if (switchAS->count > 0)
+      /* disable agent symmetry order */
+      sys->switchAgentSymm = 0;
+
 #ifdef DEBUG
   sys->porparam = porparam->ival[0];
 #endif
diff --git a/src/modelchecker.c b/src/modelchecker.c
index 94baedf..f0f7b78 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -468,11 +468,13 @@ explorify (const System sys, const int run)
     {
       /* traverse the system after the step */
       flag = traverse (sys);
-      runPointerSet (sys, run, rd);	// reset rd pointer
-      sys->runs[run].step = myStep;	// reset local index
-      sys->step--;
-      indentSet (sys->step);
     }
+  /* restore executeStep "damage" */
+  runPointerSet (sys, run, rd);	// reset rd pointer
+  sys->runs[run].step = myStep;	// reset local index
+  sys->step--;
+  indentSet (sys->step);
+
   if (roleCap != NULL)
     {
       roleCap->next = roleCapPart;
diff --git a/src/runs.c b/src/runs.c
index d035f67..212e8ec 100644
--- a/src/runs.c
+++ b/src/runs.c
@@ -66,6 +66,7 @@ systemInit ()
   sys->switchStatespace = 0;
   sys->switchForceChoose = 0;	// don't force explicit chooses by default
   sys->switchReadSymm = 0;	// don't force read symmetries by default
+  sys->switchAgentSymm = 1;	// default enable agent symmetry
   sys->switchSymmOrder = 0;	// don't force symmetry order reduction by default
 
   /* set illegal traversal by default, to make sure it is set
diff --git a/src/runs.h b/src/runs.h
index bdceb51..e4e25d7 100644
--- a/src/runs.h
+++ b/src/runs.h
@@ -211,6 +211,7 @@ 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 switchAgentSymm;		//!< Enable agent symmetry reduction
   int switchSymmOrder;		//!< Enable symmetry order reduction
 
   //! Latex output switch.