- Improved dot class output.

src/depend.c

@@ -542,3 +542,29 @@ eventNode (const int r, const int e)
 {
   return eventtonode (currentdepgraph, r, e);
 }
+
+//! Iterate over any preceding events
+int
+iteratePrecedingEvents (const System sys, int (*func) (int run, int ev),
+			const int run, const int ev)
+{
+  int run2;
+
+  for (run2 = 0; run2 < sys->maxruns; run2++)
+    {
+      int ev2;
+
+      for (ev2 = 0; ev2 < sys->runs[run2].step; ev2++)
+	{
+	  if (isDependEvent (run2, ev2, run, ev))
+	    {
+	      if (!func (run2, ev2))
+		{
+		  return false;
+		}
+	      break;
+	    }
+	}
+    }
+  return true;
+}

src/depend.h

@@ -38,5 +38,7 @@ void setDependEvent (const int r1, const int e1, const int r2, const int e2);
 int hasCycle ();
 int eventNode (const int r, const int e);
 int nodeCount (void);
+int iteratePrecedingEvents (const System sys, int (*func) (int run, int ev),
+			    const int run, const int ev);
 
 #endif

src/dotout.c

@@ -3,6 +3,7 @@
 #include "system.h"
 #include "switches.h"
 #include "arachne.h"
+#include "binding.h"
 #include "depend.h"
 
 extern Protocol INTRUDER;	// Pointers, to be set by the Init of arachne.c
@@ -16,6 +17,28 @@ extern Role I_RRSD;
 #define length		step
 
 
