#include <stdlib.h>
#include <limits.h>
#include "system.h"
#include "switches.h"
#include "arachne.h"
#include "binding.h"
#include "depend.h"
#include "debug.h"

extern Protocol INTRUDER;	// Pointers, to be set by the Init of arachne.c
extern Role I_M;		// Same here.
extern Role I_RRS;
extern Role I_RRSD;

#define INVALID		-1
#define isGoal(rd)	(rd->type == READ && !rd->internal)
#define isBound(rd)	(rd->bound)
#define length		step


#define CLAIMTEXTCOLOR "#ffffff"
#define CLAIMCOLOR "#000000"
#define GOODCOMMCOLOR "forestgreen"

#define INTRUDERCOLORH 18.0
#define INTRUDERCOLORL 0.65
#define INTRUDERCOLORS 0.9
#define RUNCOLORL1 0.90
#define RUNCOLORL2 0.65
#define RUNCOLORH1 (INTRUDERCOLORH + 360 - 10.0)
#define RUNCOLORH2 (INTRUDERCOLORH + 10.0)
#define RUNCOLORS1 0.8
#define RUNCOLORS2 0.6
#define RUNCOLORDELTA 0.2	// maximum hue delta between roles (0.2): smaller means role colors of a protocol become more similar.
#define RUNCOLORCONTRACT 0.8	// contract from protocol edges: smaller means more distinction between protocols.
#define UNTRUSTEDCOLORS 0.4

/*
 * Dot output
 *
 *
 * The algorithm itself is not very complicated; because the semi-bundles have
 * bindings etcetera, a graph can be draw quickly and efficiently.
 *
 * Interesting issues:
 *
 * Binding annotations are only drawn if they don't connect with regular
 * events, and when the item does not occur in any previous binding, it might
 * be connected to the initial intruder knowledge.
 *
 * Color management is quite involved. We draw identical protocols in similar
 * color schemes.  A color scheme is a gradient between two colors, evenly
 * spread over all the runs.
 */

static System sys = NULL;

/*
 * code
 */

void
printVisualRun (int rid)
{
  int run;
  int displayi;
  int displayr;
  int display;

  if (rid < sys->maxruns)
    {
      // < sys->maxruns means normal thing (not from makeTraceConcrete)
      displayi = 0;
      displayr = 0;
      for (run = 0; run < rid; run++)
	{
	  if (sys->runs[run].protocol != INTRUDER)
	    {
	      displayr++;
	    }
	  else
	    {
	      displayi++;
	    }
	}
      if (sys->runs[rid].protocol == INTRUDER)
	{
	  display = sys->maxruns + displayi + 1;
	}
      else
	{
	  display = displayr + 1;
	}
      eprintf ("#%i", display);
    }
  else
    {
      // >= sys->maxruns means intruder choice
      eprintf ("%i", (rid - sys->maxruns + 1));
    }
}

//! Remap term stuff
void
termPrintRemap (const Term t)
{
  termPrintCustom (t, "", "", "(", ")", "\\{ ", " \\}", printVisualRun);
}

//! Print a term; if it is a variable, show that
void
explainVariable (Term t)
{
  t = deVar (t);
  if (realTermVariable (t))
    {
      eprintf ("any ");
      if (t->roleVar)
	{
	  eprintf ("agent ");
	}
      termPrintRemap (t);
      if (!t->roleVar)
	{
	  if (switches.match == 0 && t->stype != NULL)
	    {
	      Termlist tl;

	      eprintf (" of type ");
	      for (tl = t->stype; tl != NULL; tl = tl->next)
		{
		  termPrintRemap (tl->term);
		  if (tl->next != NULL)
		    {
		      eprintf (",");
		    }
		}
	    }
	}
    }
  else
    {
      termPrintRemap (t);
    }
}

//! 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 ("intruder");
	}
      else
	{
	  eprintf ("ri%i", run);
	}
    }
  else
    {
      eprintf ("r%ii%i", run, index);
    }
}

