From 47a96937acdde2d6ce28d0cce3ced5487eb8100f Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Thu, 13 May 2004 10:06:21 +0000
Subject: [PATCH] - Layout improvements accross the board of the MSCs.

---
 src/attacktemplate.tex |  5 +++
 src/latex.c            | 81 ++++++++++++++++++++++++++++++++++++++----
 src/runs.c             |  2 +-
 src/runs.h             |  1 +
 src/testl              |  4 +--
 5 files changed, 83 insertions(+), 10 deletions(-)

diff --git a/src/attacktemplate.tex b/src/attacktemplate.tex
index 1390fc0..d2847d7 100644
--- a/src/attacktemplate.tex
+++ b/src/attacktemplate.tex
@@ -2,6 +2,11 @@
 \usepackage{a4wide}
 \usepackage{msc}
 
+\setlength{\instwidth}{3.0cm}
+\setlength{\instdist}{4cm}
+\setlength{\actionwidth}{3.6cm}
+\setlength{\conditionoverlap}{1.9cm}
+
 \begin{document}
 
 \input{attack}
diff --git a/src/latex.c b/src/latex.c
index ffaccfa..c5b90e4 100644
--- a/src/latex.c
+++ b/src/latex.c
@@ -279,19 +279,52 @@ latexMSCEnd ()
 /*
  * 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.
  */
 
 void
 latexDeclInst (const System sys, int run)
 {
-  Term bar = NULL;
+  Term myAgent;
+  Term myRole;
+  Termlist roles;
+  int first;
 
-  bar = agentOfRun (sys, run);
-  printf ("\\declinst{run%d}{$", run);
-  termPrint (bar);
-  printf ("\\sharp%i$}{$", run);
-  agentsOfRunPrint (sys, run);
+  myAgent = agentOfRun (sys, run);
+  myRole = sys->runs[run].role->nameterm;
+  printf ("\\declinst{run%i}{", run);
+
+  /* display above assumptions */
+  roles = sys->runs[run].protocol->rolenames;
+  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);
 }
 
 /*
@@ -908,9 +941,43 @@ attackDisplayLatex (System sys)
 	latexDeclInst (sys, i);
     }
   /* Add the intruder instance */
-  printf ("\\declinst{eve}{Eve}{Intruder}\n");
+  printf ("\\declinst{eve}{}{{\\bf Eve}: Intruder}\n");
   printf ("\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)
+		    {
+		      printf ("\\action{creates $");
+		      first = 0;
+		    }
+		  else
+		    {
+		      printf (", ");
+		    }
+		  termPrint (tl->term);
+		}
+	      tl = tl->next;
+	    }
+	  if (!first)
+	    {
+	      printf ("$}{run%i}\n", i);
+	    }
+	}
+    }
+
   /* Print the initial intruder knowledge */
 
   printf ("\\action{knows $");
diff --git a/src/runs.c b/src/runs.c
index b042ca8..b3b06b6 100644
--- a/src/runs.c
+++ b/src/runs.c
@@ -511,7 +511,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
       rd = rd->next;
     }
   termlistDelete (fromlist);
-  termlistDelete (tolist);
+  runs[rid].locals = tolist;
 }
 
 Roledef
diff --git a/src/runs.h b/src/runs.h
index fc41d04..6f8bd14 100644
--- a/src/runs.h
+++ b/src/runs.h
@@ -65,6 +65,7 @@ struct run
   Roledef index;
   Roledef start;
   Knowledge know;
+  Termlist locals;
 };
 
 typedef struct run *Run;
diff --git a/src/testl b/src/testl
index 6b67fb6..03cc56e 100755
--- a/src/testl
+++ b/src/testl
@@ -20,9 +20,9 @@ then
     mv $template.dvi attack.dvi
     dvips attack.dvi -o attack.ps
 
-#    xdvi attack.dvi		# for Xdvi
+    xdvi attack.dvi		# for Xdvi
 #    kdvi attack.dvi		# for KDE environment
-    kghostview attack.ps	# postscript in KDE
+#    kghostview attack.ps	# postscript in KDE
 
 else