scyther/src/latex.c

/*
 * LaTeX output component
 */

#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include "runs.h"
#include "memory.h"
#include "modelchecker.h"
#include "tracebuf.h"
#include "varbuf.h"
#include "output.h"
#include "latex.h"

//! Multiplication factor for distance between events in an MSC diagram.
#define EVENTSPACE 1
//! Similarity factor required for connecting arrows. Ranges from 0 to 1.
#define LINKTHRESHOLD 0.95

extern const char *progname;
extern const char *releasetag;
extern int globalLatex;
extern Term TERM_Function;

/*! Additional information for an events. */
struct traceinfo
{
  int match;
  int position;
};

/* global variables for this module */

//! Additional information for each event in the trace.
struct traceinfo *tinfo;
//! The maximum run number involved, plus 1.
int width;
//! Landscape/portrait switch. Currently not used.
int landscape = 0;

//! Phase of MSC production.
/**
 * In pass 1, the widths of the boxes are determined.
 * In pass 2 the actual MSC is constructed.
 */
int pass;

/* code */

//! Start the latex output. 
/** Prints some headers, and 
 * the command line that was used, as comments.
 *@param sys The system buffer.
 *@param argv The command line arguments as they were passed to the tool.
 *@param argc The number of arguments.
 */

void
latexInit (const System sys, int argc, char **argv)
{
  int i;

  printf ("%%\n");
  printf ("%% LaTeX output generated by %s\n", progname);
  printf ("%% Input:\n");

  /* print command line */
  printf ("%% $");
  for (i = 0; i < argc; i++)
    printf (" %s", argv[i]);
  printf ("\n");

  printf ("%%\n");

  /* comment macro (used for debugging) */
  printf ("\\newcommand{\\comment}[1]{}\n");
}

//! Close up any LaTeX output.
/**
 *@param sys The system state.
 */

void
latexDone (const System sys)
{
  /* closing of the document */
}

//! Print a term using LaTeX and highlighting.
/**
 * Basically a recode of termPrint, now specific using latex codes and with a
 * highlighting feature. There is still some obsolete code to show variable mappings in a term.
 *@param term a term to be printed.
 *@param highlight a list of terms to be highlighted.
 */

void
latexTermPrint (Term term, Termlist highlight)
{
  if (term == NULL)
    {
      printf ("Empty term");
      return;
    }
#ifdef DEBUG
  if (!DEBUGL (1))
    {
      term = deVar (term);
    }
#else
  term = deVar (term);
#endif
  if (realTermLeaf (term))
    {
      if (inTermlist (highlight, term))
	printf ("\\mathbf{");
      symbolPrint (term->symb);
      if (realTermVariable (term))
	printf ("V");
      if (term->runid >= 0)
	{
	  printf ("\\sharp%i", term->runid);
	}
      if (term->subst != NULL)
	{
	  printf ("\\rightarrow");
	  latexTermPrint (term->subst, highlight);
	}
      if (inTermlist (highlight, term))
	printf ("}");
    }
  if (realTermTuple (term))
    {
      printf ("(");
      latexTermTuplePrint (term, highlight);
      printf (")");
      return;
    }
  if (realTermEncrypt (term))
    {
      if (isTermLeaf (term->key)
	  && inTermlist (term->key->stype, TERM_Function))
	{
	  /* function application */
	  latexTermPrint (term->key, highlight);
	  printf ("(");
	  latexTermTuplePrint (term->op, highlight);
	  printf (")");
	}
      else
	{
	  /* normal encryption */
	  printf ("\\{");
	  latexTermTuplePrint (term->op, highlight);
	  printf ("\\}_{");
	  latexTermPrint (term->key, highlight);
	  printf ("}");
	}
    }
}

//! Print an inner (tuple) term using LaTeX, without brackets.
/**
 * The tuple printing only works correctly for normalized terms.
 * If not, they might are displayed as "((x,y),z)". Maybe that is even
 * desirable to distinguish them.
 */
