- Layout improvements accross the board of the MSCs.

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}

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);
+  myAgent = agentOfRun (sys, run);
-  printf ("\\declinst{run%d}{$", run);
+  myRole = sys->runs[run].role->nameterm;
-  termPrint (bar);
+  printf ("\\declinst{run%i}{", run);
-  printf ("\\sharp%i$}{$", run);
+
-  agentsOfRunPrint (sys, 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 $");

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

src/runs.h

@@ -65,6 +65,7 @@ struct run
   Roledef index;
   Roledef start;
   Knowledge know;
+  Termlist locals;
 };
 
 typedef struct run *Run;

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