From 2fb0ecde97b7d39f651c786d00d27edb48f43ad0 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Tue, 4 Jan 2011 15:18:22 +0100
Subject: [PATCH] NEW: Added Aliveness and Weak Agreement claims.

---
 src/claim.c       | 110 +++++++++++++++++++++++++++++++++++++++++++++-
 src/specialterm.c |   7 ++-
 src/specialterm.h |   2 +
 3 files changed, 117 insertions(+), 2 deletions(-)

diff --git a/src/claim.c b/src/claim.c
index 186ce97..a4fd21d 100644
--- a/src/claim.c
+++ b/src/claim.c
@@ -727,7 +727,85 @@ arachne_claim_nisynch (const System sys, const int claim_run,
   return arachne_claim_authentications (sys, claim_run, claim_index, 1);
 }
 
-//! Are all agents trusted of the claim run (as required by the property?)
+//! Test weak agreement
+int
+arachne_claim_weakagree (const System sys, const int claim_run,
+			 const int claim_index)
+{
+  /*
+   * Runs for each role, with matching lists for rho.
+   */
+  Role role;
+
+  for (role = sys->runs[claim_run].protocol->roles; role != NULL;
+       role = role->next)
+    {
+      if (role != sys->runs[claim_run].role)
+	{
+	  int run;
+	  int roleokay;
+
+	  roleokay = false;
+	  for (run = 0; run < sys->maxruns; run++)
+	    {
+	      if (run != claim_run)
+		{
+		  if (role == sys->runs[run].role)
+		    {
+		      if (isTermlistEqual
+			  (sys->runs[run].rho, sys->runs[claim_run].rho))
+			{
+			  roleokay = true;
+			  break;
+			}
+		    }
+		}
+	    }
+	  if (!roleokay)
+	    {
+	      return false;
+	    }
+	}
+    }
+  return true;
+}
+//! Test aliveness
+int
+arachne_claim_alive (const System sys, const int claim_run,
+		     const int claim_index)
+{
+  /*
+   * Fairly simple claim: there must exist runs for each agent involved.
+   * We don't even consider the roles.
+   */
+  Termlist tl;
+
+  for (tl = sys->runs[claim_run].rho; tl != NULL; tl = tl->next)
+    {
+      int run;
+      int principalLives;
+
+      principalLives = false;
+      for (run = 0; run < sys->maxruns; run++)
+	{
+	  if (isTermEqual (tl->term, agentOfRun (sys, run)))
+	    {
+	      principalLives = true;
+	      break;
+	    }
+	}
+      if (!principalLives)
+	{
+	  return false;
+	}
+    }
+  return true;
+}
+
+//! Determine good height for full session
+/**
+ * For a role, assume in context of claim role
+ */
 int
 pruneClaimRunTrusted (const System sys)
 {
@@ -802,6 +880,36 @@ prune_claim_specifics (const System sys)
 	  return 1;
 	}
     }
+  if (sys->current_claim->type == CLAIM_Weakagree)
+    {
+      if (arachne_claim_weakagree (sys, 0, sys->current_claim->ev))
+	{
+	  sys->current_claim->count =
+	    statesIncrease (sys->current_claim->count);
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned: Weak agreement holds in this part of the proof tree.\n");
+	    }
+	  return 1;
+	}
+    }
+  if (sys->current_claim->type == CLAIM_Alive)
+    {
+      if (arachne_claim_alive (sys, 0, sys->current_claim->ev))
+	{
+	  sys->current_claim->count =
+	    statesIncrease (sys->current_claim->count);
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned: alive holds in this part of the proof tree.\n");
+	    }
+	  return 1;
+	}
+    }
   return 0;
 }
 
diff --git a/src/specialterm.c b/src/specialterm.c
index 3d28fba..bab7f92 100644
--- a/src/specialterm.c
+++ b/src/specialterm.c
@@ -44,6 +44,8 @@ Term TERM_Data;
 
 Term TERM_Claim;
 Term CLAIM_Secret;
+Term CLAIM_Alive;
+Term CLAIM_Weakagree;
 Term CLAIM_Nisynch;
 Term CLAIM_Niagree;
 Term CLAIM_Empty;
@@ -82,6 +84,8 @@ specialTermInit (const System sys)
   langcons (TERM_Data, "Data", TERM_Type);
 
   langcons (CLAIM_Secret, "Secret", TERM_Claim);
+  langcons (CLAIM_Alive, "Alive", TERM_Claim);
+  langcons (CLAIM_Weakagree, "Weakagree", TERM_Claim);
   langcons (CLAIM_Nisynch, "Nisynch", TERM_Claim);
   langcons (CLAIM_Niagree, "Niagree", TERM_Claim);
   langcons (CLAIM_Empty, "Empty", TERM_Claim);
@@ -101,7 +105,8 @@ specialTermInit (const System sys)
   /* basically all authentication claims */
   CLAIMS_dep_prec = termlistAdd (NULL, CLAIM_Niagree);
   CLAIMS_dep_prec = termlistAdd (CLAIMS_dep_prec, CLAIM_Nisynch);
-
+  CLAIMS_dep_prec = termlistAdd (CLAIMS_dep_prec, CLAIM_Alive);
+  CLAIMS_dep_prec = termlistAdd (CLAIMS_dep_prec, CLAIM_Weakagree);
 }
 
 //! After compilation (so the user gets the first choice)
diff --git a/src/specialterm.h b/src/specialterm.h
index 619c442..e3abc49 100644
--- a/src/specialterm.h
+++ b/src/specialterm.h
@@ -38,6 +38,8 @@ extern Term TERM_Data;
 
 extern Term TERM_Claim;
 extern Term CLAIM_Secret;
+extern Term CLAIM_Alive;
+extern Term CLAIM_Weakagree;
 extern Term CLAIM_Nisynch;
 extern Term CLAIM_Niagree;
 extern Term CLAIM_Empty;