void
latexTermTuplePrint (Term term, Termlist hl)
{
  if (term == NULL)
    {
      printf ("Empty term");
      return;
    }
  term = deVar(term);
  while (realTermTuple (term))
    {
      // To remove any brackets, change this into latexTermTuplePrint.
      latexTermPrint (term->op1, hl);
      printf (",");
      term = deVar(term->op2);
    }
  latexTermPrint(term, hl);
  return;
}

//! Print a termlist in LaTeX using highlighting.
/**
 * Extending LaTeX term printing to term list printing, again with highlight
 * list parameter.
 *@param tl A term list to print.
 *@param highlight Any terms to be highlighted.
 */

void
latexTermlistPrint (Termlist tl, Termlist highlight)
{
  if (tl == NULL)
    {
      printf ("\\emptyset");
      return;
    }
  while (tl != NULL)
    {
      latexTermPrint (tl->term, highlight);
      tl = tl->next;
      if (tl != NULL)
	printf (", ");
    }
}

//! Display the timers and states traversed using LaTeX.
/**
 * Obsolete: we will now only print timers on stderr. 
 */

void
latexTimers (const System sys)
{
}

//! Start drawing MSC environment.
/**
 * Includes printing title.
 *@param protocolnames A termlist with protocol name terms.
 */

void
latexMSCStart (Termlist protocolnames)
{
  if (landscape)
    printf ("\\begin{landscape}\n");

  printf ("\\begin{msc}{attack on $");
  termlistPrint (protocolnames);
  printf ("$}\n");
}

//! Close drawing MSC

void
latexMSCEnd ()
{
  printf ("\\end{msc}\n");

  if (landscape)
    printf ("\\end{landscape}\n");

}

/**
 * Declare the MSC stick for a single instance of a run participating in an
 * attack.
 * This involves layout of the partners roles, and the agent etc.
 *@param sys System state.
 *@param run The run to be declared.
 */

void
latexDeclInst (const System sys, int run)
{
  Term myAgent;
  Term myRole;
  Termlist roles;
  int first;

  myAgent = agentOfRun (sys, run);
  myRole = sys->runs[run].role->nameterm;
  if (pass == 1)
    {
      printf ("\\maxlength{\\maxmscinst}{");
    }
  else
    {
      printf ("\\declinst{run%i}{", run);
    }

  /* display above assumptions */
  roles = sys->runs[run].protocol->rolenames;
  if (pass == 2)
    {
      printf ("assumes $");
      first = 1;
      while (roles != NULL)
	{
	  if (!isTermEqual (myRole, roles->term))
	    {
	      if (!first)
		  printf (", ");
	      else
		  first = 0;
	      termPrint (agentOfRunRole(sys,run,roles->term));
	      printf(": ");
	      termPrint (roles->term);
	    }
	  roles = roles->next;
	}
      printf ("$}{");
    }

  /* display agent and role */
  printf ("$\\mathbf{");
  termPrint (myAgent);
  printf("}: ");
  termPrint (myRole);
  
  printf ("$}\n");

  /* cleanup */
  termDelete (myAgent);
}

//! Add vertical space in MSC diagrams.
/**
 * Make some space in the diagram by nextlevels.
 * TODO: can be incorporated in nextlevel[param] without loop.
 *@param amount the line integer.
 */

void
latexEventSpace (int amount)
{
  if (pass < 2)
    {
      /* not printing */
      return;
    }

  int i;
  //printf("%% number of newlines: %d\n",amount);
  for (i = 0; i < EVENTSPACE * amount; i++)
    printf ("\\nextlevel\n");
}

//! MSC message print.
/**
 * Print an arrow with message from event i to event j, as defined in the
 * tracebuffer. If either i or j are -1, the intruder is meant.
 */

