From 1bbd2f1ab78ca7b3e41101ad9576afb4e84b6f5c Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Tue, 2 Oct 2012 13:43:30 +0200
Subject: [PATCH] Introduced markers in proof output for consistency with book
 description.

---
 src/arachne.c     | 61 ++++++++++++++++++++++++++++++++++++++++++++---
 src/specialterm.c |  8 +++++++
 src/specialterm.h |  5 ++++
 src/system.c      |  3 +++
 src/system.h      |  1 +
 5 files changed, 75 insertions(+), 3 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index 4fd0905..35d0bcc 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -1084,6 +1084,53 @@ bind_new_run (const Binding b, const Protocol p, const Role r,
   return true;
 }
 
+//! Proof markers
+void
+proof_go_down(const Term label, const Term t)
+{
+  Termlist l;
+  int depth;
+  int len;
+
+  if (switches.output != PROOF)
+      return;
+  // Prepend the terms (the list is in reverse)
+  TERMLISTPREPEND(sys->proofstate,label);
+  TERMLISTPREPEND(sys->proofstate,t);
+  len = termlistLength(sys->proofstate) / 2;
+  // Display state
+  eprintf("Proof state: branch at level %i\n", len);
+  l = termlistForward(sys->proofstate);
+  depth = 0;
+  while (l != NULL)
+    {
+      int i;
+      eprintf("Proof state: ");
+
+      for (i = 0; i < depth; i++)
+	{
+	  eprintf("  ");
+	}
+      termPrint(l->prev->term);
+      eprintf("(");
+      termPrint(l->term);
+      eprintf("); ");
+      l = l->prev->prev;
+      eprintf("\n");
+      depth++;
+    }
+}
+
+void
+proof_go_up(void)
+{
+  if (switches.output != PROOF)
+      return;
+  sys->proofstate = termlistDelTerm(sys->proofstate);
+  sys->proofstate = termlistDelTerm(sys->proofstate);
+  return;
+}
+
 //! Print the current semistate
 void
 printSemiState ()
@@ -1382,12 +1429,16 @@ bind_goal_regular_run (const Binding b)
 #ifdef DEBUG
 	debug (5, "Trying to bind to existing run.");
 #endif
+	proof_go_down(TERM_DeEx,b->term);
 	sflag = bind_existing_run (b, p, r, index);
+	proof_go_up();
 	// bind to new run
 #ifdef DEBUG
 	debug (5, "Trying to bind to new run.");
 #endif
+	proof_go_down(TERM_DeNew,b->term);
 	sflag = sflag && bind_new_run (b, p, r, index);
+	proof_go_up();
 
 	indentDepth--;
 	return sflag;
@@ -1583,17 +1634,21 @@ bind_goal_all_options (const Binding b)
 	  if (know_only)
 	    {
 	      // Special case: only from intruder
+	      proof_go_down(TERM_CoOld,b->term);
 	      flag = flag && bind_goal_old_intruder_run (b);
 	      //flag = flag && bind_goal_new_intruder_run (b);
+	      proof_go_up();
 	    }
 	  else
 	    {
 	      // Normal case
-	      {
-		flag = bind_goal_regular_run (b);
-	      }
+              flag = bind_goal_regular_run (b);
+	      proof_go_down(TERM_CoOld,b->term);
 	      flag = flag && bind_goal_old_intruder_run (b);
+	      proof_go_up();
+	      proof_go_down(TERM_CoNew,b->term);
 	      flag = flag && bind_goal_new_intruder_run (b);
+	      proof_go_up();
 	    }
 	  proofDepth--;
 
diff --git a/src/specialterm.c b/src/specialterm.c
index f0ccac1..6459bd7 100644
--- a/src/specialterm.c
+++ b/src/specialterm.c
@@ -39,6 +39,10 @@
 Term TERM_Agent;
 Term TERM_Function;
 Term TERM_Hidden;
+Term TERM_CoOld;
+Term TERM_CoNew;
+Term TERM_DeEx;
+Term TERM_DeNew;
 Term TERM_Type;
 Term TERM_Nonce;
 Term TERM_Ticket;
@@ -81,6 +85,10 @@ specialTermInit (const System sys)
   langhide (TERM_Type, "Type");
   langhide (TERM_Hidden, "Hidden");
   langhide (TERM_Claim, "Claim");
+  langhide (TERM_CoOld, "Co(Old)");
+  langhide (TERM_CoNew, "Co(New)");
+  langhide (TERM_DeEx, "DeEx");
+  langhide (TERM_DeNew, "DeNew");
 
   langcons (TERM_Agent, "Agent", TERM_Type);
   langcons (TERM_Function, "Function", TERM_Type);
diff --git a/src/specialterm.h b/src/specialterm.h
index ea3e65f..3a9f510 100644
--- a/src/specialterm.h
+++ b/src/specialterm.h
@@ -31,6 +31,11 @@
 extern Term TERM_Agent;
 extern Term TERM_Function;
 extern Term TERM_Hidden;
+extern Term TERM_CoOld;
+extern Term TERM_CoNew;
+extern Term TERM_DeEx;
+extern Term TERM_DeNew;
+
 extern Term TERM_Type;
 extern Term TERM_Nonce;
 extern Term TERM_Ticket;
diff --git a/src/system.c b/src/system.c
index 5a176e6..f7fa2ad 100644
--- a/src/system.c
+++ b/src/system.c
@@ -128,6 +128,9 @@ systemReset (const System sys)
 
   /* transfer switches */
   sys->maxtracelength = switches.maxtracelength;
+
+  /* proof state */
+  sys->proofstate = NULL;	// list of proof state terms
 }
 
 //! Initialize runtime system (according to cut traces, limited runs)
diff --git a/src/system.h b/src/system.h
index 428fedb..e1148c4 100644
--- a/src/system.h
+++ b/src/system.h
@@ -153,6 +153,7 @@ struct system
   List bindings;		//!< List of bindings
   Claimlist current_claim;	//!< The claim under current investigation
   Termlist trustedRoles;	//!< Roles that should be trusted for this claim (the default, NULL, means all)
+  Termlist proofstate;		//!< State of the proof markers
 };
 
 typedef struct system *System;