+//! Draw node
+void
+node (const System sys, const int run, const int index)
+{
+  if (sys->runs[run].protocol == INTRUDER)
+    {
+      if (sys->runs[run].role == I_M)
+	{
+	  eprintf ("m0");
+	}
+      else
+	{
+	  eprintf ("i%i", run);
+	}
+    }
+  else
+    {
+      eprintf ("r%ii%i", run, index);
+    }
+}
+
+
 //! Determine ranks for all nodes
 /**
  * Some crude algorithm I sketched on the blackboard.
@@ -78,6 +101,40 @@ graph_ranks (int *ranks, int nodes)
 }
 
 
+//! Iterate over events (in non-intruder runs) in which some value term occurs first.
+// Function should return true for iteration to continue.
+int
+iterate_first_regular_occurrences (const System sys,
+				   int (*func) (int run, int ev),
+				   const Term t)
+{
+  int run;
+
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      if (sys->runs[run].protocol != INTRUDER)
+	{
+	  int ev;
+	  Roledef rd;
+
+	  rd = sys->runs[run].start;
+	  for (ev = 0; ev < sys->runs[run].step; ev++)
+	    {
+	      if (termSubTerm (rd->from, t) ||
+		  termSubTerm (rd->to, t) || termSubTerm (rd->message, t))
+		{
+		  // Allright, t occurs here in this run first
+		  if (!func (run, ev))
+		    {
+		      return false;
+		    }
+		  break;
+		}
+	    }
+	}
+    }
+  return true;
+}
 
 //! Iterate over all events that have an incoming arrow to the current one (forgetting the intruder for a moment)
 void
@@ -236,6 +293,320 @@ iterate_outgoing_arrows (const System sys, void (*func) (), const int run,
     }
 }
 
+
+//! Draw the dependencies (returns from_intruder_count)
+int
+drawBindings (const System sys)
+{
+  int run;
+  int from_intruder_count;
+
+  // We now determine them ourselves between existing runs
+  run = 0;
+  from_intruder_count = 0;
+  while (run < sys->maxruns)
+    {
+      if (sys->runs[run].protocol != INTRUDER)
+	{
+	  int ev;
+
+	  ev = 0;
+	  while (ev < sys->runs[run].length)
+	    {
+	      int incoming_arrow_count;
+
+	      void incoming_arrow (int run2, int ev2)
+	      {
+		Roledef rd, rd2;
+
+		incoming_arrow_count++;
+		/*
+		 * We have decided to draw this binding,
+		 * from run2,ev2 to run,ev
+		 * However, me might need to decide some colouring for this node.
+		 */
+		eprintf ("\t");
+		node (sys, run2, ev2);
+		eprintf (" -> ");
+		node (sys, run, ev);
+		eprintf (" ");
+		// decide color
+		rd = roledef_shift (sys->runs[run].start, ev);
+		rd2 = roledef_shift (sys->runs[run2].start, ev2);
+		if (rd->type == CLAIM)
+		  {
+		    // Towards a claim, so only indirect dependency
+		    eprintf ("[color=cornflowerblue]");
+		  }
+		else
+		  {
+		    // Not towards claim should imply towards read,
+		    // but we check it to comply with future stuff.
+		    if (rd->type == READ && rd2->type == SEND)
+		      {
+			// We want to distinguish where it is from a 'broken' send
+			if (isTermEqual (rd->message, rd2->message))
+			  {
+			    if (isTermEqual
+				(rd->from, rd2->from)
+				&& isTermEqual (rd->to, rd2->to))
+			      {
+				// Wow, a perfect match. Leave the arrow as-is :)
+				eprintf ("[color=darkgreen]");
+			      }
+			    else
+			      {
+				// Same message, different people
+				eprintf
+				  ("[label=\"redirect\",color=darkorange2]");
+			      }
+			  }
+			else
+			  {
+			    // Not even the same message, intruder construction
+			    eprintf ("[label=\"construct\",color=red]");
+			  }
+		      }
+		  }
+		// close up
+		eprintf (";\n");
+	      }
+
+	      incoming_arrow_count = 0;
+	      iterate_incoming_arrows (sys, incoming_arrow, run, ev);
+
+	      ev++;
+	    }
+	}
+      run++;
+    }
+  return from_intruder_count;
+}
+
+
+//! Draw simple runs
+void
+drawSimpleRuns (const System sys)
+{
+  int run;
+
+  // Draw graph
+  // First, all simple runs
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      Roledef rd;
+      int index;
+
+      index = 0;
+      rd = sys->runs[run].start;
+      if (sys->runs[run].protocol != INTRUDER && sys->runs[run].length > 0)
+	{
+	  // Regular run
+
+	  /* DISABLED subgraphs
+	     eprintf ("\tsubgraph cluster_run%i {\n", run);
+	     eprintf ("\t\tlabel = \"");
+	     eprintf ("#%i: ", run);
+	     termPrint (sys->runs[run].protocol->nameterm);
+	     eprintf (", ");
+	     agentsOfRunPrint (sys, run);
+	     eprintf ("\";\n", run);
+	     if (run == 0)
+	     {
+	     eprintf ("\t\tcolor = red;\n");
+	     }
+	     else
+	     {
+	     eprintf ("\t\tcolor = blue;\n");
+	     }
+	   */
+
+
+	  // Display the respective events
+	  while (index < sys->runs[run].length)
+	    {
+	      // Print node itself
+	      eprintf ("\t\t");
+	      node (sys, run, index);
+	      eprintf (" [");
+	      if (run == 0 && index == sys->current_claim->ev)
+		{
+		  eprintf
+		    ("style=filled,fillcolor=mistyrose,color=salmon,shape=doubleoctagon,");
+		}
+	      else
+		{
+		  eprintf ("shape=box,");
+		}
+	      eprintf ("label=\"");
+	      roledefPrintShort (rd);
+	      eprintf ("\"]");
+	      eprintf (";\n");
+
+	      // Print binding to previous node
+	      if (index > sys->runs[run].firstReal)
+		{
+		  // index > 0
+		  eprintf ("\t\t");
+		  node (sys, run, index - 1);
+		  eprintf (" -> ");
+		  node (sys, run, index);
+		  eprintf (" [style=\"bold\", weight=\"10.0\"]");
+		  eprintf (";\n");
+		}
+	      else
+		{
+		  // index <= firstReal
+		  if (index == sys->runs[run].firstReal)
+		    {
+		      // index == firstReal
+		      Roledef rd;
+		      int send_before_read;
+		      int done;
+
+		      // Determine if it is an active role or note
+		      /**
+		       *@todo note that this will probably become a standard function call for role.h
+		       */
+		      rd =
+			roledef_shift (sys->runs[run].start,
+				       sys->runs[run].firstReal);
+		      done = 0;
+		      send_before_read = 0;
+		      while (!done && rd != NULL)
+			{
+			  if (rd->type == READ)
+			    {
+			      done = 1;
+			    }
+			  if (rd->type == SEND)
+			    {
+			      done = 1;
+			      send_before_read = 1;
+			    }
+			  rd = rd->next;
+			}
+		      // Draw the first box
+		      // This used to be drawn only if done && send_before_read, now we always draw it.
+		      eprintf ("\t\ts%i [label=\"Run %i: ", run, run);
+		      termPrint (sys->runs[run].protocol->nameterm);
+		      eprintf (", ");
+		      termPrint (sys->runs[run].role->nameterm);
+		      eprintf ("\\n");
+		      agentsOfRunPrint (sys, run);
+		      eprintf ("\", shape=diamond];\n");
+		      eprintf ("\t\ts%i -> ", run);
+		      node (sys, run, index);
+		      eprintf (" [weight=\"10.0\"];\n");
+		    }
+		}
+	      index++;
+	      rd = rd->next;
+	    }
+	  /* DISABLED subgraphs
+	     eprintf ("\t}\n");
+	   */
+	}
+      run++;
+    }
+}
+
+//! Choose term node
+void
+chooseTermNode (const Term t)
+{
+  eprintf ("CHOOSE");
+  {
+    char *rsbuf;
+
+    rsbuf = RUNSEP;
+    RUNSEP = "x";
+    termPrint (t);
+    RUNSEP = rsbuf;
+  }
+}
+
+//! Show intruder choices
+void
+drawIntruderChoices (const System sys)
+{
+  Termlist shown;
+  List bl;
+
+  shown = NULL;
+  for (bl = sys->bindings; bl != NULL; bl = bl->next)
+    {
+      Binding b;
+
+      b = (Binding) bl->data;
+      if ((!b->blocked) && (!b->done) && isTermVariable (b->term))
+	{
+	  /*
+	   * If the binding is not blocked, but also not done,
+	   * the intruder can apparently satisfy it at will.
+	   */
+
+	  if (!inTermlist (shown, b->term))
+	    {
+	      int firsthere (int run, int ev)
+	      {
+					/**
+					 * @todo This is not very efficient,
+					 * but maybe that is not really
+					 * needed here.
+					 */
+		int notearlier (int run2, int ev2)
+		{
+		  if (sys->runs[run2].protocol != INTRUDER)
+		    {
+		      return (!roledefSubTerm
+			      (eventRoledef (sys, run2, ev2), b->term));
+		    }
+		  else
+		    {
+		      return true;
+		    }
+		}
+
+		if (iteratePrecedingEvents (sys, notearlier, run, ev))
+		  {
+		    eprintf ("\t");
+		    chooseTermNode (b->term);
+		    eprintf (" -> ");
+		    node (sys, run, ev);
+		    eprintf (" [color=\"darkgreen\"];\n");
+		  }
+		return true;
+	      }
+
+	      // If the first then we add a header
+	      if (shown == NULL)
+		{
+		  eprintf ("// Showing intruder choices.\n");
+		}
+	      // Not in the list, show new node
+	      shown = termlistAdd (shown, b->term);
+	      eprintf ("\t");
+	      chooseTermNode (b->term);
+	      eprintf (" [label=\"Class: any ");
+	      termPrint (b->term);
+	      eprintf ("\",color=\"darkgreen\"];\n");
+
+	      iterate_first_regular_occurrences (sys, firsthere, b->term);
+	    }
+	}
+
+    }
+
+  if (shown != NULL)
+    {
+      eprintf ("\n");
+    }
+  termlistDelete (shown);
+}
+
+
 //! Display the current semistate using dot output format.
 /**
  * This is not as nice as we would like it. Furthermore, the function is too big.
@@ -251,25 +622,6 @@ dotSemiState (const System sys)
   int from_intruder_count;
   int nodes;
 
-  void node (const int run, const int index)
-  {
-    if (sys->runs[run].protocol == INTRUDER)
-      {
-	if (sys->runs[run].role == I_M)
-	  {
-	    eprintf ("m0");
-	  }
-	else
-	  {
-	    eprintf ("i%i", run);
-	  }
-      }
-    else
-      {
-	eprintf ("r%ii%i", run, index);
-      }
-  }
-
   // Open graph
   attack_number++;
   eprintf ("digraph semiState%i {\n", attack_number);
@@ -282,8 +634,6 @@ dotSemiState (const System sys)
   termPrint (sys->current_claim->type);
   eprintf ("\";\n");
 
-  from_intruder_count = 0;	// number of terms that can come from the initial knowledge
-
   // Needed for the bindings later on: create graph
 
   nodes = nodeCount ();
@@ -347,218 +697,10 @@ dotSemiState (const System sys)
   }
 #endif
 
-  // Draw graph
+  // First, simple runs
-  // First, all simple runs
+  drawSimpleRuns (sys);
-  run = 0;
-  while (run < sys->maxruns)
-    {
-      Roledef rd;
-      int index;
-
-      index = 0;
-      rd = sys->runs[run].start;
-      if (sys->runs[run].protocol != INTRUDER && sys->runs[run].length > 0)
-	{
-	  // Regular run
-
-	  /* DISABLED subgraphs
-	     eprintf ("\tsubgraph cluster_run%i {\n", run);
-	     eprintf ("\t\tlabel = \"");
-	     eprintf ("#%i: ", run);
-	     termPrint (sys->runs[run].protocol->nameterm);
-	     eprintf (", ");
-	     agentsOfRunPrint (sys, run);
-	     eprintf ("\";\n", run);
-	     if (run == 0)
-	     {
-	     eprintf ("\t\tcolor = red;\n");
-	     }
-	     else
-	     {
-	     eprintf ("\t\tcolor = blue;\n");
-	     }
-	   */
-
-
-	  // Display the respective events
-	  while (index < sys->runs[run].length)
-	    {
-	      // Print node itself
-	      eprintf ("\t\t");
-	      node (run, index);
-	      eprintf (" [");
-	      if (run == 0 && index == sys->current_claim->ev)
-		{
-		  eprintf
-		    ("style=filled,fillcolor=mistyrose,color=salmon,shape=doubleoctagon,");
-		}
-	      else
-		{
-		  eprintf ("shape=box,");
-		}
-	      eprintf ("label=\"");
-	      roledefPrintShort (rd);
-	      eprintf ("\"]");
-	      eprintf (";\n");
-
-	      // Print binding to previous node
-	      if (index > sys->runs[run].firstReal)
-		{
-		  // index > 0
-		  eprintf ("\t\t");
-		  node (run, index - 1);
-		  eprintf (" -> ");
-		  node (run, index);
-		  eprintf (" [style=\"bold\", weight=\"10.0\"]");
-		  eprintf (";\n");
-		}
-	      else
-		{
-		  // index <= firstReal
-		  if (index == sys->runs[run].firstReal)
-		    {
-		      // index == firstReal
-		      Roledef rd;
-		      int send_before_read;
-		      int done;
-
-		      // Determine if it is an active role or note
-		      /**
-		       *@todo note that this will probably become a standard function call for role.h
-		       */
-		      rd =
-			roledef_shift (sys->runs[run].start,
-				       sys->runs[run].firstReal);
-		      done = 0;
-		      send_before_read = 0;
-		      while (!done && rd != NULL)
-			{
-			  if (rd->type == READ)
-			    {
-			      done = 1;
-			    }
-			  if (rd->type == SEND)
-			    {
-			      done = 1;
-			      send_before_read = 1;
-			    }
-			  rd = rd->next;
-			}
-		      // Draw the first box
-		      // This used to be drawn only if done && send_before_read, now we always draw it.
-		      eprintf ("\t\ts%i [label=\"Run %i: ", run, run);
-		      termPrint (sys->runs[run].protocol->nameterm);
-		      eprintf (", ");
-		      termPrint (sys->runs[run].role->nameterm);
-		      eprintf ("\\n");
-		      agentsOfRunPrint (sys, run);
-		      eprintf ("\", shape=diamond];\n");
-		      eprintf ("\t\ts%i -> ", run);
-		      node (run, index);
-		      eprintf (" [weight=\"10.0\"];\n");
-		    }
-		}
-	      index++;
-	      rd = rd->next;
-	    }
-	  /* DISABLED subgraphs
-	     eprintf ("\t}\n");
-	   */
-	}
-      run++;
-    }
-
   // Second, all bindings.
