- Added the trace prefix cutter. Goody.

src/main.c

@@ -85,6 +85,8 @@ main (int argc, char **argv)
   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_scenario_size =
+      arg_int0 ("S", "scenario-size", NULL, "scenario size (fixed trace prefix length)");
   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 =
@@ -113,7 +115,7 @@ main (int argc, char **argv)
   struct arg_lit *switch_enable_symmetry_order = arg_lit0 (NULL, "symm-order", "enable ordering symmetry reductions");
   struct arg_lit *switch_disable_noclaims_reductions = arg_lit0 (NULL, "no-noclaims-red", "disable no more claims reductions");
   struct arg_lit *switch_disable_endgame_reductions = arg_lit0 (NULL, "no-endgame-red", "disable endgame reductions");
-  struct arg_lit *switch_summary = arg_lit0 ("S", "summary", "show summary on stdout instead of stderr");
+  struct arg_lit *switch_summary = arg_lit0 (NULL, "summary", "show summary on stdout instead of stderr");
   struct arg_lit *switch_echo = arg_lit0 ("E", "echo", "echo command line to stdout");
 #ifdef DEBUG
   struct arg_int *switch_por_parameter = arg_int0 (NULL, "pp", NULL, "POR parameter");
@@ -132,6 +134,7 @@ main (int argc, char **argv)
     switch_empty,
     switch_state_space_graph,
     switch_scenario,
+    switch_scenario_size,
     switch_latex_output,
     switch_summary,
     switch_echo,
@@ -178,6 +181,7 @@ main (int argc, char **argv)
   switch_por_parameter->ival[0] = 0;
 #endif
   switch_scenario->ival[0] = 0;
+  switch_scenario_size->ival[0] = 0;
   switch_traversal_method->ival[0] = 12;
   switch_match_method->ival[0] = 0;
   switch_prune_trace_length->ival[0] = -1;
@@ -338,14 +342,23 @@ main (int argc, char **argv)
    * any scenario traversing selects chooses first.
    */
   sys->switchScenario = switch_scenario->ival[0];		/* scenario selector */
+  sys->switchScenarioSize = switch_scenario_size->ival[0];	/* scenario size */
+  if (sys->switchScenario == 0 && sys->switchScenarioSize > 0)
+    {
+      /* no scenario, but a size is set. so override */
+#ifdef DEBUG
+      warning ("Scanning scenarios.");
+#endif
+      sys->switchScenario = -1;
+    }
   if (sys->switchScenario < 0)
     {
       sys->output = SCENARIOS;
     }
-  if (sys->switchScenario != 0)
+  if (sys->switchScenario != 0 && sys->switchScenarioSize == 0)
     {
 #ifdef DEBUG
-      warning ("Scenario selection implies --choose-first.");
+      warning ("Scenario selection without trace prefix length implies --choose-first.");
 #endif
       sys->switchChooseFirst = 1;
     }

src/modelchecker.c

@@ -553,6 +553,9 @@ explorify (const System sys, const int run)
    * should be the last special check.
    */
   if (sys->switchScenario != 0)
+    {
+      /* two variants. If scenario size is 0, we operate on the old method involving chooses */
+      if (sys->switchScenarioSize == 0)
 	{
 	  /* only after chooses */
 	  if (myStep == 0 &&
@@ -582,18 +585,51 @@ explorify (const System sys, const int run)
 			{
 			  graphScenario (sys, run, rd);
 			}
-		  return 0;
+		      /* act as if executed, but don't really explore it. */
+		      return 1;
 		    }
 		}
 	    }
 	}