//! Draw arrow
void
arrow (const System sys, Binding b)
{
  node (sys, b->run_from, b->ev_from);
  eprintf (" -> ");
  node (sys, b->run_to, b->ev_to);
}

//! Redirect node
void
redirNode (const System sys, Binding b)
{
  eprintf ("redir_");
  node (sys, b->run_from, b->ev_from);
  node (sys, b->run_to, b->ev_to);
}

//! Roledef draw
void
roledefDraw (Roledef rd)
{
  void optlabel (void)
  {
    Term label;

    label = rd->label;
    if (label != NULL)
      {
	if (realTermTuple (label))
	  {
	    label = TermOp2 (label);
	  }
	eprintf ("_");
	termPrintRemap (label);
      }
  }

  if (rd->type == READ)
    {
      eprintf ("read");
      optlabel ();
      eprintf (" from ");
      termPrintRemap (rd->from);
      eprintf ("\\n");
      termPrintRemap (rd->message);
    }
  if (rd->type == SEND)
    {
      eprintf ("send");
      optlabel ();
      eprintf (" to ");
      termPrintRemap (rd->to);
      eprintf ("\\n");
      termPrintRemap (rd->message);
    }
  if (rd->type == CLAIM)
    {
      eprintf ("claim");
      optlabel ();
      eprintf ("\\n");
      termPrintRemap (rd->to);
      if (rd->message != NULL)
	{
	  eprintf (" : ");
	  termPrintRemap (rd->message);
	}
    }
}

//! Choose term node
void
chooseTermNode (const Term t)
{
  eprintf ("CHOOSE");
  {
    char *rsbuf;

    rsbuf = RUNSEP;
    RUNSEP = "x";
    termPrint (t);
    RUNSEP = rsbuf;
  }
}

//! Value for hlsrgb conversion
static double
hlsValue (double n1, double n2, double hue)
{
  if (hue > 360.0)
    hue -= 360.0;
  else if (hue < 0.0)
    hue += 360.0;
  if (hue < 60.0)
    return n1 + (n2 - n1) * hue / 60.0;
  else if (hue < 180.0)
    return n2;
  else if (hue < 240.0)
    return n1 + (n2 - n1) * (240.0 - hue) / 60.0;
  else
    return n1;
}

//! hls to rgb conversion
void
hlsrgb (int *r, int *g, int *b, double h, double l, double s)
{
  double m1, m2;

  int bytedouble (double d)
  {
    double x;

    x = 255.0 * d;
    if (x <= 0)
      return 0;
    else if (x >= 255.0)
      return 255;
    else
      return (int) x;
  }

  while (h >= 360.0)
    h -= 360.0;
  while (h < 0)
    h += 360.0;
  m2 = (l <= 0.5) ? (l * (l + s)) : (l + s - l * s);
  m1 = 2.0 * l - m2;
  if (s == 0.0)
    {
      *r = *g = *b = bytedouble (l);
    }
  else
    {
      *r = bytedouble (hlsValue (m1, m2, h + 120.0));
      *g = bytedouble (hlsValue (m1, m2, h));
      *b = bytedouble (hlsValue (m1, m2, h - 120.0));
    }
}

//! print color from h,l,s triplet
void
printColor (double h, double l, double s)
{
  int r, g, b;

  hlsrgb (&r, &g, &b, h, l, s);
  eprintf ("#%02x%02x%02x", r, g, b);
}


//! Set local buffer with the correct color for this run.
/**
 * Determines number of protocols, shifts to the right color pair, and colors
 * the run within the current protocol in the fade between the color pair.
 *
 * This can be done much more efficiently by computing these colors once,
 * instead of each time again for each run. However, this is not a
 * speed-critical section so this will do just nicely.
 */
