- Added preliminary support for state space printing using the dot

package. Use the "--state-space" switch.

src/main.c

@@ -97,7 +97,8 @@ main (int argc, char **argv)
   struct arg_lit *latex = arg_lit0 (NULL, "latex", "output in LaTeX format.");
   struct arg_lit *noreport =
     arg_lit0 ("d", "disable-report", "don't report violations.");
-  struct arg_lit *switchS = arg_lit0 (NULL, "no-progress", "surpress progress bar.");
+  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.");
 #ifdef DEBUG
   struct arg_int *porparam = arg_int0 (NULL, "pp", NULL, "POR parameter.");
   struct arg_lit *switchI = arg_lit0 ("I", "debug-indent",
@@ -121,6 +122,7 @@ main (int argc, char **argv)
     latex,
     noreport,
     switchS, 
+    switchSS,
 #ifdef DEBUG
     porparam,
     switchI,
@@ -327,6 +329,11 @@ main (int argc, char **argv)
   else
       /* enable progress display */
       sys->switchS = 10000;
+  if (switchSS->count > 0)
+    {
+      /* enable state space graph output */
+      sys->switchStatespace = 1;
+    }
 
   /* TODO for now, warning for -m2 and non-clp */
   if (sys->match == 2 && !sys->clp)
@@ -612,8 +619,16 @@ MC_single (const System sys)
 int
 modelCheck (const System sys)
 {
+  if (sys->switchStatespace)
+    {
+      graphInit (sys);
+    }
   traverse (sys);		// start model checking
   timersPrint (sys);
+  if (sys->switchStatespace)
+    {
+      graphDone (sys);
+    }
   return (sys->failed);
 }
 

src/modelchecker.c

@@ -94,18 +94,18 @@ traverse (const System sys)
     }
 }
 
-/*
- * executeStep
- *
+//! Progress counters to next step.
+/**
  * Does not really execute anything, it's just bookkeeping, progressing
  * counters and such.
  *
- * If it returns TRUE, explore. If false, don't traverse.
+ *@returns If it returns TRUE, explore. If false, don't traverse.
  */
 
 int
 executeStep (const System sys, const int run)
 {
+  unsigned long int parentBuffer;
   Roledef runPoint;
   runPoint = runPointerGet (sys, run);
 #ifdef DEBUG
@@ -176,6 +176,13 @@ executeStep (const System sys, const int run)
 	  fprintf (stderr, " \r");
 	}
     }
+
+  /* the construction below always assumes MAX_GRAPH_STATES to be smaller than the unsigned long it, which seems realistic. */
+  if (sys->switchStatespace && sys->statesHigh == 0 && sys->statesLow < MAX_GRAPH_STATES)
+    {
+      /* display graph */
+      graphNode (sys);
+    }
   return 1;
 }
 
@@ -201,7 +208,16 @@ explorify (const System sys, const int run)
 
   if (executeStep (sys, run))
     {
+      /* traverse the system after the step */
+      /* be sure to do bookkeeping for the parent state */
+      unsigned long int parentBuffer;
+
+      parentBuffer = sys->parentState;
+      sys->parentState = sys->statesLow;
+
       flag = traverse (sys);
+
+      sys->parentState = parentBuffer;
     }
   else
     {

src/modelchecker.h

@@ -1,3 +1,4 @@
+#define MAX_GRAPH_STATES 1000	//!< Maximum number of state space nodes drawn
 int traverse (const System oldsys);
 int explorify (const System sys, const int run);
 int executeStep (const System sys, const int run);

src/output.c

@@ -490,3 +490,63 @@ attackDisplay (System sys)
       attackDisplayAscii (sys);
     }
 }
+
+/* state space graph section */
+void graphInit (System sys)
+{
+  Termlist tl;
+
+  /* drawing state space. start with initial node 0 */
+  printf ("digraph Statespace {\n");
+  printf ("\tn0 [shape=box,label=\"M0: ");
+  tl = knowledgeSet (sys->know);
+  termlistPrint (tl);
+  termlistDelete (tl);
+  printf ("\"];\n");
+}
+
+void graphDone (System sys)
+{
+  /* drawing state space. close up. */
+  printf ("}\n");
+}
+
+void graphNode (System sys)
+{
+  Termlist newtl;
+
+  /* add node */
+  printf ("\tn%li [shape=", sys->statesLow);
+  
+  newtl = knowledgeNew (sys->traceKnow[sys->step-1], sys->traceKnow[sys->step]);
+  if (newtl != NULL)
+    {
+      /* knowledge added */
+      printf ("box,label=\"M + ");
+      termlistPrint (newtl);
+      termlistDelete (newtl);
+      printf ("\"");
+    }
+  else
+    {
+      /* no added knowledge */
+      printf ("point");
+    }
+  printf ("];\n");
+
+  /* add edge */
+  printf ("\tn%li -> n%li ", sys->parentState, sys->statesLow);
+  /* add label */
+  printf ("[label=\"");
+  roledefPrint (sys->traceEvent[sys->step - 1]);
+  printf ("\#%i", sys->traceRun[sys->step -1]);
+  printf ("\"");
+  /* a choose? */
+  if (sys->traceEvent[sys->step -1]->type == READ && sys->traceEvent[sys->step -1]->internal)
+    {
+      printf (",color=blue");
+      //printf (",style=dotted");
+    }
+  printf ("]");
+  printf (";\n");
+}

src/output.h

@@ -5,5 +5,8 @@
 
 void tracePrint(System sys);
 void attackDisplay(System sys);
+void graphInit (System sys);
+void graphDone (System sys);
+void graphNode (System sys);
 
 #endif

src/runs.c

@@ -63,6 +63,7 @@ systemInit ()
   /* switches */
   sys->porparam = 0;		// multi-purpose parameter
   sys->latex = 0;		// latex output?
+  sys->switchStatespace = 0;
 
   /* set illegal traversal by default, to make sure it is set
      later */
@@ -108,6 +109,7 @@ systemReset (const System sys)
   /* some initial counters */
   sys->statesLow = 0;		// number of explored states
   sys->statesHigh = 0;		// this is not as ridiculous as it might seem
+  sys->parentState = 0;
   sys->explore = 1;		// do explore the space
   sys->claims = 0;		// number of claims encountered
   sys->failed = 0;		// number of failed claims
@@ -292,7 +294,7 @@ roledefPrint (Roledef rd)
     }
   if (globalLatex)
     printf ("$");
-  printf ("\t(");
+  printf ("(");
   termPrint (rd->from);
   printf (",");
   if (rd->type == CLAIM)

src/runs.h

@@ -211,6 +211,7 @@ 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 switchStatespace;		//!< Output statespace for dot package
   //! Latex output switch.
   /**
    * Obsolete. Use globalLatex instead.
@@ -223,11 +224,13 @@ struct system
   int explore;			//!< Boolean: explore states after actions or not.
 
   /* counters */
-  unsigned long int statesLow;
-  unsigned long int statesHigh;
+  unsigned long int statesLow;	//!< State number (low)
+  unsigned long int statesHigh; //!< State number (high)
   unsigned long int claims;	//!< Number of claims encountered.
   unsigned long int failed;	//!< Number of claims failed.
 
+  unsigned long int parentState; //!< Parent state number
+
   /* matching */
   int match;			//!< Matching type.
   int clp;			//!< Do we use clp?