void
latexMessagePrint (struct tracebuf *tb, int from, int to)
{

  Term sendTerm = NULL;
  Term readTerm = NULL;

  if (pass < 2)
    {
      /* no measurement of messages yet */
      return;
    }

  if (from == -1 && to == -1)
    {
      return;
    }
  if (from != -1)
    {
      sendTerm = tb->event[from]->message;
    }
  if (to != -1)
    {
      readTerm = tb->event[to]->message;
    }
  if (from == -1 && to != -1)
    {
      /* message from intruder into system */
      printf ("\\mess{$");
      termPrint (readTerm);
      printf ("$}{eve}{run%d}\n", tb->run[to]);
    }
  else if (from != -1 && to == -1)
    {
      /* message from system to intruder */
      printf ("\\mess{$");
      termPrint (sendTerm);
      printf ("$}{run%d}{eve}\n", tb->run[from]);
    }
  else if (from != -1 && to != -1)
    {
      /* message from one agent to another, possibly transformed */

      printf ("\\mess{$");

      termPrint (sendTerm);

      if (!isTermEqual (sendTerm, readTerm))
	{
	  printf ("\\rightarrow");
	  termPrint (readTerm);
	}

      printf ("$}{run%d", tb->run[from]);
      printf ("}{run%d}[%d]", tb->run[to],
	      EVENTSPACE * (tinfo[to].position - tinfo[from].position));

      printf ("\n");
    }
}

/**
 * hmm? TODO apparently, some other variant used, with duplicate handling of
 * lost and found ??? But only using lost...  weirdness.
 */

void
latexMessagePrintHighlight (struct tracebuf *tb, int from, int to,
			    Termlist highlight)
{

  Term sendTerm = NULL;
  Term readTerm = NULL;

  if (pass < 2)
    {
      /* no measurements on message width yet */
      return;
    }

  if (from == -1 && to == -1)
    {
      return;
    }
  if (from != -1)
    {
      sendTerm = tb->event[from]->message;
    }
  if (to != -1)
    {
      readTerm = tb->event[to]->message;
    }
  if (from == -1 && to != -1)
    {
      /* TODO redundant */
      printf ("\\found{$");
      latexTermPrint (readTerm, highlight);
      printf ("$}{}{run%d}\n", tb->run[to]);
    }
  else if (from != -1 && to == -1)
    {
      printf ("\\mess{$");
      latexTermPrint (sendTerm, highlight);
      printf ("$}{run%d}{eve}\n", tb->run[from]);
    }
  else if (from != -1 && to != -1)
    {

      printf ("\\mess{$");

      latexTermPrint (sendTerm, highlight);

      if (!isTermEqual (sendTerm, readTerm))
	{
	  printf ("\\rightarrow");
	  latexTermPrint (readTerm, highlight);
	}

      printf ("$}{run%d", tb->run[from]);
      printf ("}{run%d}[%d]", tb->run[to],
	      EVENTSPACE * (tinfo[to].position - tinfo[from].position));

      printf ("\n");
    }
}

//! Display claim violation.
/**
 * For now, only secrecy: TODO
 */

void
latexClaim (struct tracebuf *tb, int run, Termlist tl)
{
  if (pass == 1)
    {
      printf ("\\maxlength{\\maxmsccondition}{");
    }
  else
    {
      printf ("\\condition{");
    }
  printf ("$\\neg secret ");
  termlistPrint (tl);
  printf ("$}");
  if (pass == 1)
    {
      printf ("\n");
    }
  else
    {
      printf ("{run%d}\n", run);
    }
}

//! Determine matching send event.
/**
 * Given a read event, tries to find a corresponding send event in the trace
 * buffer. Currently unused.
 */

