- Introduced the 'force-choose' switch, which helps the symmetry

reduction algorithm along, notably.

src/main.c

@@ -99,6 +99,7 @@ main (int argc, char **argv)
     arg_lit0 ("d", "disable-report", "don't report violations.");
   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.");
 #ifdef DEBUG
   struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter.");
   struct arg_lit *switchI = arg_lit0 ("I", "debug-indent",
@@ -123,6 +124,7 @@ main (int argc, char **argv)
     noreport,
     switchS, 
     switchSS,
+    switchFC,
 #ifdef DEBUG
     porparam,
     switchI,
@@ -271,6 +273,12 @@ main (int argc, char **argv)
 
   /* generate system */
   sys = systemInit ();
+  if (switchFC->count > 0)
+    {
+      /* force explicit chooses */
+      sys->switchForceChoose = 1;
+      warning ("Force choose enabled");
+    }
 #ifdef DEBUG
   sys->porparam = porparam->ival[0];
 #endif

src/runs.c

@@ -64,6 +64,7 @@ systemInit ()
   sys->porparam = 0;		// multi-purpose parameter
   sys->latex = 0;		// latex output?
   sys->switchStatespace = 0;
+  sys->switchForceChoose = 0;	// don't force explicit chooses by default
 
   /* set illegal traversal by default, to make sure it is set
      later */
@@ -568,10 +569,9 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 	  /* newvar is apparently new, but it might occur
 	   * in the first event if it's a read, in which
 	   * case we forget it */
-	  if (!(rd->type == READ && termOccurs (rd->message, scanfrom->term)))
+	  if (sys->switchForceChoose || !(rd->type == READ && termOccurs (rd->message, scanfrom->term)))
 	    {
-	      /* but this is already set in the first
+	      /* this term is forced as a choose, or it does not occur in the (first) read event */
-	       * read... */
 	      /* TODO scan might be more complex, but
 	       * this will do for now. I.e. occurring
 	       * first in a read will do */

src/runs.h

@@ -207,6 +207,7 @@ struct system
   int switchS;			//!< Progress display switch. (traversed states)
   int porparam;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
   int switchStatespace;		//!< Output statespace for dot package
+  int switchForceChoose;	//!< Force chooses for each run, even if involved in first read
   //! Latex output switch.
   /**
    * Obsolete. Use globalLatex instead.