- Added switch --choose-first.

- Added switch --scenario (-s), to enable scenario exploration only.
  Use --scenario=-1 to count the number of possible scenarios.

src/main.c

@@ -78,6 +78,8 @@ main (int argc, char **argv)
 
   struct arg_file *infile  = arg_file0(NULL,NULL,"FILE",    "input file ('-' for stdin)");
   struct arg_file *outfile = arg_file0("o","output","FILE", "output file (default is stdout)");
+  struct arg_int *switch_scenario =
+      arg_int0 ("s", "scenario", NULL, "select a scenario instance 1-n (-1 to count)");
   struct arg_int *switch_traversal_method = arg_int0 ("t", "traverse", NULL,
 					"set traversal method, partial order reduction (default is 12)");
   struct arg_int *switch_match_method =
@@ -100,6 +102,7 @@ main (int argc, char **argv)
   struct arg_lit *switch_no_progress_bar = arg_lit0 (NULL, "no-progress", "suppress progress bar");
   struct arg_lit *switch_state_space_graph = arg_lit0 (NULL, "state-space", "output state space graph");
   struct arg_lit *switch_implicit_choose = arg_lit0 (NULL, "implicit-choose", "allow implicit choose events (useful for few runs)");
+  struct arg_lit *switch_choose_first = arg_lit0 (NULL, "choose-first", "priority to any choose events");
   struct arg_lit *switch_enable_read_symmetries = arg_lit0 (NULL, "read-symm", "enable read symmetry reductions");
   struct arg_lit *switch_disable_agent_symmetries = arg_lit0 (NULL, "no-agent-symm", "disable agent symmetry reductions");
   struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions");
