From bcbaff93dd6d7842bc087b6bd09b0fcafad0b0eb Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Wed, 12 May 2004 14:56:45 +0000
Subject: [PATCH] - Removed some redundant code. - Sends and reads now to
 intruder run. - Intruder learn event on intruder run branch.

---
 src/latex.c | 39 +++++++++++++++------------------------
 1 file changed, 15 insertions(+), 24 deletions(-)

diff --git a/src/latex.c b/src/latex.c
index 6fa2db9..94fc8b0 100644
--- a/src/latex.c
+++ b/src/latex.c
@@ -338,16 +338,16 @@ latexMessagePrint (struct tracebuf *tb, int from, int to)
   if (from == -1 && to != -1)
     {
       /* message from intruder into system */
-      printf ("\\found{$");
+      printf ("\\mess{$");
       termPrint (readTerm);
-      printf ("$}{}{run%d}\n", tb->run[to]);
+      printf ("$}{eve}{run%d}\n", tb->run[to]);
     }
   else if (from != -1 && to == -1)
     {
       /* message from system to intruder */
-      printf ("\\lost{$");
+      printf ("\\mess{$");
       termPrint (sendTerm);
-      printf ("$}{}{run%d}\n", tb->run[from]);
+      printf ("$}{run%d}{eve}\n", tb->run[from]);
     }
   else if (from != -1 && to != -1)
     {
@@ -372,7 +372,8 @@ latexMessagePrint (struct tracebuf *tb, int from, int to)
 }
 
 /*
- * hmm? TODO
+ * hmm? TODO apparently, some other variant used, with duplicate handling of
+ * lost and found ??? But only using lost...  weirdness.
  */
 
 void
@@ -403,9 +404,9 @@ latexMessagePrintHighlight (struct tracebuf *tb, int from, int to,
     }
   else if (from != -1 && to == -1)
     {
-      printf ("\\lost{$");
+      printf ("\\mess{$");
       latexTermPrint (sendTerm, highlight);
-      printf ("$}{}{run%d}\n", tb->run[from]);
+      printf ("$}{run%d}{eve}\n", tb->run[from]);
     }
   else if (from != -1 && to != -1)
     {
@@ -428,19 +429,6 @@ latexMessagePrintHighlight (struct tracebuf *tb, int from, int to,
     }
 }
 
-/*
- * Display the fact that an intruder learns some facts.
- */
-
-void
-latexLearnComment (struct tracebuf *tb, int index, Termlist tl)
-{
-  /* currently implemented as a comment */
-  printf ("\\msccomment[4ex]{$I_%d=I_%d\\oplus ", index + 1, index);
-  termlistPrint (tl);
-  printf ("$}{envright}\n");
-}
-
 /*
  * ?? TODO
  */
@@ -927,7 +915,7 @@ attackDisplayLatex (System sys)
 	latexDeclInst (sys, i);
     }
   /* Add the intruder instance */
-  printf("\\declinst{eve}{Intruder}{Eve}\n");
+  printf("\\declinst{eve}{Eve}{Intruder}\n");
   printf("\n\n");
 
   /* print the events in the attack */
@@ -962,11 +950,14 @@ attackDisplayLatex (System sys)
 			}
 		      tl = tl->next;
 		    }
-		  printf ("\\msccomment[4ex]{$I_%d=I_%d\\oplus ",
-			  cKnowledge + 1, cKnowledge);
+
+		  /* print what was learned */
+
+		  printf ("\\action{learns $");
 		  cKnowledge++;
 		  latexTermlistPrint (newtl, highlights);
-		  printf ("$}{envright}\n");
+		  printf ("$}{eve}\n");
+		  printf ("\\nextlevel[2]\n");
 		}
 
 	      if (tb->link[i] != -1 && i < tb->length)