void
setRunColorBuf (const System sys, int run, char *colorbuf)
{
  int range;
  int index;
  double protoffset, protrange;
  double roleoffset, roledelta;
  double color;
  double h, l, s;
  int r, g, b;

  // help function: contract roleoffset, roledelta with a factor (<= 1.0)
  void contract (double factor)
  {
    roledelta = roledelta * factor;
    roleoffset = (roleoffset * factor) + ((1.0 - factor) / 2.0);
  }

  // determine #protocol, resulting in two colors
  {
    Termlist protocols;
    Term refprot;
    int r;
    int firstfound;

    protocols = NULL;
    refprot = sys->runs[run].protocol->nameterm;
    index = 0;
    range = 1;
    firstfound = false;
    for (r = 0; r < sys->maxruns; r++)
      {
	if (sys->runs[r].protocol != INTRUDER)
	  {
	    Term prot;

	    prot = sys->runs[r].protocol->nameterm;
	    if (!isTermEqual (prot, refprot))
	      {
		// Some 'other' protocol
		if (!inTermlist (protocols, prot))
		  {
		    // New other protocol
		    protocols = termlistAdd (protocols, prot);
		    range++;
		    if (!firstfound)
		      {
			index++;
		      }
		  }
	      }
	    else
	      {
		// Our protocol
		firstfound = true;
	      }
	  }
      }
    termlistDelete (protocols);
  }

  // Compute protocol offset [0.0 ... 1.0>
  protrange = 1.0 / range;
  protoffset = index * protrange;

  // We now now our range, and we can determine which role this one is.
  {
    Role rr;
    int done;

    range = 0;
    index = 0;
    done = false;

    for (rr = sys->runs[run].protocol->roles; rr != NULL; rr = rr->next)
      {
	if (sys->runs[run].role == rr)
	  {
	    done = true;
	  }
	else
	  {
	    if (!done)
	      {
		index++;
	      }
	  }
	range++;
      }
  }

  // Compute role offset [0.0 ... 1.0]
  if (range <= 1)
    {
      roledelta = 0.0;
      roleoffset = 0.5;
    }
  else
    {
      // range over 0..1
      roledelta = 1.0 / (range - 1);
      roleoffset = index * roledelta;
      // Now this can result in a delta that is too high (depending on protocolrange)
      if (protrange * roledelta > RUNCOLORDELTA)
	{
	  contract (RUNCOLORDELTA / (protrange * roledelta));
	}
    }

  // We slightly contract the colors (taking them away from protocol edges)
  contract (RUNCOLORCONTRACT);

  // Now we can convert this to a color
  color = protoffset + (protrange * roleoffset);
  h = RUNCOLORH1 + color * (RUNCOLORH2 - RUNCOLORH1);
  l = RUNCOLORL1 + color * (RUNCOLORL2 - RUNCOLORL1);
  s = RUNCOLORS1 + color * (RUNCOLORS2 - RUNCOLORS1);

  // If the run is not trusted, we lower the saturation significantly
  if (!isRunTrusted (sys, run))
    {
      s = UNTRUSTEDCOLORS;
    }

  // set to buffer
  hlsrgb (&r, &g, &b, h, l, s);
  sprintf (colorbuf, "#%02x%02x%02x", r, g, b);

  // compute second color (light version)
  /*
     l += 0.07;
     if (l > 1.0)
     l = 1.0;
   */
  hlsrgb (&r, &g, &b, h, l, s);
  sprintf (colorbuf + 8, "#%02x%02x%02x", r, g, b);
}

//! Communication status
int
isCommunicationExact (const System sys, Binding b)
{
  Roledef rd1, rd2;

  rd1 = eventRoledef (sys, b->run_from, b->ev_from);
  rd2 = eventRoledef (sys, b->run_to, b->ev_to);

  if (!isTermEqual (rd1->message, rd2->message))
    {
      return false;
    }
  if (!isTermEqual (rd1->from, rd2->from))
    {
      return false;
    }
  if (!isTermEqual (rd1->to, rd2->to))
    {
      return false;
    }
  if (!isTermEqual (rd1->label, rd2->label))
    {
      return false;
    }
  return true;
}

//! Determine ranks for all nodes
/**
 * Some crude algorithm I sketched on the blackboard.
 */