@@ -119,6 +122,7 @@ main (int argc, char **argv)
   void *argtable[] = {
     infile, 
     outfile,
+    switch_scenario,
     switch_traversal_method, 
     switch_match_method, 
     switch_clp,
@@ -130,6 +134,7 @@ main (int argc, char **argv)
     switch_no_progress_bar, 
     switch_state_space_graph,
     switch_implicit_choose,
+    switch_choose_first,
     switch_enable_read_symmetries,
     switch_disable_agent_symmetries,
     switch_enable_symmetry_order,
@@ -161,6 +166,7 @@ main (int argc, char **argv)
   switch_debug_level->ival[0] = 0;
   switch_por_parameter->ival[0] = 0;
 #endif
+  switch_scenario->ival[0] = 0;
   switch_traversal_method->ival[0] = 12;
   switch_match_method->ival[0] = 0;
   switch_prune_trace_length->ival[0] = -1;
@@ -272,7 +278,12 @@ main (int argc, char **argv)
   symbolsInit ();
   tacInit ();
 
-  /* generate system */
+  /*
+   * ------------------------------------------------
+   *	 generate system 
+   * ------------------------------------------------
+   */
+
   sys = systemInit ();
 
   /* transfer command line */
@@ -289,6 +300,8 @@ main (int argc, char **argv)
   if (switch_implicit_choose->count > 0)
       /* allow implicit chooses */
       sys->switchForceChoose = 0;
+  if (switch_choose_first->count > 0)
+      sys->switchChooseFirst = 1;	/* priority to chooses */
   if (switch_enable_read_symmetries->count > 0)
     {
       if (switch_enable_symmetry_order->count > 0)
@@ -304,6 +317,19 @@ main (int argc, char **argv)
   if (switch_disable_endgame_reductions->count > 0)
       sys->switchReduceEndgame = 0;	/* disable endgame cutter */
 
+  /*
+   * The scenario selector has an important side effect; when it is non-null,
+   * any scenario traversing selects chooses first.
+   */
+  sys->switchScenario = switch_scenario->ival[0];	/* scenario selector */
+  if (sys->switchScenario != 0)
+    {
+#ifdef DEBUG
+      warning ("Scenario selection implies --choose-first.");
+#endif
+      sys->switchChooseFirst = 1;
+    }
+
 #ifdef DEBUG
   sys->porparam = switch_por_parameter->ival[0];
 #endif
@@ -525,6 +551,12 @@ timersPrint (const System sys)
 
   fprintf (stderr, "\n");
 #endif
+  
+  /* if scenario counting, display */
+  if (sys->switchScenario < 0)
+    {
+      fprintf (stderr, "Number of scenarios found: %i\n", sys->countScenario);
+    }
 }
 
 //! Analyse the model by incremental runs.
@@ -550,6 +582,7 @@ MC_incRuns (const System sys)
     {
       systemReset (sys);
       sys->maxruns = runs;
+      systemRuns (sys);
       fprintf (stderr, "%i of %i runs in incremental runs search.\n", runs, maxruns);
       res = modelCheck (sys);
       fprintf (stderr, "\n");
@@ -603,6 +636,7 @@ MC_incTraces (const System sys)
     {
       systemReset (sys);
       sys->maxtracelength = tracelen;
+      systemRuns (sys);
       fprintf (stderr, "%i of %i trace length in incremental trace length search.\n",
 	      tracelen, maxtracelen);
       res = modelCheck (sys);
@@ -636,6 +670,7 @@ MC_single (const System sys)
    */
 
   systemReset (sys);		// reset any globals
+  systemRuns (sys);		// init runs data
   modelCheck (sys);
 }
 

src/modelchecker.c

@@ -74,9 +74,45 @@ statePrint (const System sys)
   printf ("\n");
 }
 
+//! Scenario selection makes sure implicit and explicit chooses are selected first.
+/**
+ * This help function traverses any chooses first.
+ */
+__inline__ int
+traverse_chooses_first (const System sys)
+{
+  int run_scan;
+
+  for (run_scan = 0; run_scan < sys->maxruns; run_scan++)
+    {
+      Roledef rd_scan;
+
+      rd_scan = runPointerGet (sys, run_scan);
+      if (rd_scan != NULL &&				// Not empty run
+	  rd_scan == sys->runs[run_scan].start &&	// First event
+	  rd_scan->type == READ)			// Read
+	{
+	  if (executeTry (sys, run_scan))
+	      return 1;
+	}
+    }
+  return 0;
+}
+
+//! Main traversal call.
+/**
+ * Branches into submethods.
+ */
 int
 traverse (const System sys)
 {
+  /* maybe chooses have precedence over _all_ methods */
+  if (sys->switchChooseFirst)
+    {
+      if (traverse_chooses_first (sys))
+	  return 1;
+    }
+  
   /* branch for traversal methods */
   switch (sys->traverse)
     {
@@ -369,7 +405,7 @@ explorify (const System sys, const int run)
 	    }
 	}
 
-      /* Special check 2: Symmetry reduction.
+      /* Special check 2: Symmetry reduction on chooses.
        * If the run we depend upon has already been activated (otherwise warn!) check for instance ordering
        */
 
@@ -509,6 +545,59 @@ explorify (const System sys, const int run)
 	}
     }
 
+  /**
+   * Final special check; we must be sure that chooses have been done. Only
+   * necessary for scenario != 0.
+   *
+   * Note: any choose selection after this would result in empty scenarios, so this
+   * should be the last special check.
+   */
+  if (sys->switchScenario != 0)
+    {
+      /* only after chooses */
+      if (myStep == 0 &&
+	  rd->type == READ)
+	{
+	  if (run == sys->lastChooseRun)
+	    {
+	      /* We are just after the last choose instance */
+	      /* count this instance */
+	      if (sys->countScenario < INT_MAX)
+		{
+      	          sys->countScenario++;
+		}
+#ifdef DEBUG
+	      /* If we are counting and debug, print it */
+	      if (sys->switchScenario < 0)
+		{
+		  printf ("// Scenario %i: ", sys->countScenario);
+		  scenarioPrint (sys);
+		  printf ("\n");
+		}
+#endif
+	      /* If it is not the selected one, abort */
+	      if (sys->switchScenario != sys->countScenario)
+		{
+		  /* this branch is not interesting */
+		  /* unfortunately, it is also not drawn in the state graph because of this */
+		  if (sys->switchStatespace)
+		    {
+		      graphScenario (sys, run, rd);
+		    }
+		  return 0;
+		}
+	    }
+	}
+    }
+
+  /* if there are chooses, and they are to go first, we must always wait for them */
+  if (myStep == 1 && sys->switchChooseFirst && sys->lastChooseRun >= 0)
+    {
+      /* we only explore this if all chooses have been done, and will be doing stuff */
+      if (sys->runs[sys->lastChooseRun].step == 0)
+	  return 0;
+    }
+
   /**
    * --------------------------------------------
    * Now we assume the event is indeed enabled !

src/output.c

@@ -514,7 +514,8 @@ void graphInit (const System sys)
 
   /* fit stuff onto the page */
   printf ("\trankdir=LR;\n");
