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

@@ -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)
 /**

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,

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)
     {
@@ -1156,9 +1156,26 @@ drawAllBindings (const System sys)
 	  // if the binding is not done (class choice) we might
 	  // still show it somewhere.
 	  if (b->done)
+	    {
+	      // Check whether we already drew it
+	      List bl2;
+	      int drawn;
+
+	      drawn = false;
+	      for (bl2 = bldone; bl2 != NULL; bl2 = bl2->next)
+		{
+		  if (same_binding (b, (Binding) bl2->data))
+		    {
+		      drawn = true;
+		      break;
+		    }
+		}
+
+	      if (!drawn)
 		{
 		  // done, draw
 		  drawBinding (sys, b);
+
 		  // from intruder?
 		  if (sys->runs[b->run_from].protocol == INTRUDER)
 		    {
@@ -1167,6 +1184,9 @@ drawAllBindings (const System sys)
 			  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;
 }