- XML output should be workable now.

src/arachne.c

@@ -43,7 +43,6 @@ extern int nodes;
 extern int graph_uordblks;
 
 static System sys;
-static Claimlist current_claim;
 static int attack_length;
 
 Protocol INTRUDER;		// Pointers, to be set by the Init
@@ -1042,12 +1041,12 @@ latexSemiState ()
   // Open graph
   attack_number++;
   eprintf ("\\begin{msc}{Attack on ");
-  p = (Protocol) current_claim->protocol;
+  p = (Protocol) sys->current_claim->protocol;
   termPrint (p->nameterm);
   eprintf (", role ");
-  termPrint (current_claim->rolename);
+  termPrint (sys->current_claim->rolename);
   eprintf (", claim type ");
-  termPrint (current_claim->type);
+  termPrint (sys->current_claim->type);
   eprintf ("}\n%% Attack number %i\n", attack_number);
   eprintf ("\n");
 
@@ -1218,12 +1217,12 @@ dotSemiState ()
   attack_number++;
   eprintf ("digraph semiState%i {\n", attack_number);
   eprintf ("\tlabel = \"Protocol ");
-  p = (Protocol) current_claim->protocol;
+  p = (Protocol) sys->current_claim->protocol;
   termPrint (p->nameterm);
   eprintf (", role ");
-  termPrint (current_claim->rolename);
+  termPrint (sys->current_claim->rolename);
   eprintf (", claim type ");
-  termPrint (current_claim->type);
+  termPrint (sys->current_claim->type);
   eprintf ("\";\n");
 
   // Needed for the bindings later on: create graph
@@ -1334,7 +1333,7 @@ dotSemiState ()
 	      eprintf ("\t\t");
 	      node (run, index);
 	      eprintf (" [");
-	      if (run == 0 && index == current_claim->ev)
+	      if (run == 0 && index == sys->current_claim->ev)
 		{
 		  eprintf
 		    ("style=filled,fillcolor=mistyrose,color=salmon,shape=doubleoctagon,");
@@ -2648,7 +2647,7 @@ prune_bounds ()
 		   get_time_limit ());
 	}
       // Pruned because of time bound!
-      current_claim->timebound = 1;
+      sys->current_claim->timebound = 1;
       return 1;
     }
 
@@ -2751,11 +2750,11 @@ prune_bounds ()
 int
 prune_claim_specifics ()
 {
-  if (current_claim->type == CLAIM_Niagree)
+  if (sys->current_claim->type == CLAIM_Niagree)
     {
-      if (arachne_claim_niagree (sys, 0, current_claim->ev))
+      if (arachne_claim_niagree (sys, 0, sys->current_claim->ev))
 	{
-	  current_claim->count = statesIncrease (current_claim->count);
+	  sys->current_claim->count = statesIncrease (sys->current_claim->count);
 	  if (sys->output == PROOF)
 	    {
 	      indentPrint ();
@@ -2765,11 +2764,11 @@ prune_claim_specifics ()
 	  return 1;
 	}
     }
-  if (current_claim->type == CLAIM_Nisynch)
+  if (sys->current_claim->type == CLAIM_Nisynch)
     {
-      if (arachne_claim_nisynch (sys, 0, current_claim->ev))
+      if (arachne_claim_nisynch (sys, 0, sys->current_claim->ev))
 	{
-	  current_claim->count = statesIncrease (current_claim->count);
+	  sys->current_claim->count = statesIncrease (sys->current_claim->count);
 	  if (sys->output == PROOF)
 	    {
 	      indentPrint ();
@@ -2814,7 +2813,7 @@ add_claim_specifics (const Claimlist cl, const Roledef rd)
 void
 count_false ()
 {
-  current_claim->failed = statesIncrease (current_claim->failed);
+  sys->current_claim->failed = statesIncrease (sys->current_claim->failed);
 }
 
 //------------------------------------------------------------------------
@@ -2940,8 +2939,8 @@ iterate ()
 			  eprintf ("All goals are now bound.\n");
 			}
 		      sys->claims = statesIncrease (sys->claims);
-		      current_claim->count =
+		      sys->current_claim->count =
-			statesIncrease (current_claim->count);
+			statesIncrease (sys->current_claim->count);
 		      flag = property_check ();
 		    }
 		  else
@@ -2956,7 +2955,7 @@ iterate ()
 	  else
 	    {
 	      // Pruned because of bound!
-	      current_claim->complete = 0;
+	      sys->current_claim->complete = 0;
 	    }
 	}
     }
@@ -3057,7 +3056,7 @@ arachne ()
 	{
 	  int run;
 
-	  current_claim = cl;
+	  sys->current_claim = cl;
 	  attack_length = INT_MAX;
 	  cl->complete = 1;
 	  p = (Protocol) cl->protocol;

src/system.c

@@ -104,6 +104,10 @@ systemInit ()
   /* matching CLP */
   sys->constraints = NULL;	// no initial constraints
 
+  /* Arachne assist */
+  sys->bindings = NULL;
+  sys->current_claim = NULL;
+
   /* reset global counters */
   systemReset (sys);
 

src/system.h

@@ -195,6 +195,7 @@ struct system
 
   /* Arachne assistance */
   List bindings;		//!< List of bindings
+  Claimlist current_claim;	//!< The claim under current investigation
 
   //! Shortest attack storage.
   struct tracebuf *attack;

src/xmlout.c

@@ -109,6 +109,25 @@ xmlAttrTerm (const char *tag, const Term term)
     }
 }
 