int
graph_ranks (int *ranks, int nodes)
{
  int i;
  int todo;
  int rank;

#ifdef DEBUG
  if (hasCycle ())
    {
      error ("Graph ranks tried, but a cycle exists!");
    }
#endif

  i = 0;
  while (i < nodes)
    {
      ranks[i] = INT_MAX;
      i++;
    }

  todo = nodes;
  rank = 0;
  while (todo > 0)
    {
      // There are still unassigned nodes
      int n;

      n = 0;
      while (n < nodes)
	{
	  if (ranks[n] == INT_MAX)
	    {
	      // Does this node have incoming stuff from stuff with equal rank or higher?
	      int refn;

	      refn = 0;
	      while (refn < nodes)
		{
		  if (ranks[refn] >= rank && getNode (refn, n))
		    refn = nodes + 1;
		  else
		    refn++;
		}
	      if (refn == nodes)
		{
		  ranks[n] = rank;
		  todo--;
		}
	    }
	  n++;
	}
      rank++;
    }
  return rank;
}


//! 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;
}

//! Does a term occur in a run?
int
termOccursInRun (Term t, int run)
{
  Roledef rd;
  int e;

  rd = sys->runs[run].start;
  e = 0;
  while (e < sys->runs[run].step)
    {
      if (roledefSubTerm (rd, t))
	{
	  return true;
	}
      e++;
      rd = rd->next;
    }
  return false;
}

//! Draw a class choice
/**
 * \rho classes are already dealt with in the headers, so we should ignore them.
 */
void
drawClass (const System sys, Binding b)
{
  Term varterm;

  // now check in previous things whether we saw that term already
  int notSameTerm (Binding b2)
  {
    return (!isTermEqual (varterm, b2->term));
  }

  varterm = deVar (b->term);

  // Variable?
  if (!isTermVariable (varterm))
    {
      return;
    }

  // Agent variable?
  {
    int run;

    run = TermRunid (varterm);
    if ((run >= 0) && (run < sys->maxruns))
      {
	if (inTermlist (sys->runs[run].rho, varterm))
	  {
	    return;
	  }
      }
  }

  // Seen before?
  if (!iterate_preceding_bindings (b->run_to, b->ev_to, notSameTerm))
    {
      // We saw the same term before. Exit.
      return;
    }




  // not seen before: choose class
  eprintf ("\t");
  chooseTermNode (varterm);
  eprintf (" [label=\"");
  explainVariable (varterm);
  eprintf ("\"];\n");
  eprintf ("\t");
  chooseTermNode (varterm);
  eprintf (" -> ");
  node (sys, b->run_to, b->ev_to);
  eprintf (" [weight=\"2.0\",arrowhead=\"none\",style=\"dotted\"];\n");
}

//! Print label of a regular->regular transition node (when comm. is not exact)
/**
 * Note that we ignore any label differences, these are left implicit
 */
void
regularModifiedLabel (Binding b)
{
  Roledef rdfrom;
  Roledef rdto;

  rdfrom = eventRoledef (sys, b->run_from, b->ev_from);
  rdto = eventRoledef (sys, b->run_to, b->ev_to);

  // First up: compare messages contents'
  if (!isTermEqual (rdfrom->message, b->term))
    {
      // What is sent is not equal to what is bound
      if (termInTerm (rdfrom->message, b->term))
	{
	  // Interm: simple select
	  eprintf ("select ");
	  termPrintRemap (b->term);
	  eprintf ("\\n");
	}
      else
	{
	  // I'm not quite sure
	  eprintf ("modify\\n");
	}
    }

  // Second: agent things
  if (!isTermEqual (rdfrom->from, rdto->from))
    {
      eprintf ("fake sender ");
      termPrintRemap (rdto->from);
      eprintf ("\\n");
    }
  if (!isTermEqual (rdfrom->to, rdto->to))
    {
      eprintf ("redirect to ");
      termPrintRemap (rdto->to);
      eprintf ("\\n");
    }
}