-
+      else
-  /* 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 */
+	  /* scenario size is not zero */
-      if (sys->runs[sys->lastChooseRun].step == 0)
+
-	  return 0;
+	  //!@todo Optimization: if the good scenario is already traversed, other trace prefixes need not be explored any further.
+	  if (sys->step+1 == sys->switchScenarioSize)
+	    {
+	      /* Now, the prefix has been set. Count it */
+    	      if (sys->countScenario < INT_MAX)
+		{
+		  sys->countScenario++;
+		}
+	      if (sys->output == SCENARIOS)
+		{
+		  /* apparently we want the output */
+		  int index;
+		  eprintf ("%i\t", sys->countScenario);
+		  index = 0;
+		  while (index < sys->switchScenarioSize)
+		    {
+		      roledefPrint (sys->traceEvent[index]);
+		      eprintf ("#%i; ", sys->traceRun[index]);
+		      index++;
+		    }
+		  eprintf ("\n");
+		}
+	      /* Is this the selected one? */
+	      if (sys->switchScenario != sys->countScenario)
+		{
+		  /* unfortunately, it is also not drawn in the state graph because of this */
+		  if (sys->output == STATESPACE)
+		    {
+		      graphScenario (sys, run, rd);
+		    }
+		  /* act as if executed, but don't really explore it. */
+		  return 1;
+		}
+	    }
+	}
     }
 
   /**

src/role.c

@@ -25,56 +25,56 @@ makeRoledef ()
   return (Roledef) memAlloc (sizeof (struct roledef));
 }
 
-//! Print a role event list.
+//! Print a role event.
 void
 roledefPrint (Roledef rd)
 {
   if (rd == NULL)
     {
-      printf ("[Empty roledef]\n");
+      eprintf ("[Empty roledef]");
       return;
     }
   if (rd->type == READ && rd->internal)
     {
       /* special case: internal read == choose ! */
-      printf ("CHOOSE(");
+      eprintf ("CHOOSE(");
       termPrint (rd->message);
-      printf (")");
+      eprintf (")");
       return;
     }
   if (rd->type == READ)
-    printf ("READ");
+    eprintf ("READ");
   if (rd->type == SEND)
-    printf ("SEND");
+    eprintf ("SEND");
   if (rd->type == CLAIM)
-    printf ("CLAIM");
+    eprintf ("CLAIM");
   if (rd->label != NULL)
     {
       if (globalLatex)
 	{
-	  printf ("$_{");
+	  eprintf ("$_{");
 	  termPrint (rd->label);
-	  printf ("}$");
+	  eprintf ("}$");
 	}
       else
 	{
-	  printf ("_");
+	  eprintf ("_");
 	  termPrint (rd->label);
 	}
     }
   if (globalLatex)
-    printf ("$");
+    eprintf ("$");
-  printf ("(");
+  eprintf ("(");
   termPrint (rd->from);
-  printf (",");
+  eprintf (",");
   if (rd->type == CLAIM)
-    printf (" ");
+    eprintf (" ");
   termPrint (rd->to);
-  printf (", ");
+  eprintf (", ");
   termPrint (rd->message);
-  printf (" )");
+  eprintf (" )");
   if (globalLatex)
-    printf ("$");
+    eprintf ("$");
 }
 
 //! Duplicate a single role event node.
@@ -204,16 +204,16 @@ rolePrint (Role r)
     return;
 
   indent ();
-  printf ("[[Role : ");
+  eprintf ("[[Role : ");
   termPrint (r->nameterm);
-  printf ("]]\n");
+  eprintf ("]]\n");
   locVarPrint (r->locals);
 
   rd = r->roledef;
   while (rd != NULL)
     {
       roledefPrint (rd);
-      printf ("\n");
+      eprintf ("\n");
       rd = rd->next;
     }
 }
@@ -224,7 +224,7 @@ rolesPrint (Role r)
 {
   if (r == NULL)
     {
-      printf ("Empty role.");
+      eprintf ("Empty role.");
     }
   else
     {

src/system.c

@@ -58,6 +58,7 @@ systemInit ()
   sys->porparam = 0;		// multi-purpose parameter
   sys->latex = 0;		// latex output?
   sys->switchScenario = 0;
+  sys->switchScenarioSize = 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

src/system.h

@@ -121,6 +121,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 switchScenario;		//!< -1 to count, 0 for disable, 1-n to select the choose scenario
+  int switchScenarioSize;	//!< Scenario size, also called fixed trace prefix length
   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