- Modified a number of things related to the attack analysis tools.

* removed <term> wrappers
  * added <const> wrappers
  * removed <role><term> construct, now <rolename>R</rolename>
    constructs.
  * added <variables> section.
  * variable substitutions are followed through in runs. Thus, only
    unbound variables occur in the semitrace.
  * added the untested claims back in, so that all events in a
    role/semitrace are now shown. Note that they can be disabled
    again by using the new '-H' switch.

src/switches.c

@@ -295,6 +295,20 @@ switcher (const int process, const System sys, int index)
 	}
     }
 
+  if (detect ('H', "human-readable", 0))
+    {
+      if (!process)
+	{
+	  helptext ("-H,--human-readable",
+		    "try to make the output human-friendly (e.g. in XML)");
+	}
+      else
+	{
+	  sys->switchHuman = true;
+	  return index;
+	}
+    }
+
   /* ==================
    *  Modelchecker only
    */

src/system.c

@@ -76,6 +76,7 @@ systemInit ()
   sys->switchClaims = 0;	// default don't report on claims
   sys->switchClaimToCheck = NULL;	// default check all claims
   sys->switchXMLoutput = 0;	// default no xml output
+  sys->switchHuman = false;		// not human friendly by default
   sys->switchGoalSelectMethod = 3;	// default goal selection method
   sys->traverse = 12;		// default traversal method
 

src/system.h

@@ -144,6 +144,7 @@ struct system
   int switchGoalSelectMethod;	//!< Goal selection method for Arachne engine
   Term switchClaimToCheck;	//!< Which claim should be checked?
   int switchXMLoutput;		//!< xml output
+  int switchHuman;		//!< human readable
 
   //! Latex output switch.
   /**

src/xmlout.c

@@ -31,6 +31,7 @@ extern Term TERM_Function;	// from termlist.c
  */
 static int xmlindent;		// indent level for xml elements in output
 static Term only_claim_label;	// if NULL, show all claims in xml event lists. Otherwise, only this one.
+static int show_substitution_path;	// is only set to true for variable printing, normally false.
 
 /*
  * Default external interface: init/done
@@ -43,6 +44,7 @@ xmlOutInit (void)
   printf ("<scyther>\n");
   xmlindent = 1;
   only_claim_label = NULL;
+  show_substitution_path = false;
 }
 
 //! Close up
@@ -96,10 +98,18 @@ xmlOutInteger (const char *tag, const int value)
 
 //! Print a term in XML form (iteration inner)
 void
-xmlTermPrintInner (const Term term)
+xmlTermPrintInner (Term term)
 {
   if (term != NULL)
     {
+      if (!show_substitution_path)
+	{
+	  /* In a normal situation, variables are immediately substituted, and
+	   * only the result is output.
+	   */
+	  term = deVar (term);
+	}
+
       if (realTermLeaf (term))
 	{
 	  // Variable?
@@ -129,7 +139,9 @@ xmlTermPrintInner (const Term term)
 	  else
 	    {
 	      // Constant
+	      printf ("<const>");
 	      termPrint (term);	// Must be a normal termPrint
+	      printf ("</const>");
 	    }
 	}
       else
@@ -170,12 +182,17 @@ xmlTermPrintInner (const Term term)
 }
 
 //! Print a term in XML form (wrapper)
+/**
+ * In the original setupt, a <term> wrapper was added. It is disabled for now.
+ * If this turns out to be the preferred situation, xmlTermPrintInner can be
+ * renamed to xmlTermPrint and all will be well.
+ */
 void
 xmlTermPrint (const Term term)
 {
-  printf ("<term>");
+  // printf ("<term>");
   xmlTermPrintInner (term);
-  printf ("</term>");
+  // printf ("</term>");
 }
 
 //! Print a termlist in XML form
@@ -240,11 +257,98 @@ roleTermPrint (const Term t)
 
       typebuffer = t->type;
       t->type = GLOBAL;
-      xmlTermPrint (t);
+      termPrint (t);
       t->type = typebuffer;
     }
 }
 