+//! Print a term, known to be a role name
+/**
+ * Arachne turns all role names into variables for convenience. Here we
+ * temporarily undo it for pretty-printing.
+ */
+void
+roleTermPrint (const Term t)
+{
+  if (t != NULL)
+    {
+      int typebuffer;
+
+      typebuffer = t->type;
+      t->type = GLOBAL;
+      termPrint (t);
+      t->type = typebuffer;
+    }
+}
+
 //! Global system info
 /**
  * To be used by concrete trace as well as semitrace output
@@ -136,10 +155,34 @@ xmlOutSysInfo (const System sys)
   xmlPrint ("</system>");
 }
 
+//! Nicely format the role and agents we think we're talking to.
+void
+xmlAgentsOfRunPrint (const System sys, const int run)
+{
+  Termlist roles;
+
+  xmlPrint ("<roleagents>");
+  xmlindent++;
+
+  roles = sys->runs[run].protocol->rolenames;
+  while (roles != NULL)
+    {
+      xmlIndentPrint ();
+      printf ("<");
+      roleTermPrint (roles->term);
+      printf (">");
+      termPrint (agentOfRunRole (sys, run, roles->term));
+      printf ("</");
+      roleTermPrint (roles->term);
+      printf (">\n");
+      roles = roles->next;
+    }
+
+  xmlindent--;
+  xmlPrint ("</roleagents>");
+}
+
 //! Static information about a run
-/**
- * TODO: Does not output any sigma info yet (role->agent mappings), which is very important.
- */
 void
 xmlRunInfo (const System sys, const int run)
 {
@@ -155,13 +198,17 @@ xmlRunInfo (const System sys, const int run)
    * more generic. */
   oldagent = r->nameterm->subst;
   r->nameterm->subst = NULL;
-  xmlOutTerm ("role", r->nameterm);
+  xmlIndentPrint ();
+  printf ("<role>");
+  roleTermPrint (r->nameterm);
+  printf ("</role>\n");
   /* reinstate substitution */
   r->nameterm->subst = oldagent;
   if (oldagent != NULL)
     {
       xmlOutTerm ("agent", r->nameterm);
     }
+  xmlAgentsOfRunPrint (sys, run);
 }
 
 //! Show a single event from a run
@@ -309,22 +356,27 @@ xmlOutTrace (const System sys)
 
 //! Output for a semitrace (from arachne method)
 /**
- * Note: Uses get_trace_length(), which is defined for the arachne method only.
+ * Note: Uses get_trace_length(), which is defined for the arachne method
- *
+ * only.
- * TODO does not show violated claim yet, this must now be guessed by the
- * reader.
  */
 void
 xmlOutSemitrace (const System sys)
 {
   xmlIndentPrint ();
   printf ("<attack");
+  /* mention the broken claim in the attributes */
+  if (sys->current_claim != NULL)
+    {
+      xmlAttrTerm ("claim", sys->current_claim->type);
+      xmlAttrTerm ("label", sys->current_claim->label);
+    }
   /* add trace length attribute */
   printf (" tracelength=\"%i\"", get_semitrace_length ());
   printf (">\n");
   xmlindent++;
   /* any global information about the system */
   xmlOutSysInfo (sys);
+  /* semitrace */
   xmlPrint ("<semitrace>");
   xmlindent++;
   xmlOutRuns (sys);