-  printf ("\tpage=\"8.5,11\";\n");
+  printf ("\tsize=\"8.5,11\";\n");
+  //printf ("\tpage=\"8.5,11\";\n");
   printf ("\tfontsize=\"6\";\n");
   printf ("\tfontname=\"Helvetica\";\n");
   printf ("\tmargin=0.5;\n");
@@ -550,6 +551,7 @@ void graphNode (const System sys)
   Termlist newtl;
   states_t thisNode, parentNode;
   int index;
+  int run;
   Roledef rd;
 
   /* determine node numbers */
@@ -557,6 +559,7 @@ void graphNode (const System sys)
   parentNode = sys->traceNode[index];
   thisNode = sys->states;
   rd = sys->traceEvent[index];
+  run = sys->traceRun[index];
 
   /* add node */
   printf ("\tn");
@@ -575,8 +578,22 @@ void graphNode (const System sys)
   else
     {
       /* no added knowledge */
+      if (sys->switchScenario != 0 &&
+	  rd != NULL &&
+	  rd == sys->runs[run].start &&
+	  rd->type == READ &&
+	  run == sys->lastChooseRun)
+	{
+	  /* last choose; scenario selected */
+	  printf ("shape=box,height=0.2,label=\"Scenario %i: ", sys->countScenario);
+	  scenarioPrint (sys);
+	  printf ("\"");
+	}
+      else
+	{
       	  printf ("label=\"\"");
 	}
+    }
   printf ("];\n");
 
   /* add edge */
@@ -586,14 +603,19 @@ void graphNode (const System sys)
   statesFormat (stdout, thisNode);
   /* add label */
   printf (" [label=\"");
-  if (rd->type == CLAIM && untrustedAgent (sys, sys->runs[sys->traceRun[index]].agents))
+
+  // Print step 
+  printf ("%i:",sys->runs[run].step-1);
+
+  if (rd->type == CLAIM && untrustedAgent (sys, sys->runs[run].agents))
     {
-      printf ("Skip claim in #%i\"", sys->traceRun[index]);
+      printf ("Skip claim in #%i\"", run);
     }
   else
     {
+      // Print event
       roledefPrint (rd);
-      printf ("#%i\"", sys->traceRun[index]);
+      printf ("#%i\"", run);
       if (rd->type == CLAIM)
 	{
           printf (",shape=house,color=green");
@@ -656,3 +678,25 @@ void graphPath (const System sys, int length)
   graphNodePath (sys,length,"style=bold,color=red");
   graphEdgePath (sys,length-1,"style=bold,color=red");
 }
+
+//! Scenario for graph; bit of a hack
+void
+graphScenario (const System sys, const int run, const Roledef rd)
+{
+  /* Add scenario node */
+  printf ("\ts%i [shape=box,height=0.2,label=\"Scenario %i: ",
+	  sys->countScenario,
+	  sys->countScenario);
+  scenarioPrint (sys);
+  printf ("\"];\n");
+
+  /* draw edge */
+  printf ("\tn%i -> s%i",
+	  sys->traceNode[sys->step],
+	  sys->countScenario);
+  printf (" [color=blue,label=\"");
+  printf ("%i:",sys->runs[run].step);
+  roledefPrint (rd);
+  printf ("#%i", run);
+  printf ("\"];\n");
+}

src/output.h

@@ -13,5 +13,6 @@ void graphNodePath (const System sys, const int length, const char*
 void graphEdgePath (const System sys, const int length, const char*
 		edgepar);
 void graphPath (const System sys, int length);
+void graphScenario (const System sys, const int run, const Roledef rd);
 
 #endif

src/system.c

@@ -56,8 +56,10 @@ systemInit ()
   /* switches */
   sys->porparam = 0;		// multi-purpose parameter
   sys->latex = 0;		// latex output?
+  sys->switchScenario = 0;
   sys->switchStatespace = 0;
   sys->switchForceChoose = 1;	// force explicit chooses by default
+  sys->switchChooseFirst = 0;	// no priority to 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
@@ -111,6 +113,7 @@ systemReset (const System sys)
   sys->interval = statesIncrease (STATES0);	//!< To keep in line with the states
   sys->claims = STATES0;
   sys->failed = STATES0;
+  sys->countScenario = 0;
   sys->explore = 1;		// do explore the space
   cl = sys->claimlist;
   while (cl != NULL)
@@ -136,6 +139,35 @@ systemReset (const System sys)
    * single subprocedure such as termPrint */
 
   globalLatex = sys->latex;
+
+}
+
+//! Initialize runtime system (according to cut traces, limited runs)
+void
+systemRuns (const System sys)
+{
+  int run;
+
+  sys->lastChooseRun = -1;
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      Roledef rd;
+
+      rd = runPointerGet (sys, run);
+      if (rd != NULL &&
+	  rd->internal &&
+	  rd->type == READ)
+	{
+	  /* increasing run traversal, so this yields max */
+	  sys->lastChooseRun = run;
+	}
+    }
+#ifdef DEBUG
+  if (sys->switchScenario < 0)
+    {
+      printf ("// Last run with a choose: %i\n",sys->lastChooseRun);
+    }
+#endif
 }
 
 //! Delete a system structure and clear used memory for all buffers.