-  // We now determine them ourselves between existing runs
+  from_intruder_count = drawBindings (sys);
-  run = 0;
-  while (run < sys->maxruns)
-    {
-      if (sys->runs[run].protocol != INTRUDER)
-	{
-	  int ev;
-
-	  ev = 0;
-	  while (ev < sys->runs[run].length)
-	    {
-	      int incoming_arrow_count;
-
-	      void incoming_arrow (int run2, int ev2)
-	      {
-		Roledef rd, rd2;
-
-		incoming_arrow_count++;
-		/*
-		 * We have decided to draw this binding,
-		 * from run2,ev2 to run,ev
-		 * However, me might need to decide some colouring for this node.
-		 */
-		eprintf ("\t");
-		node (run2, ev2);
-		eprintf (" -> ");
-		node (run, ev);
-		eprintf (" ");
-		// decide color
-		rd = roledef_shift (sys->runs[run].start, ev);
-		rd2 = roledef_shift (sys->runs[run2].start, ev2);
-		if (rd->type == CLAIM)
-		  {
-		    // Towards a claim, so only indirect dependency
-		    eprintf ("[color=cornflowerblue]");
-		  }
-		else
-		  {
-		    // Not towards claim should imply towards read,
-		    // but we check it to comply with future stuff.
-		    if (rd->type == READ && rd2->type == SEND)
-		      {
-			// We want to distinguish where it is from a 'broken' send
-			if (isTermEqual (rd->message, rd2->message))
-			  {
-			    if (isTermEqual
-				(rd->from, rd2->from)
-				&& isTermEqual (rd->to, rd2->to))
-			      {
-				// Wow, a perfect match. Leave the arrow as-is :)
-				eprintf ("[color=forestgreen]");
-			      }
-			    else
-			      {
-				// Same message, different people
-				eprintf
-				  ("[label=\"redirect\",color=darkorange2]");
-			      }
-			  }
-			else
-			  {
-			    // Not even the same message, intruder construction
-			    eprintf ("[label=\"construct\",color=red]");
-			  }
-		      }
-		  }
-		// close up
-		eprintf (";\n");
-	      }
-
-	      incoming_arrow_count = 0;
-	      iterate_incoming_arrows (sys, incoming_arrow, run, ev);
-	      /*
-	       * Currently disabled: generates too much garbage
-	       */
-	      if (false && incoming_arrow_count == 0)
-		{
-		  // No incoming arrows: can be generated from initial intruder knowledge
-
-		  from_intruder_count++;
-		  eprintf ("\tintruder -> ");
-		  node (run, ev);
-		  eprintf (";\n");
-		}
-
-	      ev++;
-	    }
-	}
-      run++;
-    }
 
   // Third, the intruder node (if needed)
   if (from_intruder_count > 0)
