- Improved the trace highlight in the state space, but it isn't as I

want it yet.

src/modelchecker.c

@@ -176,6 +176,8 @@ executeStep (const System sys, const int run)
 	}
     }
 
+  /* store new node numbder */
+  sys->traceNode[sys->step] = sys->statesLow;
   /* 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)
     {
@@ -208,15 +210,8 @@ 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->traceNode[sys->step];
-      sys->traceNode[sys->step] = sys->statesLow;
 
       flag = traverse (sys);
-
-      sys->traceNode[sys->step] = parentBuffer;
     }
   else
     {
@@ -1048,7 +1043,8 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
   /* mark the path in the state graph? */
   if (sys->switchStatespace)
     {
-      graphPath (sys,"shape=doubleoctagon,color=red","color=red");
+      graphNodePath (sys,length,"shape=parallelogram,color=red");
+      graphEdgePath (sys,length-1,"color=red");
     }
 
   /* Copy the current trace to the buffer, if the new one is shorter than the previous one. */
@@ -1084,7 +1080,7 @@ executeTry (const System sys, int run)
 
   runPoint = runPointerGet (sys, run);
   sys->traceEvent[sys->step] = runPoint;	// store for later usage, problem: variables are substituted later...
-  sys->traceRun[sys->step] = run;	// same
+  sys->traceRun[sys->step] = run;		// same
 
   if (runPoint == NULL)
     {

src/output.c

@@ -571,26 +571,38 @@ void graphNode (const System sys)
   printf (";\n");
 }
 
-void graphPath (const System sys, const char* nodepar, const char* edgepar)
+void graphNodePath (const System sys, const int length, const char* nodepar)
 {
   int i;
+  unsigned long int thisNode;
 
   i = 0;
-  while (i < sys->step)
+  while (i < length)
     {
+      /* determine node number */
+      thisNode = sys->traceNode[i];
+
       /* color node */
-      if (nodepar != NULL)
-	{
-          printf ("\tn%li [%s];\n", sys->traceNode[i], nodepar);
-	}
-      /* color edge */
-      if (edgepar != NULL)
-	{
-      	  printf ("\tn%li -> n%li [%s];\n",
-	          sys->traceNode[i], 
-	          sys->traceNode[i+1],
-	          edgepar);
-	}
+      printf ("\tn%li [%s];\n", thisNode, nodepar);
+      i++;
+    }
+}
+
+void graphEdgePath (const System sys, const int length, const char* edgepar)
+{
+  int i;
+  unsigned long int thisNode, prevNode;
+
+  i = 0;
+  prevNode = sys->traceNode[i];
+  while (i < length)
+    {
+      /* determine node number */
+      thisNode = sys->traceNode[i+1];
+
+      /* color edge */
+      printf ("\tn%li -> n%li [%s];\n", prevNode, thisNode, edgepar);
+      prevNode = thisNode;
       i++;
     }
 }

src/output.h

@@ -8,7 +8,9 @@ void attackDisplay(const System sys);
 void graphInit (const System sys);
 void graphDone (const System sys);
 void graphNode (const System sys);
-void graphPath (const System sys, const char* nodepar, const char*
+void graphNodePath (const System sys, const int length, const char*
+		nodepar);
+void graphEdgePath (const System sys, const int length, const char*
 		edgepar);
 
 #endif