- Fixed weird behaviour of executeStep restoration.

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

src/modelchecker.c

@@ -468,11 +468,13 @@ explorify (const System sys, const int run)
     {
       /* traverse the system after the step */
       flag = traverse (sys);
+    }
+  /* 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;

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

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.