+//! Print a role term with <rolename> tag and indenting etc.
+void
+xmlRoleTermPrint (const Term t)
+{
+  xmlIndentPrint ();
+  printf ("<rolename>");
+  roleTermPrint (t);
+  printf ("</rolename>\n");
+}
+
+//! Show a single variable instantiation, depth one
+void
+xmlVariableDepthOne (const Term variable)
+{
+  /*
+   * To print a variable, we would wish to see only the first substitution.
+   * Therefore, we temporarily undo any further substitutions, and reset
+   * them at the end.
+   */
+  Term varsubst;		// substitution shortcut
+  Term nextsubst;		// temporary buffer
+
+  varsubst = variable->subst;
+  if (varsubst != NULL && realTermVariable (varsubst))
+    {
+      nextsubst = varsubst->subst;
+      varsubst->subst = NULL;
+    }
+  else
+    {
+      nextsubst = NULL;
+    }
+
+  // Print the actual term
+  xmlIndentPrint ();
+  xmlTermPrint (variable);
+  printf ("\n");
+
+  if (nextsubst != NULL)
+    {
+      varsubst->subst = nextsubst;
+    }
+
+}
+
+//! Show variable instantiations
+/**
+ * Show the instantiations of all variables. Maybe we need to restrict this,
+ * and scan only for those variables that actually occur in the semitrace.
+ */
+void
+xmlVariables (const System sys)
+{
+  int prev_mode;		// buffer for show mode
+  int run;			// for loop
+
+  prev_mode = show_substitution_path;
+  show_substitution_path = true;
+  xmlPrint ("<variables>");
+  xmlindent++;
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (sys->runs[run].protocol != INTRUDER)
+	{
+	  Termlist varlist;
+
+	  varlist = sys->runs[run].locals;
+	  while (varlist != NULL)
+	    {
+	      if (realTermVariable (varlist->term))
+		{
+		  // xmlVariableDepthOne (varlist->term);
+		  xmlIndentPrint ();
+		  xmlTermPrint (varlist->term);
+		  printf ("\n");
+		}
+	      varlist = varlist->next;
+	    }
+	}
+      run++;
+    }
+  xmlindent--;
+  xmlPrint ("</variables>");
+  show_substitution_path = prev_mode;
+}
+
 //! Show inverses
 void
 xmlInverses (const System sys)
@@ -305,28 +409,35 @@ isProtocolInvolved (const System sys, const Protocol p)
 
 //! Determine whether to show an event
 int
-isEventInteresting (const Roledef rd)
+isEventInteresting (const System sys, const Roledef rd)
 {
-  if (rd->type != CLAIM)
+  if (sys->switchHuman)
     {
-      return 1;
+      if (rd->type != CLAIM)
-    }
-  else
-    {
-      // A claim
-      if (only_claim_label == NULL)
 	{
 	  return 1;
 	}
       else
 	{
-	  if (isTermEqual (only_claim_label, rd->label))
+	  // A claim
+	  if (only_claim_label == NULL)
 	    {
 	      return 1;
 	    }
+	  else
+	    {
+	      if (isTermEqual (only_claim_label, rd->label))
+		{
+		  return 1;
+		}
+	    }
 	}
+      return 0;
+    }
+  else
+    {
+      return 1;
     }
-  return 0;
 }
 
 //! Show a single event from a run
@@ -340,7 +451,7 @@ isEventInteresting (const Roledef rd)
 void
 xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
 {
-  if (!isEventInteresting (rd))
+  if (!isEventInteresting (sys, rd))
     {
       return;
     }
@@ -457,12 +568,16 @@ xmlOutEvent (const System sys, Roledef rd, const int run, const int index)
 void
 xmlRoleEventlist (const System sys, Roledef rd, int index)
 {
+  xmlPrint ("<eventlist>");
+  xmlindent++;
   while (rd != NULL)
     {
       xmlOutEvent (sys, rd, -1, index);
       index++;
       rd = rd->next;
     }
+  xmlindent--;
+  xmlPrint ("</eventlist>");
 }
 
 //! Show all protocol roles that are in the attack.
@@ -486,7 +601,7 @@ xmlInvolvedProtocolRoles (const System sys)
 	    {
 	      xmlPrint ("<role>");
 	      xmlindent++;
-	      xmlOutTerm ("name", r->nameterm);
+	      xmlRoleTermPrint (r->nameterm);
 	      xmlRoleEventlist (sys, r->roledef, 0);
 	      xmlindent--;
 	      xmlPrint ("</role>");
@@ -530,8 +645,10 @@ xmlAgentsOfRunPrint (const System sys, const int run)
   while (roles != NULL)
     {
       xmlPrint ("<role>");
-      xmlOutTerm ("name", roles->term);
+      xmlindent++;
+      xmlRoleTermPrint (roles->term);
       xmlOutTerm ("agent", deVar (agentOfRunRole (sys, run, roles->term)));
+      xmlindent--;
       xmlPrint ("</role>");
       roles = roles->next;
     }
@@ -564,10 +681,7 @@ xmlRunInfo (const System sys, const int run)
    * more generic. */
   oldagent = r->nameterm->subst;
   r->nameterm->subst = NULL;
-  xmlIndentPrint ();
+  xmlRoleTermPrint (r->nameterm);
-  printf ("<role>");
-  roleTermPrint (r->nameterm);
-  printf ("</role>\n");
   /* reinstate substitution */
   r->nameterm->subst = oldagent;
   if (oldagent != NULL)
@@ -643,6 +757,7 @@ xmlOutSemitrace (const System sys)
 
   /* mention the broken claim */
   buffer_only_claim_label = only_claim_label;
+  only_claim_label = NULL;
   if (sys->current_claim != NULL)
     {
       xmlPrint ("<broken>");
@@ -653,12 +768,11 @@ xmlOutSemitrace (const System sys)
       xmlPrint ("</broken>");
       only_claim_label = sys->current_claim->label;
     }
-  else
+
-    {
-      only_claim_label = NULL;
-    }
   /* any global information about the system */
   xmlOutSysInfo (sys);
+  /* instantiations of the variables */
+  xmlVariables (sys);
   /* semitrace */
   xmlPrint ("<semitrace>");
   xmlindent++;