int
latexCorrespondingSend (struct tracebuf *tb, int rd)
{

  int labelMatch = 0;
  int toMatch = 0;
  int fromMatch = 0;
  int tofromMatch = 0;
  int messageMatch = 0;
  int nMatches = 0;
  int maxNMatches = 0;

  int readEvent = rd;
  int sendEvent = -1;
  int bestSendEvent = -1;

  for (sendEvent = readEvent; sendEvent >= 0; sendEvent--)
    {
      if (tb->event[sendEvent]->type == SEND)
	{
	  /* do all the different kind of matchings first */

	  labelMatch =
	    isTermEqual (tb->event[sendEvent]->label,
			 tb->event[readEvent]->label);
	  toMatch =
	    isTermEqual (tb->event[sendEvent]->to, tb->event[readEvent]->to);
	  fromMatch =
	    isTermEqual (tb->event[sendEvent]->from,
			 tb->event[readEvent]->from);
	  tofromMatch = toMatch || fromMatch;
	  messageMatch =
	    isTermEqual (tb->event[sendEvent]->message,
			 tb->event[readEvent]->message);

	  /* calculate the score */

	  nMatches = labelMatch + tofromMatch + messageMatch;

	  if (nMatches == 3)
	    {
	      /* bingo! success on all matches */

	      //printf("Found perfect match: %d\n", s);
	      bestSendEvent = sendEvent;
	      break;
	    }
	  if (nMatches > maxNMatches)
	    {
	      if (labelMatch && messageMatch)
		{
		  /* strongest restriction: message and label should match */

		  maxNMatches = nMatches;
		  bestSendEvent = sendEvent;

		}
	      else if (messageMatch)
		{
		  /* if label AND message don't match: */
		  /* at least message should match */

		  maxNMatches = nMatches;
		  bestSendEvent = sendEvent;
		}
	      else if (labelMatch)
		{
		  /* if message doesn't match */
		  /* the label should matches */

		  maxNMatches = nMatches;
		  bestSendEvent = sendEvent;
		}
	    }
	}
    }

  //bestSendEvent = NULL;
  if (bestSendEvent == -1)
    {

      int u;

      for (u = 0; u < rd; u++)
	{
	  if (tb->event[u]->type == SEND)
	    {
	      //knowledgePrint(sys->traceKnow[u]);
	      if (inKnowledge
		  (tb->know[u + 1], tb->event[readEvent]->message))
		{
		  bestSendEvent = u;
		  break;
		}
	    }
	}
    }

  if (bestSendEvent == -1)
    {
      printf ("%% Could not find a matching SEND\n");
    }
  return bestSendEvent;
}

//! Determine matching send event.
/**
 * Simplified variant of finding the matching send event.
 * However, if it is introduced at a non-send event, things start to break
 * done. REVIEW later.
 */

int
latexCorrespondingSend2 (struct tracebuf *tb, int readEvent)
{
  int u;

  for (u = tb->length - 1; u >= 0; u--)
    {
      if (tb->event[u]->type == SEND)
	{
	  if (!inKnowledge (tb->know[u], tb->event[readEvent]->message))
	    {
	      /*
	         printf("%% term[");
	         printf("]#%d is introduced at traceEvent[%d] ",readEvent,u);
	         printf("\n");
	       */
	      return u;
	    }
	}
    }

  return -1;

}

//! Display knowledge in LaTeX.

void
knowledgePrintLatex (Knowledge know)
{
  Termlist tl;

  if (know == NULL)
    {
      printf ("\\emptyset");
    }
  else
    {
      tl = knowledgeSet (know);
      latexTermlistPrint (tl, NULL);
      termlistDelete (tl);
    }
}

//! Display the attack in the systems attack buffer using LaTeX.