@@ -498,6 +530,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
       rdnew->internal = 1;
       rdnew->next = rd;
       rd = rdnew;
+      /* mark the first real action */
       runs[rid].firstReal = 1;
     }
   else
@@ -882,3 +915,26 @@ int compute_roleeventmax (const System sys)
     }
   return maxev;
 }
+
+//! Print the role, agents of a run
+void
+runInstancePrint (const System sys, const int run)
+{
+  termlistPrint (sys->runs[run].agents);
+}
+
+//! Print an instantiated scenario (chooses and such)
+void
+scenarioPrint (const System sys)
+{
+  int run;
+
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      runInstancePrint (sys, run);
+      if (run < sys->maxruns - 2)
+	{
+          printf (", ");
+	}
+    }
+}

src/system.h

@@ -117,8 +117,10 @@ struct system
   int switchT;			//!< Time display switch.
   int switchS;			//!< Progress display switch. (traversed states)
   int porparam;			//!< A multi-purpose integer parameter, passed to the partial order reduction method selected.
+  int switchScenario;		//!< -1 to count, 0 for disable, 1-n to select the choose scenario
   int switchStatespace;		//!< Output statespace for dot package
   int switchForceChoose;	//!< Force chooses for each run, even if involved in first read
+  int switchChooseFirst;	//!< Priority to chooses, implicit and explicit
   int switchReadSymm;		//!< Enable read symmetry reduction
   int switchAgentSymm;		//!< Enable agent symmetry reduction
   int switchSymmOrder;		//!< Enable symmetry order reduction
@@ -141,6 +143,7 @@ struct system
   states_t interval;		//!< Used to update state printing at certain intervals
   states_t claims;		//!< Number of claims encountered.
   states_t failed;		//!< Number of claims failed.
+  int countScenario;		//!< Number of scenarios skipped.
 
   /* matching */
   int match;			//!< Matching type.
@@ -155,6 +158,7 @@ struct system
   /* protocol preprocessing */
   int rolecount;		//!< Number of roles in the system
   int roleeventmax;		//!< Maximum number of events in a single role
+  int lastChooseRun;		//!< Last run with a choose event
   Claimlist claimlist;		//!< List of claims in the system, with occurrence counts
 
   /* constructed trace pointers, static */
@@ -181,6 +185,7 @@ typedef struct system *System;
 
 System systemInit ();
 void systemReset (const System sys);
+void systemRuns (const System sys);
 System systemDuplicate (const System fromsys);
 void statesPrint (const System sys);
 void statesPrintShort (const System sys);
@@ -212,4 +217,6 @@ void commandlinePrint (FILE *stream, const System sys);
 int compute_rolecount (const System sys);
 int compute_roleeventmax (const System sys);
 
+void scenarioPrint (const System sys);
+
 #endif