/*
 * 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"

#define EVENTSPACE 1
#define LINKTHRESHOLD 0.95

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

/* struct for additional info */

struct traceinfo
{
  int match;
  int position;
};

/* global variables for this module */

struct traceinfo *tinfo;
int width;
int landscape = 0;
int *runPerm;

/* code */

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");
}

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

/*
 * latexTermPrint
 *
 * basically a recode of termPrint, now specific using latex codes and with a
 * highlighting feature.
 *
 * In:
 * - a term to be printed.
 * - 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 ("(");
      while (realTermTuple (term))
	{
	  latexTermPrint (term->op1, highlight);
	  printf (",");
	  term = term->op2;
	  if (!realTermTuple (term))
	    latexTermPrint (term, highlight);

	}
      printf (")");
      return;
    }
  if (realTermEncrypt (term))
    {
      if (isTermLeaf (term->key)
	  && inTermlist (term->key->stype, TERM_Function))
	{
	  /* function application */
	  latexTermPrint (term->key, highlight);
	  printf ("(");
	  latexTermPrint (term->op, highlight);
	  printf (")");
	}
      else
	{
	  /* normal encryption */
	  printf ("\\{");
	  latexTermPrint (term->op, highlight);
	  printf ("\\}_{");
	  latexTermPrint (term->key, highlight);
	  printf ("}");
	}
    }
}

/*
 * extending LaTeX term printing to term list printing, again with highlight
 * list parameter.
 */

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

/*
 * Display the timers and states traversed, LaTeX version.
 */

void
latexTimers (const System sys)
{
  void endline (void)
  {
    printf ("\\\\ \\hline\n");
  }

  printf ("\\begin{tabular}{|r|r|c|r|} \\hline\n");

  /* display stats, header first */

  printf ("Time & States & Attack & st/sec");
  endline ();

  /* print time */

  double seconds;
  seconds = (double) clock () / CLOCKS_PER_SEC;
  printf ("$%.3e$ &", seconds);

  /* states traversed */

  printf ("$");
  statesPrintShort (sys);
  printf ("$ &");

  /* flag
   *
   * L n          Attack of length <n>
   * None         failed claim
   * NoClaim      no claims
   */

  if (sys->claims == 0)
    {
      printf ("NoClaim & ");
    }
  else
    {
      if (sys->failed > 0)
	printf ("L:%i & ", attackLength (sys->attack));
      else
	printf ("None & ");
    }

  /*
     printf("%.3e (%li) claims encountered.\n",(double)
     sys->claims, sys->claims);
     printf("%.3e (%li) claims failed.\n",(double)
     sys->failed, sys->failed);
   */

  /* states per second */

  if (seconds > 0)
    {
      printf ("$%.3e$ ",
	      (double) (sys->statesLow +
			(sys->statesHigh * ULONG_MAX)) / seconds);
    }
  else
    {
      printf ("$\\infty$ ");
    }
  endline ();

  printf ("\\end{tabular}\n\n");
}

/*
 * Start drawing MSC environment.
 *
 * Includes printing title
 */

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.
 */

void
latexDeclInst (const System sys, int run)
{
  Term bar = NULL;

  bar = agentOfRun (sys, run);
  printf ("\\declinst{run%d}{$", run);
  termPrint (bar);
  printf ("\\sharp%i$}{$", run);
  agentsOfRunPrint (sys, run);
  printf ("$}\n");
}

/*
 * Make some space in the diagram by nextlevels.
 *
 * TODO: can be incorporated in nextlevel[param] without loop.
 */

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

/*
 * 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 (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 (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)
    {
      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");
    }
}

/*
 * ?? TODO
 */

void
latexAction (struct tracebuf *tb, int te)
{
  printf ("\\action{$");
  termPrint (tb->event[te]->message);
  printf ("$}{run%d}\n", tb->run[te]);
  //printf("\\nextlevel\n");
}

/*
 * display claim violation.
 *
 * for now, only secrecy: TODO
 */

void
latexClaim (struct tracebuf *tb, int run, Termlist tl)
{
  printf ("\\condition{$");
  printf ("\\neg secret ");
  termlistPrint (tl);
  printf ("$}{run%d}\n", run);
}

/*
 * Given a read event, tries to find a corresponding send event in the trace
 * buffer.
 */

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

/*
 * VERY broken. Mindwipe and recursion using inKnowledge, so this can't work.
 *
 * Apparently, it's supposed to find any subterm and was added in revision 526
 * by Lutger.
 */

int
newInKnowledge (const Knowledge know, Term term)
{
  /* if there is no term, then it's okay 'fur sure' */
  if (term == NULL)
    return 1;
  /* if there is a term, but no knowledge, we're in trouble */
  if (know == NULL)
    return 0;

  mindwipe (know, inKnowledge (know, term));

  term = deVar (term);
  if (isTermLeaf (term))
    {
      return inTermlist (know->basic, term);
    }
  if (term->type == ENCRYPT)
    {
      return inTermlist (know->encrypt, term) ||
	(inKnowledge (know, term->key) || inKnowledge (know, term->op));
    }
  if (term->type == TUPLE)
    {
      return (inTermlist (know->encrypt, term) ||
	      (inKnowledge (know, term->op1) ||
	       inKnowledge (know, term->op2)));
    }
  return 0;			/* unrecognized term type, weird */
}

/*
 * 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 format.
 */

void
knowledgePrintLatex (Knowledge know)
{
  Termlist tl;

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

/*
 * Display an attack
 */

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

  /* 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 */
  printf("\\declinst{eve}{Eve}{Intruder}\n");
  printf("\n\n");

  /* Print the initial intruder knowledge */

  printf ("\\action{knows $");
  knowledgePrintLatex (tb->know[0]);
  printf ("$}{eve}\n");
  printf ("\\nextlevel[2]\n\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:

	      /* TODO issue: this causes the knowledge learning to be printed
	       * before the actual read arrow is drawn, which is not what we
	       * want.  We would like to see the learning after it.
	       */
	       
	      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;
		    }

		  /* print what was learned */

		  printf ("\\action{learns $");
		  cKnowledge++;
		  latexTermlistPrint (newtl, highlights);
		  printf ("$}{eve}\n");
		  printf ("\\nextlevel[2]\n");
		}

	      if (tb->link[i] != -1 && i < tb->length)
		{
		  latexMessagePrintHighlight (tb, i, tb->link[i], highlights);
		}
	      else
		{
		  latexMessagePrintHighlight (tb, i, -1, highlights);	//lost message
		}
	      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!
	    }
	}
    }
  latexEventSpace (2);
  latexMSCEnd ();
  memFree (runPosition, width * sizeof (int));
  memFree (tinfo, (tb->length + 1) * sizeof (struct traceinfo));
}