From 5c2eded8f9158bf13c1885d9840b907223bd6580 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Thu, 23 May 2013 16:38:44 +0200
Subject: [PATCH] Weakagree and Alive claims now also allow for a role
 parameter + BUGFIX.

Previously, weak agreement and aliveness claims would enforce a requirement for all agents in the range
of the rho of the claim run.

For some three-party protocols this was stronger than needed. We now allow an
optional role name parameter for these claims; if such a parameter is used, the claim
is only evaluated for the agents performing that role.

En passant fixed a potential bug: aliveness and weak agreement require a run for each
agent, but previously we didn't check if these were helper protocols. Clearly they
should not be.
---
 src/claim.c    | 114 +++++++++++++++++++++++++++++++------------------
 src/compiler.c |   4 +-
 2 files changed, 75 insertions(+), 43 deletions(-)

diff --git a/src/claim.c b/src/claim.c
index 99728a1..0fcf880 100644
--- a/src/claim.c
+++ b/src/claim.c
@@ -727,6 +727,29 @@ arachne_claim_nisynch (const System sys, const int claim_run,
   return arachne_claim_authentications (sys, claim_run, claim_index, 1);
 }
 
+//! Test weak agreement with a single agent
+int
+has_weakagree_agent (const System sys, const int claim_run, const Term agent)
+{
+  int run;
+
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      if (!isHelperProtocol (sys->runs[run].protocol))
+	{
+	  if (isTermEqual (agent, agentOfRun (sys, run)))
+	    {
+	      if (isTermlistSetEqual
+		  (sys->runs[run].rho, sys->runs[claim_run].rho))
+		{
+		  return true;
+		}
+	    }
+	}
+    }
+  return false;
+}
+
 //! Test weak agreement
 int
 arachne_claim_weakagree (const System sys, const int claim_run,
@@ -736,41 +759,31 @@ arachne_claim_weakagree (const System sys, const int claim_run,
    * Runs for each supposed agent, with matching *sets* for rho.
    * (so we can skip the actor)
    */
-  Termlist tl;
-
-  for (tl = sys->runs[claim_run].rho; tl != NULL; tl = tl->next)
+  if (sys->current_claim->parameter == NULL)
     {
-      Term agent;
+      // No parameter: need agents for all roles
+      Termlist tl;
 
-      agent = tl->term;
-      if (!isTermEqual (agent, agentOfRun (sys, claim_run)))
+      for (tl = sys->runs[claim_run].rho; tl != NULL; tl = tl->next)
 	{
-	  int run;
-	  int agentokay;
+	  Term agent;
 
-	  agentokay = false;
-	  for (run = 0; run < sys->maxruns; run++)
-	    {
-	      if (run != claim_run)
-		{
-		  if (isTermEqual (agent, agentOfRun (sys, run)))
-		    {
-		      if (isTermlistSetEqual
-			  (sys->runs[run].rho, sys->runs[claim_run].rho))
-			{
-			  agentokay = true;
-			  break;
-			}
-		    }
-		}
-	    }
-	  if (!agentokay)
+	  agent = tl->term;
+	  if (!has_weakagree_agent (sys, claim_run, agent))
 	    {
 	      return false;
 	    }
 	}
+      return true;
+    }
+  else
+    {
+      // Parameter for role
+      Term agent;
+
+      agent = agentOfRunRole (sys, claim_run, sys->current_claim->parameter);
+      return has_weakagree_agent (sys, claim_run, agent);
     }
-  return true;
 }
 
 //! Test commit(X) => running(X)
@@ -861,6 +874,25 @@ arachne_claim_commit (const System sys, const int claim_run,
   return false;
 }
 
+//! Test aliveness of agent
+int
+is_agent_alive (const System sys, const Term agent)
+{
+  int run;
+
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      if (!isHelperProtocol (sys->runs[run].protocol))
+	{
+	  if (isTermEqual (agent, agentOfRun (sys, run)))
+	    {
+	      return true;
+	    }
+	}
+    }
+  return false;
+}
+
 //! Test aliveness
 int
 arachne_claim_alive (const System sys, const int claim_run,
@@ -870,28 +902,28 @@ arachne_claim_alive (const System sys, const int claim_run,
    * 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)
+  if (sys->current_claim->parameter == NULL)
     {
-      int run;
-      int principalLives;
+      // No parameter: check for all roles
+      Termlist tl;
 
-      principalLives = false;
-      for (run = 0; run < sys->maxruns; run++)
+      for (tl = sys->runs[claim_run].rho; tl != NULL; tl = tl->next)
 	{
-	  if (isTermEqual (tl->term, agentOfRun (sys, run)))
+	  if (!is_agent_alive (sys, tl->term))
 	    {
-	      principalLives = true;
-	      break;
+	      return false;
 	    }
 	}
-      if (!principalLives)
-	{
-	  return false;
-	}
+      return true;
+    }
+  else
+    {
+      // Parameter: check for agent in that role
+      Term agent;
+
+      agent = agentOfRunRole (sys, claim_run, sys->current_claim->parameter);
+      return is_agent_alive (sys, agent);
     }
-  return true;
 }
 
 //! Determine good height for full session
diff --git a/src/compiler.c b/src/compiler.c
index d6c2a4c..126db58 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -754,8 +754,8 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
     }
   checkParameterRange (cl, CLAIM_Secret, 1, -1);
   checkParameterRange (cl, CLAIM_SKR, 1, -1);
-  checkParameterRange (cl, CLAIM_Alive, 0, 0);
-  checkParameterRange (cl, CLAIM_Weakagree, 0, 0);
+  checkParameterRange (cl, CLAIM_Alive, 0, 1);
+  checkParameterRange (cl, CLAIM_Weakagree, 0, 1);
   checkParameterRange (cl, CLAIM_Nisynch, 0, 0);
   checkParameterRange (cl, CLAIM_Niagree, 0, 0);
   checkParameterRange (cl, CLAIM_Reachable, 0, 0);