- Started working on coloring of the attack trace in the state space.

src/modelchecker.c

@@ -212,12 +212,12 @@ explorify (const System sys, const int run)
       /* be sure to do bookkeeping for the parent state */
       unsigned long int parentBuffer;
 
-      parentBuffer = sys->parentState;
+      parentBuffer = sys->traceNode[sys->step - 1];
-      sys->parentState = sys->statesLow;
+      sys->traceNode[sys->step - 1] = sys->statesLow;
 
       flag = traverse (sys);
 
-      sys->parentState = parentBuffer;
+      sys->traceNode[sys->step - 1] = parentBuffer;
     }
   else
     {
@@ -1046,6 +1046,12 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
   /* Count the violations */
   sys->failed++;
 
+  /* mark the path in the state graph? */
+  if (sys->switchStatespace)
+    {
+      graphPath (sys,"color=red");
+    }
+
   /* Copy the current trace to the buffer, if the new one is shorter than the previous one. */
   if (sys->attack == NULL || length < sys->attack->reallength)
     {

src/output.c

@@ -491,8 +491,13 @@ attackDisplay (System sys)
     }
 }
 
-/* state space graph section */
+/* 
-void graphInit (System sys)
+ *-------------------------------------------
+ * state space graph section
+ *-------------------------------------------
+ */
+
+void graphInit (const System sys)
 {
   Termlist tl;
 
@@ -512,18 +517,23 @@ void graphInit (System sys)
   printf ("\"];\n");
 }
 
-void graphDone (System sys)
+void graphDone (const System sys)
 {
   /* drawing state space. close up. */
   printf ("}\n");
 }
 
-void graphNode (System sys)
+void graphNode (const System sys)
 {
   Termlist newtl;
+  unsigned long int thisNode, parentNode;
+
+  /* determine node numbers */
+  parentNode = sys->traceNode[sys->step - 1];
+  thisNode = sys->statesLow;
 
   /* add node */
-  printf ("\tn%li [shape=", sys->statesLow);
+  printf ("\tn%li [shape=", thisNode);
   
   newtl = knowledgeNew (sys->traceKnow[sys->step-1], sys->traceKnow[sys->step]);
   if (newtl != NULL)
@@ -542,7 +552,7 @@ void graphNode (System sys)
   printf ("];\n");
 
   /* add edge */
-  printf ("\tn%li -> n%li ", sys->parentState, sys->statesLow);
+  printf ("\tn%li -> n%li ", parentNode, thisNode);
   /* add label */
   printf ("[label=\"");
   roledefPrint (sys->traceEvent[sys->step - 1]);
@@ -557,3 +567,15 @@ void graphNode (System sys)
   printf ("]");
   printf (";\n");
 }
+
+void graphPath (const System sys, const char* params)
+{
+  int i;
+
+  i = 0;
+  while (i < sys->step)
+    {
+      printf ("\tn%i [%s]\n", sys->traceNode[i], params);
+      i++;
+    }
+}

src/output.h

@@ -3,10 +3,11 @@
 
 #include "runs.h"
 
-void tracePrint(System sys);
+void tracePrint(const System sys);
-void attackDisplay(System sys);
+void attackDisplay(const System sys);
-void graphInit (System sys);
+void graphInit (const System sys);
-void graphDone (System sys);
+void graphDone (const System sys);
-void graphNode (System sys);
+void graphNode (const System sys);
+void graphPath (const System sys, const char* params);
 
 #endif

src/runs.c

@@ -156,6 +156,7 @@ systemDone (System sys)
   memFree (sys->traceEvent, s * sizeof (Roledef));
   memFree (sys->traceRun, s * sizeof (int));
   memFree (sys->traceKnow, s * sizeof (Knowledge));
+  memFree (sys->traceNode, s * sizeof (unsigned long int));
 
   /* clear roledefs */
   for (run = 0; run < sys->maxruns; run++)
@@ -644,6 +645,7 @@ systemStart (System sys)
   sys->traceEvent = memAlloc (s * sizeof (Roledef));
   sys->traceRun = memAlloc (s * sizeof (int));
   sys->traceKnow = memAlloc (s * sizeof (Knowledge));
+  sys->traceNode = memAlloc (s * sizeof (unsigned long int));
 
   /* clear, for niceties */
   for (i = 0; i < s; i++)
@@ -651,6 +653,7 @@ systemStart (System sys)
       sys->traceEvent[i] = NULL;
       sys->traceRun[i] = 0;
       sys->traceKnow[i] = NULL;
+      sys->traceNode[i] = 0;
     }
 }
 

src/runs.h

@@ -250,6 +250,7 @@ struct system
   Roledef *traceEvent;		//!< Trace roledefs: MaxRuns * maxRoledef
   int *traceRun;		//!< Trace run ids: MaxRuns * maxRoledef
   Knowledge *traceKnow;		//!< Trace intruder knowledge: Maxruns * maxRoledef
+  unsigned long int *traceNode;	//!< Trace node traversal
 
   /* POR reduction assistance */
   int PORphase;			//!< -1: init (all sends), 0...: recurse reads