From 269b5c76467ee05c5990c0f09489b5bdba34c635 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 14 Jul 2004 09:33:55 +0000
Subject: [PATCH] - Introduced the 'force-choose' switch, which helps the
 symmetry   reduction algorithm along, notably.

---
 src/main.c | 8 ++++++++
 src/runs.c | 6 +++---
 src/runs.h | 1 +
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/main.c b/src/main.c
index c3cd205..2068fb5 100644
--- a/src/main.c
+++ b/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
diff --git a/src/runs.c b/src/runs.c
index b23d536..d99bf25 100644
--- a/src/runs.c
+++ b/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
-	       * read... */
+	      /* this term is forced as a choose, or it does not occur in the (first) read event */
 	      /* TODO scan might be more complex, but
 	       * this will do for now. I.e. occurring
 	       * first in a read will do */
diff --git a/src/runs.h b/src/runs.h
index aa5dced..c05e485 100644
--- a/src/runs.h
+++ b/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.