//! Draw a single binding
void
drawBinding (const System sys, Binding b)
{
  int intr_to, intr_from;

  intr_from = (sys->runs[b->run_from].protocol == INTRUDER);
  intr_to = (sys->runs[b->run_to].protocol == INTRUDER);

  if (intr_from)
    {
      // from intruder
      /*
       * Because this can be generated many times, it seems
       * reasonable to not duplicate such arrows, especially when
       * they're from M_0. Maybe the others are still relevant.
       */
      if (1 == 1 || sys->runs[b->run_from].role == I_M)
	{
	  // now check in previous things whether we saw that term already
	  int notSameTerm (Binding b2)
	  {
	    return (!isTermEqual (b->term, b2->term));
	  }

	  if (!iterate_preceding_bindings (b->run_to, b->ev_to, notSameTerm))
	    {
	      // We saw the same term before. Exit.
	      return;
	    }
	}

      // normal from intruder (not M0)
      if (intr_to)
	{
	  // intr->intr
	  eprintf ("\t");
	  arrow (sys, b);
	  eprintf (" [label=\"");
	  termPrintRemap (b->term);
	  eprintf ("\"]");
	  eprintf (";\n");
	}
      else
	{
	  // intr->regular
	  eprintf ("\t");
	  arrow (sys, b);
	  eprintf (";\n");
	}
    }
  else
    {
      // not from intruder
      if (intr_to)
	{
	  // regular->intr
	  eprintf ("\t");
	  arrow (sys, b);
	  eprintf (";\n");
	}
      else
	{
	  // regular->regular
	  /*
	   * Has this been done *exactly* as we hoped?
	   */
	  if (isCommunicationExact (sys, b))
	    {
	      eprintf ("\t");
	      arrow (sys, b);
	      eprintf (" [style=bold,color=\"%s\"]", GOODCOMMCOLOR);
	      eprintf (";\n");
	    }
	  else
	    {
	      // Something was changed, so we call this a redirect
	      eprintf ("\t");
	      node (sys, b->run_from, b->ev_from);
	      eprintf (" -> ");
	      redirNode (sys, b);
	      eprintf (" -> ");
	      node (sys, b->run_to, b->ev_to);
	      eprintf (";\n");

	      eprintf ("\t");
	      redirNode (sys, b);
	      eprintf (" [style=filled,fillcolor=\"");
	      printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS);
	      eprintf ("\",label=\"");
	      regularModifiedLabel (b);
	      eprintf ("\"]");
	      eprintf (";\n");

	    }
	}
    }
}

//! Draw dependecies (including intruder!)
/**
 * Returns from_intruder_count (from M_0)
 */
int
drawAllBindings (const System sys)
{
  List bl;
  int fromintr;

  fromintr = 0;
  for (bl = sys->bindings; bl != NULL; bl = bl->next)
    {
      Binding b;

      b = (Binding) bl->data;
      if (!b->blocked)
	{
	  // if the binding is not done (class choice) we might
	  // still show it somewhere.
	  if (b->done)
	    {
	      // 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++;
		    }
		}
	    }
	  else
	    {
	      drawClass (sys, b);
	    }
	}
    }
  return fromintr;
}


