From 5b527cbc9c002cd6d3d7e32c566ae5516b64ef06 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Thu, 30 Nov 2006 16:16:37 +0000
Subject: [PATCH] - Clearer output for intruder-generated terms.

---
 src/dotout.c | 64 ++++++++++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 60 insertions(+), 4 deletions(-)

diff --git a/src/dotout.c b/src/dotout.c
index 4bb1066..c33b3aa 100644
--- a/src/dotout.c
+++ b/src/dotout.c
@@ -100,7 +100,7 @@ printVisualRun (int rid)
   else
     {
       // >= sys->maxruns means intruder choice
-      eprintf ("%i", (rid - sys->maxruns + 1));
+      eprintf ("Intruder%i", (rid - sys->maxruns + 1));
     }
 }
 
@@ -111,6 +111,17 @@ termPrintRemap (const Term t)
   termPrintCustom (t, "", "", "(", ")", "\\{ ", " \\}", printVisualRun);
 }
 
+//! Remap term list
+void
+termlistPrintRemap (Termlist tl)
+{
+  while (tl != NULL)
+    {
+      termPrintRemap(tl->term);
+      tl = tl->next;
+    }
+}
+
 //! Print a term; if it is a variable, show that
 void
 explainVariable (Term t)
@@ -1689,13 +1700,58 @@ dotSemiState (const System mysys)
   from_intruder_count = drawAllBindings (sys);
 
   // Third, the intruder node (if needed)
-  if (from_intruder_count > 0)
+    {
+  /*
+   * Stupid brute analysis, can probably be done much more efficient, but
+   * this is not a timing critical bit, so we just do it like this.
+   */
+  Termlist found;
+  List bl;
+
+  // collect the intruder-generated constants
+  found = NULL;
+  for (bl = sys->bindings; bl != NULL; bl = bl->next)
+    {
+      Binding b;
+
+      b = (Binding) bl->data;
+      if (!b->blocked)
+	{
+	  int addsubterms(Term t)
+	    {
+	      if (TermRunid(t) >= sys->maxruns)
+		{
+                  // >= sys->maxruns means intruder choice
+	          found = termlistAddNew(found, t);
+		}
+	      return true;
+	    }
+
+	  term_iterate_open_leaves(b->term, addsubterms);
+	}
+    }
+
+  // now maybe we draw the node
+  if ((from_intruder_count > 0) || (found != NULL))
     {
       eprintf
-	("\tintruder [label=\"Initial intruder knowledge\", style=filled,fillcolor=\"");
+	("\tintruder [\n");
+      eprintf ("\t\tlabel=\"");
+      eprintf ("Initial intruder knowledge");
+      if (found != NULL)
+	{
+	  eprintf ("\\n");
+	  eprintf ("The intruder generates: ");
+	  termlistPrintRemap (found);
+	}
+      eprintf ("\",\n");
+      eprintf ("\t\tstyle=filled,fillcolor=\"");
       printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS);
-      eprintf ("\"];\n");
+      eprintf ("\"\n\t];\n");
     }
+  termlistDelete(found);
+    }
+
   // eprintf ("\t};\n");
 
   // For debugging we might add more stuff: full dependencies