From d88402998ec06d368fee72b6e53940bf388d26ec Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Fri, 14 Dec 2012 16:59:53 +0100
Subject: [PATCH] NEW: Added '--one-role-per-agent' switch.

This switch disallows agents from performing multiple roles.

Conflicts:
	src/prune_theorems.c
---
 src/prune_theorems.c | 74 ++++++++++++++++++++++++++++++++++++++++++++
 src/switches.c       | 18 +++++++++++
 src/switches.h       |  1 +
 3 files changed, 93 insertions(+)

diff --git a/src/prune_theorems.c b/src/prune_theorems.c
index 8ba6c51..d676027 100644
--- a/src/prune_theorems.c
+++ b/src/prune_theorems.c
@@ -234,6 +234,65 @@ inequalityConstraints (const System sys)
   return true;
 }
 
+//! Prune if agents perform multiple roles
+/**
+ * Return true if should be pruned
+ *
+ * The termlist 'agentrole' contains subsequences of length 2, the first of which is a agent name, and the second is the role it is performing.
+ * The idea is that once the agent name is assigned, it should not occur again for a different role.
+ * E.g. [ alice, initiator, bob, responder, charlie, ... ]
+ */
+int
+multipleRolePrune (const System sys)
+{
+  Termlist agentrole;
+  int run;
+  int flag;
+
+  flag = false;
+  agentrole = NULL;
+  for (run = 0; run < sys->maxruns; run++)
+    {
+      Protocol p;
+
+      p = sys->runs[run].protocol;
+      if ((p != INTRUDER) && (!isHelperProtocol (p)))
+	{
+	  Role r;
+
+	  for (r = p->roles; r != NULL; r = r->next)
+	    {
+	      Term role, agent;
+	      Termlist tl;
+
+	      // Find mapping role->agent
+	      role = r->nameterm;
+	      agent = agentOfRunRole (sys, run, role);
+
+	      // Does this agent already occur yet in the list?
+	      for (tl = agentrole; tl != NULL; tl = (tl->next)->next)
+		{
+		  if (isTermEqual (agent, tl->term))
+		    {
+		      if (!isTermEqual (role, (tl->next)->term))
+			{
+			  // Same agent, but different role! This is not allowed.
+			  termlistDelete (agentrole);	// cleanup
+			  return true;
+			}
+		    }
+		}
+	      // Does not occur yet, so add
+	      // Note we add the elements in front, so we need to reverse the order
+	      agentrole = termlistPrepend (agentrole, role);
+	      agentrole = termlistPrepend (agentrole, agent);
+	    }
+	}
+    }
+  termlistDelete (agentrole);
+  return false;
+}
+
 //! Prune determination because of theorems
 /**
  * When something is pruned because of this function, the state space is still
@@ -259,6 +318,21 @@ prune_theorems (const System sys)
       return true;
     }
 
+  // Prune if agents are disallowed from performing multiple roles
+  if (switches.oneRolePerAgent != 0)
+    {
+      if (multipleRolePrune (sys))
+	{
+	  if (switches.output == PROOF)
+	    {
+	      indentPrint ();
+	      eprintf
+		("Pruned because an agent may not perform multiple roles.\n");
+	    }
+	  return true;
+	}
+    }
+
   // Prune if any initiator run talks to itself
   /**
    * This effectively disallows Alice from talking to Alice, for all
diff --git a/src/switches.c b/src/switches.c
index facbdc5..0403009 100644
--- a/src/switches.c
+++ b/src/switches.c
@@ -70,6 +70,7 @@ switchesInit (int argc, char **argv)
   switches.filterLabel = NULL;	// default check all claims
   switches.maxAttacks = 0;	// no maximum default
   switches.maxOfRole = 0;	// no maximum default
+  switches.oneRolePerAgent = 0;	// agents can perform multiple roles
 
   // Arachne
   switches.heuristic = 674;	// default goal selection method (used to be 162)
@@ -1232,6 +1233,23 @@ switcher (const int process, int index, int commandline)
 	}
     }
 
+  if (detect (' ', "one-role-per-agent", 0))
+    {
+      if (!process)
+	{
+	  if (switches.expert)
+	    {
+	      helptext ("    --one-role-per-agent",
+			"agents are disallowd from performing multiple roles");
+	    }
+	}
+      else
+	{
+	  switches.oneRolePerAgent = 1;
+	  return index;
+	}
+    }
+
 
   /* ==================
    *  Misc switches
diff --git a/src/switches.h b/src/switches.h
index 93a73a0..fffad75 100644
--- a/src/switches.h
+++ b/src/switches.h
@@ -46,6 +46,7 @@ struct switchdata
   char *filterLabel;		//!< Which claim should be checked?
   int maxAttacks;		//!< When not 0, maximum number of attacks
   int maxOfRole;		//!< When not 0, maximum number of instances of each unique (non intruder) role
+  int oneRolePerAgent;		//!< When 0, agents can perform multiple roles
 
   // Arachne
   int heuristic;		//!< Goal selection method for Arachne engine