//! Draw regular runs
void
drawRegularRuns (const System sys)
{
  int run;
  int rcnum;
  char *colorbuf;

  // two buffers, eight chars each
  colorbuf = malloc (16 * sizeof (char));

  rcnum = 0;
  for (run = 0; run < sys->maxruns; run++)
    {
      if (sys->runs[run].length > 0)
	{
	  if (sys->runs[run].protocol != INTRUDER)
	    {
	      Roledef rd;
	      int index;
	      int prevnode;

	      prevnode = 0;
	      index = 0;
	      rd = sys->runs[run].start;
	      // Regular run

	      /*
	         eprintf ("\tsubgraph cluster_run%i {\n", run);
	         eprintf ("\t\tlabel = \"");
	         eprintf ("#%i: ", run);
	         termPrintRemap (sys->runs[run].protocol->nameterm);
	         eprintf (", ");
	         agentsOfRunPrint (sys, run);
	         eprintf ("\\nTesting the second line\";\n", run);
	         if (run == 0)
	         {
	         eprintf ("\t\tcolor = red;\n");
	         }
	         else
	         {
	         eprintf ("\t\tcolor = blue;\n");
	         }
	       */

	      // set color
	      setRunColorBuf (sys, run, colorbuf);

	      // Display the respective events
	      while (index < sys->runs[run].length)
		{
		  int showthis;

		  showthis = true;
		  if (rd->type == CLAIM)
		    {
		      if (run != 0)
			{
			  showthis = false;
			}
		      else
			{
			  if (index != sys->current_claim->ev)
			    {
			      showthis = false;
			    }
			}
		    }
		  if (showthis)
		    {
		      // Print node itself
		      eprintf ("\t\t");
		      node (sys, run, index);
		      eprintf (" [");
		      if (run == 0 && index == sys->current_claim->ev)
			{
			  // The claim under scrutiny
			  eprintf
			    ("style=filled,fontcolor=\"%s\",fillcolor=\"%s\",shape=box,",
			     CLAIMTEXTCOLOR, CLAIMCOLOR);
			}
		      else
			{
			  eprintf ("shape=box,style=filled,");
			  // print color of this run
			  eprintf ("fillcolor=\"%s\",", colorbuf);
			}
		      eprintf ("label=\"");
		      //roledefPrintShort (rd);
		      roledefDraw (rd);
		      eprintf ("\"]");
		      eprintf (";\n");

		      // Print binding to previous node
		      if (index > sys->runs[run].firstReal)
			{
			  // index > 0
			  eprintf ("\t\t");
			  node (sys, run, prevnode);
			  eprintf (" -> ");
			  node (sys, run, index);
			  eprintf (" [style=\"bold\", weight=\"10.0\"]");
			  eprintf (";\n");
			  prevnode = index;
			}
		      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 (HEADER)
			      // This used to be drawn only if done && send_before_read, now we always draw it.
			      eprintf ("\t\ts%i [label=\"{ ", run);

			      // Print first line
			      {
				Term rolename;
				Term agentname;

				rolename = sys->runs[run].role->nameterm;
				agentname =
				  agentOfRunRole (sys, run, rolename);
				explainVariable (agentname);
				eprintf (" in role ");
				termPrintRemap (rolename);
				eprintf ("\\l");
			      }

			      // Second line
			      // Possible protocol (if more than one)
			      {
				int showprotocol;
				Protocol p;
				int morethanone;

				// Simple case: don't show
				showprotocol = false;

				// Check whether the protocol spec has more than one
				morethanone = false;
				for (p = sys->protocols; p != NULL;
				     p = p->next)
				  {
				    if (p != INTRUDER)
				      {
					if (p != sys->runs[run].protocol)
					  {
					    morethanone = true;
					    break;
					  }
				      }
				  }

				// More than one?
				if (morethanone)
				  {
				    if (run == 0)
				      {
					// If this is run 0 we report the protocol anyway, even is there is only a single one in the attack
					showprotocol = true;
				      }
				    else
				      {
					int r;
					// For other runs we only report when there are multiple protocols
					showprotocol = false;
					for (r = 0; r < sys->maxruns; r++)
					  {
					    if (sys->runs[r].protocol !=
						INTRUDER)
					      {
						if (sys->runs[r].protocol !=
						    sys->runs[run].protocol)
						  {
						    showprotocol = true;
						    break;
						  }
					      }
					  }
				      }
				  }

				// Use the result
				if (showprotocol)
				  {
				    eprintf ("Protocol ");
				    termPrintRemap (sys->runs[run].protocol->
						    nameterm);
				    eprintf ("\\l");
				  }
			      }
			      eprintf ("Run ");
			      printVisualRun (run);
			      eprintf ("\\l");


			      // rho, sigma, const
			      /* true if it has printed
			       */
			      int showLocal (Term told, Term tnew)
			      {
				if (realTermVariable (tnew))
				  {
				    if (termOccursInRun (tnew, run))
				      {
					// Variables are mapped, maybe. But then we wonder whether they occur in reads.
					termPrintRemap (told);
					eprintf (" : ");
					explainVariable (tnew);
				      }
				    else
				      {
					return false;
				      }
				  }
				else
				  {
				    termPrintRemap (tnew);
				  }
				return true;
			      }

			      void showLocals (Termlist tlold, Termlist tlnew,
					       Term tavoid, char *sep)
			      {
				int printsep;

				printsep = false;
				while (tlold != NULL && tlnew != NULL)
				  {
				    if (!isTermEqual (tlold->term, tavoid))
				      {
					if (printsep)
					  {
					    eprintf (sep);
					    printsep = false;
					  }
					printsep =
					  showLocal (tlold->term,
						     tlnew->term);
				      }
				    tlold = tlold->next;
				    tlnew = tlnew->next;
				  }
			      }

			      if (termlistLength (sys->runs[run].rho) > 1)
				{
				  eprintf ("|");
				  showLocals (sys->runs[run].protocol->
					      rolenames, sys->runs[run].rho,
					      sys->runs[run].role->nameterm,
					      "\\l");
				  eprintf ("\\l");
				}

			      if (sys->runs[run].constants != NULL)
				{
				  eprintf ("|Create ");
				  showLocals (sys->runs[run].role->
					      declaredconsts,
					      sys->runs[run].constants, NULL,
					      ", ");
				  eprintf ("\\l");
				}
			      if (sys->runs[run].sigma != NULL)
				{
				  eprintf ("|");
				  showLocals (sys->runs[run].role->
					      declaredvars,
					      sys->runs[run].sigma, NULL,
					      "\\l");
				  eprintf ("\\l");
				}

			      // close up
			      eprintf ("}\", shape=record");
			      eprintf (",style=filled,fillcolor=\"%s\"",
				       colorbuf + 8);
			      eprintf ("];\n");
			      eprintf ("\t\ts%i -> ", run);
			      node (sys, run, index);
			      eprintf (" [style=bold, weight=\"10.0\"];\n");
			      prevnode = index;
			    }
			}
		    }
		  index++;
		  rd = rd->next;
		}
	      //eprintf ("\t}\n");

	    }
	}
    }
  free (colorbuf);
}

