- Added scen_st to the output, which lists the number of states in the

specific scenario.

src/main.c

@@ -593,6 +593,15 @@ timersPrint (const System sys)
   statesPrintShort (sys);
   eprintf ("\n");
 
+  /* scenario info */
+  
+  if (sys->switchScenario > 0)
+    {
+      eprintf ("scen_st\t");
+      statesFormat (sys->statesScenario);
+      eprintf ("\n");
+    }
+
   /* flag
    *
    * L n          Attack of length <n>
@@ -651,13 +660,13 @@ timersPrint (const System sys)
       eprintf (":");
       termPrint (cl_scan->label);
       eprintf ("\t");
-      statesFormat (stderr, cl_scan->count);
+      statesFormat (cl_scan->count);
       if (cl_scan->count > 0)
 	{
 	  eprintf ("\t");
 	  if (cl_scan->failed > 0)
 	    {
-	      statesFormat (stderr, cl_scan->failed);
+	      statesFormat (cl_scan->failed);
 	      eprintf (" failed");
 	    }
 	}

src/modelchecker.c

@@ -202,16 +202,25 @@ executeStep (const System sys, const int run)
   /* we will explore this state, so count it. */
   sys->states = statesIncrease (sys->states);
 
+  /* what about scenario exploration? */
+  if (sys->switchScenario && sys->step+1 > sys->switchScenarioSize)
+    {
+      /* count states within scenario */
+      sys->statesScenario = statesIncrease (sys->statesScenario);
+    }
+
   /* show progression */
   if (sys->switchS > 0)
     {
       sys->interval = statesIncrease (sys->interval);
       if (!statesSmallerThan (sys->interval, (unsigned long int) sys->switchS))
 	{
+	  globalError++;
 	  sys->interval = STATES0;
-	  fprintf (stderr, "States ");
-	  statesFormat (stderr, sys->states);
-	  fprintf (stderr, " \r");
+	  eprintf ("States ");
+	  statesFormat (sys->states);
+	  eprintf (" \r");
+	  globalError--;
 	}
     }
 

src/output.c

@@ -529,7 +529,7 @@ void graphInit (const System sys)
 
   /* start with initial node 0 */
   printf ("\tn");
-  statesFormat (stdout, STATES0);
+  statesFormat (STATES0);
   printf (" [shape=box,height=0.2,label=\"M0: ");
   tl = knowledgeSet (sys->know);
   termlistPrint (tl);
@@ -560,7 +560,7 @@ void graphNode (const System sys)
 
   /* add node */
   printf ("\tn");
-  statesFormat (stdout, thisNode);
+  statesFormat (thisNode);
   printf (" [");
   
   newtl = knowledgeNew (sys->traceKnow[index], sys->traceKnow[index+1]);
@@ -595,9 +595,9 @@ void graphNode (const System sys)
 
   /* add edge */
   printf ("\tn");
-  statesFormat (stdout, parentNode);
+  statesFormat (parentNode);
   printf (" -> n");
-  statesFormat (stdout, thisNode);
+  statesFormat (thisNode);
   /* add label */
   printf (" [label=\"");
 
@@ -641,7 +641,7 @@ void graphNodePath (const System sys, const int length, const char* nodepar)
 
       /* color node */
       printf ("\tn");
-      statesFormat (stdout, thisNode);
+      statesFormat (thisNode);
       printf (" [%s];\n", nodepar);
       i++;
     }
@@ -661,9 +661,9 @@ void graphEdgePath (const System sys, const int length, const char* edgepar)
 
       /* color edge */
       printf ("\tn");
-      statesFormat (stdout, prevNode);
+      statesFormat (prevNode);
       printf (" -> n");
-      statesFormat (stdout, thisNode);
+      statesFormat (thisNode);
       printf (" [%s];\n", edgepar);
       prevNode = thisNode;
       i++;

src/states.c

@@ -31,10 +31,10 @@ statesSmallerThan (const states_t states, unsigned long int reflint)
  * Acts like a modified form of %g
  */
 __inline__ void
-statesFormat (FILE* out, const states_t states)
+statesFormat (const states_t states)
 {
   if (states < 1000000)
-      fprintf (out, "%lu", states);
+      eprintf ("%lu", states);
   else
-      fprintf (out, "%.3e", statesDouble (states));
+      eprintf ("%.3e", statesDouble (states));
 }

src/states.h

@@ -15,6 +15,6 @@ typedef unsigned long int states_t;
 __inline__ states_t statesIncrease (const states_t states);
 __inline__ double statesDouble (const states_t states);
 __inline__ int statesSmallerThan (const states_t states, unsigned long int reflint);
-__inline__ void statesFormat (FILE* out, const states_t states);
+__inline__ void statesFormat (const states_t states);
 
 #endif

src/system.c

@@ -111,7 +111,8 @@ systemReset (const System sys)
 
   /* some initial counters */
   sys->states = statesIncrease (STATES0);	//!< Initial state is not explored, so start counting at 1
-  sys->interval = statesIncrease (STATES0);	//!< To keep in line with the states
+  sys->statesScenario = STATES0;
+  sys->interval = sys->states;			//!< To keep in line with the states
   sys->claims = STATES0;
   sys->failed = STATES0;
   sys->countScenario = 0;
@@ -205,20 +206,17 @@ systemDone (const System sys)
 void
 statesPrintShort (const System sys)
 {
-  if (globalError == 0)
-    statesFormat (stdout, sys->states);
-  else
-    statesFormat (stderr, sys->states);
+  statesFormat (sys->states);
 }
 
 //! Print the number of states.
 void
 statesPrint (const System sys)
 {
-  statesFormat (stdout, sys->states);
-  printf (" states traversed.\n");
+  statesFormat (sys->states);
+  eprintf (" states traversed.\n");
   if (globalLatex)
-      printf("\n");
+      eprintf("\n");
 }
 
 //! Destroy a system memory block and system::runs

src/system.h

@@ -143,7 +143,8 @@ struct system
   int explore;			//!< Boolean: explore states after actions or not.
 
   /* counters */
-  states_t states;
+  states_t states;		//!< States traversed
+  states_t statesScenario;	//!< States traversed that are within the scenario, not the prefix
   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.