From 03522b71089947d2c1414851a0dca07be6da7081 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Wed, 16 Jan 2008 11:55:15 +0100
Subject: [PATCH] Try to not draw duplicate arrows.

This cleans up some graphs rather nicely. There is only one potential
drawback (not observed in practive):
If two bindings have the same from/to, but different interpretations,
we might lose information. In particular the 'select' intermediate nodes might
pose a problem and we would be better off by not having any interpretation on
what is selected.
---
 src/binding.c | 25 ++++++++++++++++++++++++-
 src/binding.h |  1 +
 src/dotout.c  | 37 +++++++++++++++++++++++++++++--------
 3 files changed, 54 insertions(+), 9 deletions(-)

diff --git a/src/binding.c b/src/binding.c
index 9e071d5..f68e3a2 100644
--- a/src/binding.c
+++ b/src/binding.c
@@ -415,7 +415,30 @@ iterate_bindings (int (*func) (Binding b))
   return true;
 }
 
-
+//! Determine whether two bindings have the same source and destination
+int
+same_binding (const Binding b1, const Binding b2)
+{
+  if (b1 == b2)
+    {
+      return true;
+    }
+  if ((b1 != NULL) && (b2 != NULL))
+    {
+      if ((b1->done) && (b2->done))
+	{
+	  if ((b1->run_to == b2->run_to) && (b1->ev_to == b2->ev_to))
+	    {
+	      if ((b1->run_from == b2->run_from)
+		  && (b1->ev_from == b2->ev_from))
+		{
+		  return true;
+		}
+	    }
+	}
+    }
+  return false;
+}
 
 //! Iterate over preceding bindings (this does not include stuff bound to the same destination)
 /**
diff --git a/src/binding.h b/src/binding.h
index d694a07..ab7c9ba 100644
--- a/src/binding.h
+++ b/src/binding.h
@@ -51,6 +51,7 @@ void bindingDone ();
 
 int binding_print (Binding b);
 int valid_binding (Binding b);
+int same_binding (const Binding b1, const Binding b2);
 
 int goal_add (Term term, const int run, const int ev, const int level);
 int goal_add_fixed (Term term, const int run, const int ev, const int fromrun,
diff --git a/src/dotout.c b/src/dotout.c
index 31024f0..3cccff8 100644
--- a/src/dotout.c
+++ b/src/dotout.c
@@ -996,8 +996,6 @@ regularModifiedLabel (Binding b)
     }
 }
 
-//! 
-
 //! Draw a single binding
 void
 drawBinding (const System sys, Binding b)
@@ -1143,8 +1141,10 @@ int
 drawAllBindings (const System sys)
 {
   List bl;
+  List bldone;
   int fromintr;
 
+  bldone = NULL;
   fromintr = 0;
   for (bl = sys->bindings; bl != NULL; bl = bl->next)
     {
@@ -1157,16 +1157,36 @@ drawAllBindings (const System sys)
 	  // still show it somewhere.
 	  if (b->done)
 	    {
-	      // done, draw
-	      drawBinding (sys, b);
-	      // from intruder?
-	      if (sys->runs[b->run_from].protocol == INTRUDER)
+	      // Check whether we already drew it
+	      List bl2;
+	      int drawn;
+
+	      drawn = false;
+	      for (bl2 = bldone; bl2 != NULL; bl2 = bl2->next)
 		{
-		  if (sys->runs[b->run_from].role == I_M)
+		  if (same_binding (b, (Binding) bl2->data))
 		    {
-		      fromintr++;
+		      drawn = true;
+		      break;
 		    }
 		}
+
+	      if (!drawn)
+		{
+		  // done, draw
+		  drawBinding (sys, b);
+
+		  // from intruder?
+		  if (sys->runs[b->run_from].protocol == INTRUDER)
+		    {
+		      if (sys->runs[b->run_from].role == I_M)
+			{
+			  fromintr++;
+			}
+		    }
+		  // Add to drawn list
+		  bldone = list_add (bldone, b);
+		}
 	    }
 	  else
 	    {
@@ -1174,6 +1194,7 @@ drawAllBindings (const System sys)
 	    }
 	}
     }
+  list_destroy (bldone);	// bindings list
   return fromintr;
 }