void
attackDisplayLatex (System sys)
{
  int i;
  struct tracebuf *tb;
  int *runPosition;
  int currRun;
  int position;
  int eventSize;
  Termlist tl;
  Termlist newtl;
  Termlist claimDetails;
  Termlist highlights = NULL;
  int cKnowledge;
  int bestSend;

  tb = sys->attack;
  if (tb == NULL)
    {
      printf ("Attack pointer empty: nothing to display.\n");
      exit (1);
    }
  /* set variables */
  varbufSet (sys, tb->variables);

  /* Rebuild knowledge. Strange, this ought to be good. 
   * Maybe reconstruct dependencies as well. */
  tracebufRebuildKnow (tb);

  /* Make a comment in which the trace is displayed, for debugging etc. */
  printf ("\n\\comment{ TRACE\n\n");
  printf ("Length: %i\n", tb->length);
  printf ("Reallength: %i\n", tb->reallength);
  printf ("\n");
  i = 0;
  while (i <= tb->length)
    {
      printf ("Knowledge %i:\n", i);
      knowledgePrint (tb->know[i]);
      printf (" [Inverses]: ");
      knowledgeInversesPrint (tb->know[i]);
      printf ("\n\n");
      if (i < tb->length)
	{
	  printf ("Event %i\t[", i);
	  switch (tb->status[i])
	    {
	    case S_UNK:
	      printf ("?");
	      break;
	    case S_RED:
	      printf ("redundant");
	      break;
	    case S_TOD:
	      printf ("to do");
	      break;
	    case S_OKE:
	      printf ("okay");
	      break;
	    default:
	      printf ("illegal status code");
	      break;
	    }
	  printf ("]\t");
	  termPrint (tb->event[i]->message);
	  printf ("\t#%i", tb->run[i]);
	  printf ("\n");
	  roledefPrint (tb->event[i]);
	  printf ("\n\n");
	}
      i++;
    }
  printf ("}\n\n");

  tinfo =
    (struct traceinfo *) memAlloc ((tb->length + 1) *
				   sizeof (struct traceinfo));

  /* 
   * Determine width, which is the 1+max(runid involved in the attack)
   */

  width = 1;
  for (i = 0; i < tb->length; i++)
    {
      // TODO: I would expect here a redundancy test
      if (tb->run[i] >= width)
	width = tb->run[i] + 1;
    }

  /*
   * Initialise tinfo arrays.
   */

  for (i = 0; i < tb->length; i++)
    {
      tb->link[i] = -1;
      tinfo[i].match = -1;
      tinfo[i].position = i;
    }
  tinfo[i].match = -1;
  tinfo[i].position = i;

  /*
   * Init array of positions (ordering) of the MSC lines.
   */

  runPosition = (int *) memAlloc (width * sizeof (int));
  for (i = 0; i < width; i++)
    {
      runPosition[i] = 0;
    }

  /*
   * Determine corresponding sends and thus links
   */

  for (i = tb->length - 1; i >= 0; i--)
    {
      if (tb->status[i] != S_RED)
	{
	  if (tb->event[i]->type == READ && !tb->event[i]->internal)
	    {
	      bestSend = latexCorrespondingSend2 (tb, i);
	      printf ("%% match: %d <-> %d\n", i, bestSend);
	      if (bestSend == -1)
		continue;	// TODO major ugliness

	      tb->link[i] = bestSend;
	      tb->link[bestSend] = i;
	    }
	  if (tb->event[i]->type == CLAIM)
	    {
	      claimDetails =
		claimViolationDetails (sys, tb->run[i], tb->event[i],
				       tb->know[i]);
	    }
	}
    }
  printf ("\\comment{ claimDetails :\n");
  termlistPrint (claimDetails);
  printf ("\n}\n");

  // landscape = (width > 4);         // not for the time being

  /*
   * Apparently unlinks things that do not meet the threshold.
   */

  position = 0;
  currRun = 0;
  eventSize = 0;
  for (i = 0; i < tb->length; i++)
    {
      if (tb->status[i] != S_RED)
	{
	  tinfo[i].position = position;
	  eventSize = 1;
	  currRun = tb->run[i];

	  switch (tb->event[i]->type)
	    {
	    case SEND:
	      position++;
	      tinfo[i].position++;
	      break;
	    case READ:
	      if (tb->link[i] != -1)
		{
		  if (termDistance
		      (tb->event[i]->message,
		       tb->event[tb->link[i]]->message) < LINKTHRESHOLD)
		    {
		      /* disconnect read-send */
		      tb->link[tb->link[i]] = -1;
		      tb->link[i] = -1;
		    }
		  else
		    {
		      if (runPosition[currRun] <= tinfo[tb->link[i]].position
			  && currRun != tb->run[tb->link[i]])
			{
			  printf ("\\comment{\n");
			  termPrint (tb->event[i]->message);
			  printf ("\n");
			  termPrint (tb->event[tb->link[i]]->message);
			  printf ("\n");
			  printf ("%% termDistance: %f\n",
				  termDistance (tb->event[i]->message,
						tb->event[tb->link[i]]->
						message));
			  printf ("}\n");
			  tinfo[i].position = tinfo[tb->link[i]].position;
			  eventSize = 0;
			}
		    }
		}
	      if (tb->event[i]->internal)
		{
		  eventSize = 0;
		}
	      break;
	    case CLAIM:
	      if (claimDetails != NULL && claimDetails != (Termlist) - 1)
		{
		  eventSize = 2;
		}
	      else
		{
		  eventSize = 0;
		}
	      break;
	    default:
	      break;
	    }
	  if (!(tb->event[i]->type == READ && tb->event[i]->internal))
	    runPosition[currRun] = tinfo[i].position + eventSize;
	  /* printf("%% Event %d at %d\n", i, position); */
	  position += eventSize;
	}
    }

  /* ------------------------------------------------------
   *
   * Start of MSC creation (2-phase)
   *
   *
   * ------------------------------------------------------
   */

  /* 2 pass for widths */

  for (pass = 1; pass <= 2; pass++)
    {
      printf ("%% Pass %i\n\n",pass);

      if (pass == 1)
	{
	  printf ("\\maxlength{\\maxmscaction}{knows}\n");
	  printf ("\\maxlength{\\maxmscaction}{creates}\n");
	}
      else
	{
	  /* slightly stretch measurements */
	  printf ("\\addtolength{\\maxmscall}{2\\mscspacer}\n");
	  printf ("\\addtolength{\\maxmscaction}{\\mscspacer}\n");
	  printf ("\\addtolength{\\maxmscinst}{\\mscspacer}\n");
	  printf ("\\addtolength{\\maxmsccondition}{\\mscspacer}\n");

	  /* put out computed widths */
	  
	  printf ("\\setlength{\\envinstdist}{0.7\\maxmscall}\n");
	  printf ("\\setlength{\\instdist}{\\maxmscall}\n");
	  printf ("\\setlength{\\actionwidth}{\\maxmscaction}\n");
	  printf ("\\setlength{\\instwidth}{\\maxmscinst}\n");
	  printf ("\\setlength{\\conditionoverlap}{0.5\\maxmsccondition}\n");

	  /* create MSC title, involving protocol names and such. */

	  Termlist protocolnames = NULL;
	  Term pname;
	  for (i = 0; i < width; i++)
	    {
	      if (runPosition[i] > 0)
		{
		  pname = sys->runs[i].protocol->nameterm;
		  if (!inTermlist (protocolnames, pname))
		    {
		      protocolnames = termlistAppend (protocolnames, pname);
		    }
		}
	    }
	  latexMSCStart (protocolnames);
	  termlistDelete (protocolnames);
	}

      /* declare instances */

      for (i = 0; i < width; i++)
	{
	  if (runPosition[i] > 0)
	    latexDeclInst (sys, i);
	}
      /* Add the intruder instance */
      if (pass == 2)
	  printf ("\\declinst{eve}{}{");
      else
	  printf ("\\maxlength{\\maxmscinst}{");
      printf ("{\\bf Eve}: Intruder}\n\n");

      /* Print the local constants for each instance */

      for (i = 0; i < width; i++)
	{
	  if (runPosition[i] > 0)
	    {
	      Termlist tl = sys->runs[i].locals;
	      int first = 1;
	      while (tl != NULL)
		{
		  /* detect whether it's really local to this run */
		  Term t = deVar (tl->term);
		  if (isTermLeaf (t) && t->runid == i)
		    {
		      if (first)
			{
			  if (pass == 1)
			      printf ("\\maxlength{\\maxmscaction}{$");
			  else
			      printf ("\\ActionBox{creates \\\\\n$");
			  first = 0;
			}
		      else
			{
			  printf (", ");
			}
		      termPrint (tl->term);
		    }
		  tl = tl->next;
		}
	      if (!first)
		{
		  if (pass == 1)
		      printf ("$}\n");
		  else
		      printf ("$}{run%i}\n", i);
		}
	    }
	}

      /* Print the initial intruder knowledge */

      if (pass == 2)
	{
	  printf ("\\ActionBox{");
          printf ("knows \\\\\n$");
          knowledgePrintLatex (tb->know[0]);
          printf ("$}");
	  printf ("{eve}\n");
          printf ("\\nextlevel[3]\n");
          printf ("\n");
	}

      /* print the events in the attack */

      //for (j=-1; j<=sys->step; j++)
      position = 0;
      cKnowledge = 0;
      for (i = 0; i < tb->length; i++)
	{
	  if (tb->status[i] != S_RED)
	    {
	      latexEventSpace (tinfo[i].position - position);
	      if (tinfo[i].position >= position)
		{
		  position = tinfo[i].position;
		}
	      switch (tb->event[i]->type)
		{
		case SEND:
		  newtl = knowledgeNew (tb->know[i], tb->know[i + 1]);
		  highlights = NULL;
		  /* Build a Termlist of terms that from the claimViolationDetails,
		     that appear in the knowledge */
		  if (newtl != NULL)
		    {
		      tl = claimDetails;
		      while (tl != NULL)
			{
			  if (inTermlist (newtl, tl->term))
			    {
			      highlights = termlistAdd (highlights, tl->term);
			    }
			  tl = tl->next;
			}

		    }

		  if (tb->link[i] != -1 && i < tb->length)
		    {
		      latexMessagePrintHighlight (tb, i, tb->link[i], highlights);
		    }
		  else
		    {
		      latexMessagePrintHighlight (tb, i, -1, highlights);	//lost message
		    }

		  /* maybe extra knowledge? */
		  if (newtl != NULL)
		    {
		      /* print what was learned */

		      if (pass == 1)
			{
			  printf ("\\maxlength{\\maxmscaction}{");
			}
		      else
			{
		          printf ("\\nextlevel[1]\n");
		          printf ("\\ActionBox{learns \\\\\n");
			}
		      printf ("$");
		      cKnowledge++;
		      latexTermlistPrint (newtl, highlights);
		      printf ("$}");
		      if (pass == 1)
			{
			  printf ("\n");
			}
		      else
			{
			  printf ("{eve}\n");
		      	  printf ("\\nextlevel[2]\n");
			}
		    }

		  termlistDelete (highlights);

		  break;
		case READ:
		  if (tb->event[i]->internal)
		    {
		    }
		  else if (tb->link[i] == -1)
		    {
		      latexMessagePrint (tb, -1, i);	//found message
		    }
		  break;
		case CLAIM:
		  if (claimDetails != NULL && claimDetails != (Termlist) - 1)
		    {
		      latexClaim (tb, tb->run[i], claimDetails);
		    }
		  break;
		default:
		  break;		//kannie!
		}
	    }
	}
    }

  /*
   * close up diagrams
   */


  latexEventSpace (2);
  latexMSCEnd ();

  /*
   * free used memory
   */

  memFree (runPosition, width * sizeof (int));
  memFree (tinfo, (tb->length + 1) * sizeof (struct traceinfo));
}