From ae6b85f29058636001b36c14cee38e9bcd78aa43 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 13 Jul 2004 09:56:19 +0000
Subject: [PATCH] - Improved graph coloring etc.

---
 src/modelchecker.c |  8 ++++----
 src/output.c       | 18 +++++++++++++++---
 src/output.h       |  3 ++-
 3 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/src/modelchecker.c b/src/modelchecker.c
index 730e238..b132fc4 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -211,12 +211,12 @@ explorify (const System sys, const int run)
       /* be sure to do bookkeeping for the parent state */
       unsigned long int parentBuffer;
 
-      parentBuffer = sys->traceNode[sys->step - 1];
-      sys->traceNode[sys->step - 1] = sys->statesLow;
+      parentBuffer = sys->traceNode[sys->step];
+      sys->traceNode[sys->step] = sys->statesLow;
 
       flag = traverse (sys);
 
-      sys->traceNode[sys->step - 1] = parentBuffer;
+      sys->traceNode[sys->step] = parentBuffer;
     }
   else
     {
@@ -1048,7 +1048,7 @@ violateClaim (const System sys, int length, int claimev, Termlist reqt)
   /* mark the path in the state graph? */
   if (sys->switchStatespace)
     {
-      graphPath (sys,"color=red");
+      graphPath (sys,"shape=doubleoctagon,color=red","color=red");
     }
 
   /* Copy the current trace to the buffer, if the new one is shorter than the previous one. */
diff --git a/src/output.c b/src/output.c
index af513f8..725fdae 100644
--- a/src/output.c
+++ b/src/output.c
@@ -550,7 +550,7 @@ void graphNode (const System sys)
   else
     {
       /* no added knowledge */
-      printf ("point");
+      printf ("point,label=\"\"");
     }
   printf ("];\n");
 
@@ -571,14 +571,26 @@ void graphNode (const System sys)
   printf (";\n");
 }
 
-void graphPath (const System sys, const char* params)
+void graphPath (const System sys, const char* nodepar, const char* edgepar)
 {
   int i;
 
   i = 0;
   while (i < sys->step)
     {
-      printf ("\tn%li [%s];\n", sys->traceNode[i], params);
+      /* 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);
+	}
       i++;
     }
 }
diff --git a/src/output.h b/src/output.h
index c8642ca..686e88a 100644
--- a/src/output.h
+++ b/src/output.h
@@ -8,6 +8,7 @@ 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* params);
+void graphPath (const System sys, const char* nodepar, const char*
+		edgepar);
 
 #endif