//! Draw intruder runs
void
drawIntruderRuns (const System sys)
{
  int run;

  /*
     eprintf ("\tsubgraph intruder {\n");
     eprintf ("\t\tlabel = \"Intruder\\nTesting the seconds.\";\n");
     eprintf ("\t\tcolor = red;\n");
   */
  for (run = 0; run < sys->maxruns; run++)
    {
      if (sys->runs[run].length > 0)
	{
	  if (sys->runs[run].protocol == INTRUDER)
	    {
	      // Intruder run
	      if (sys->runs[run].role != I_M)
		{
		  // Not an M_0 run, so we can draw it.
		  eprintf ("\t\t");
		  node (sys, run, 0);
		  eprintf (" [style=filled,fillcolor=\"");
		  printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS);
		  eprintf ("\",");
		  if (sys->runs[run].role == I_RRSD)
		    {
		      eprintf ("label=\"decrypt\"");
		    }
		  if (sys->runs[run].role == I_RRS)
		    {
		      // Distinguish function application
		      if (isTermFunctionName
			  (sys->runs[run].start->next->message))
			{
			  eprintf ("label=\"apply\"");
			}
		      else
			{
			  eprintf ("label=\"encrypt\"");
			}
		    }
		  eprintf ("];\n");
		}
	    }
	}
    }
  //eprintf ("\t}\n\n");
}


//! Display the current semistate using dot output format.
/**
 * This is not as nice as we would like it. Furthermore, the function is too big.
 */