@@ -659,6 +801,9 @@ dotSemiState (const System sys)
       }
   }
 
+  // Intruder choices
+  drawIntruderChoices (sys);
+
 #ifdef DEBUG
   // Debug: print dependencies
   if (DEBUGL (3))

src/role.c

@@ -319,3 +319,18 @@ roledef_shift (Roledef rd, int i)
     }
   return rd;
 }
+
+// Check whether a term is a subterm of a roledef
+int
+roledefSubTerm (Roledef rd, Term tsub)
+{
+  if (rd == NULL)
+    {
+      return false;
+    }
+  else
+    {
+      return (termSubTerm (rd->from, tsub) ||
+	      termSubTerm (rd->to, tsub) || termSubTerm (rd->message, tsub));
+    }
+}

src/role.h

@@ -161,5 +161,6 @@ void rolesPrint (Role r);
 int roledef_iterate_events (Roledef rd, int (*func) ());
 int roledef_length (const Roledef rd);
 Roledef roledef_shift (Roledef rd, int i);
+int roledefSubTerm (Roledef rd, Term tsub);
 
 #endif

src/system.c

@@ -1413,3 +1413,10 @@ firstOccurrence (const System sys, const int r, Term t, int evtype)
 #endif
   return firste;
 }
+
+//! Get the roledef of an event
+Roledef
+eventRoledef (const System sys, const int run, const int ev)
+{
+  return roledef_shift (sys->runs[run].start, ev);
+}