void
dotSemiState (const System mysys)
{
  static int attack_number = 0;
  int run;
  Protocol p;
  int *ranks;
  int maxrank;
  int from_intruder_count;
  int nodes;

  sys = mysys;

  // Open graph
  attack_number++;
  eprintf ("digraph semiState%i {\n", attack_number);
  eprintf ("\tlabel = \"[Id %i] Protocol ", sys->attackid);
  p = (Protocol) sys->current_claim->protocol;
  termPrintRemap (p->nameterm);
  eprintf (", role ");
  termPrintRemap (sys->current_claim->rolename);
  eprintf (", claim type ");
  termPrintRemap (sys->current_claim->type);
  eprintf ("\";\n");

  // Globals
  eprintf ("\tfontname=Helvetica;\n");
  eprintf ("\tnode [fontname=Helvetica];\n");
  eprintf ("\tedge [fontname=Helvetica];\n");

  // Needed for the bindings later on: create graph

  nodes = nodeCount ();
  ranks = malloc (nodes * sizeof (int));
  maxrank = graph_ranks (ranks, nodes);	// determine ranks

#ifdef DEBUG
  // For debugging purposes, we also display an ASCII version of some stuff in the comments
  printSemiState ();
  // Even draw all dependencies for non-intruder runs
  // Real nice debugging :(
  {
    int run;

    run = 0;
    while (run < sys->maxruns)
      {
	int ev;

	ev = 0;
	while (ev < sys->runs[run].length)
	  {
	    int run2;
	    int notfirstrun;

	    eprintf ("// precedence: r%ii%i <- ", run, ev);
	    run2 = 0;
	    notfirstrun = 0;
	    while (run2 < sys->maxruns)
	      {
		int notfirstev;
		int ev2;

		notfirstev = 0;
		ev2 = 0;
		while (ev2 < sys->runs[run2].length)
		  {
		    if (isDependEvent (run2, ev2, run, ev))
		      {
			if (notfirstev)
			  eprintf (",");
			else
			  {
			    if (notfirstrun)
			      eprintf (" ");
			    eprintf ("r%i:", run2);
			  }
			eprintf ("%i", ev2);
			notfirstrun = 1;
			notfirstev = 1;
		      }
		    ev2++;
		  }
		run2++;
	      }
	    eprintf ("\n");
	    ev++;
	  }
	run++;
      }
  }
#endif

  // First, runs
  drawRegularRuns (sys);
  drawIntruderRuns (sys);
  from_intruder_count = drawAllBindings (sys);

  // Third, the intruder node (if needed)
  if (from_intruder_count > 0)
    {
      eprintf
	("\tintruder [label=\"Initial intruder knowledge\", style=filled,fillcolor=\"");
      printColor (INTRUDERCOLORH, INTRUDERCOLORL, INTRUDERCOLORS);
      eprintf ("\"];\n");
    }
  // eprintf ("\t};\n");

  // For debugging we might add more stuff: full dependencies
#ifdef DEBUG
  if (DEBUGL (3))
    {
      int r1;

      for (r1 = 0; r1 < sys->maxruns; r1++)
	{
	  if (sys->runs[r1].protocol != INTRUDER)
	    {
	      int e1;

	      for (e1 = 0; e1 < sys->runs[r1].step; e1++)
		{
		  int r2;

		  for (r2 = 0; r2 < sys->maxruns; r2++)
		    {
		      if (sys->runs[r2].protocol != INTRUDER)
			{
			  int e2;

			  for (e2 = 0; e2 < sys->runs[r2].step; e2++)
			    {
			      if (isDependEvent (r1, e1, r2, e2))
				{
				  eprintf
				    ("\tr%ii%i -> r%ii%i [color=grey];\n", r1,
				     e1, r2, e2);
				}
			    }
			}
		    }
		}
	    }
	}
    }
#endif

  // Ranks
  //showRanks (sys, maxrank, ranks);

#ifdef DEBUG
  // Debug: print dependencies
  if (DEBUGL (3))
    {
      dependPrint ();
    }
#endif

  // clean memory
  free (ranks);			// ranks

  // close graph
  eprintf ("};\n\n");
}