src/system.h

@@ -194,6 +194,7 @@ int iterateEventsType (const System sys, const int run, const int evtype,
 int iterateLocalToOther (const System sys, const int myrun,
 			 int (*callback) (Term t));
 int firstOccurrence (const System sys, const int r, Term t, int evtype);
+Roledef eventRoledef (const System sys, const int run, const int ev);
 
 
 //! Equality for run structure naming

src/term.c

@@ -21,6 +21,7 @@
 
 /* public flag */
 int rolelocal_variable;
+char *RUNSEP;
 
 /* external definitions */
 
@@ -44,6 +45,7 @@ void
 termsInit (void)
 {
   rolelocal_variable = 0;
+  RUNSEP = "#";
   return;
 }
 
@@ -333,7 +335,7 @@ termPrint (Term term)
 	eprintf ("V");
       if (TermRunid (term) >= 0)
 	{
-	  eprintf ("#%i", TermRunid (term));
+	  eprintf ("%s%i", RUNSEP, TermRunid (term));
 	}
       if (term->subst != NULL)
 	{

src/term.h

@@ -208,4 +208,6 @@ void termSubstPrint (Term t);
 
 int iterateTermOther (const int myrun, Term t, int (*callback) (Term t));
 
+extern char *RUNSEP;		// by default, set to "#"
+
 #endif