From e21627442afe84b54de35e3c311081b043ac5558 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Mon, 2 Jan 2006 16:05:53 +0000
Subject: [PATCH] - Added 'singular' directive for roles. Syntax:   protocol
 ns3 (I,R)   {     singular role I:     {     }   }

---
 src/arachne.c  | 41 +++++++++++++++++++++++++++++++++++++++++
 src/compiler.c | 12 ++++++++++++
 src/parser.y   | 18 +++++++++++++++---
 src/role.c     |  1 +
 src/role.h     |  2 ++
 src/scanner.l  |  1 +
 src/tac.h      |  3 +++
 src/todo.txt   |  2 --
 8 files changed, 75 insertions(+), 5 deletions(-)

diff --git a/src/arachne.c b/src/arachne.c
index 04ca3e6..f925a2a 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -2483,6 +2483,9 @@ bind_goal (const Binding b)
 
 //! Prune determination because of theorems
 /**
+ * When something is pruned because of this function, the state space is still
+ * considered to be complete.
+ *
  *@returns true iff this state is invalid because of a theorem
  */
 int
@@ -2724,11 +2727,49 @@ prune_theorems ()
       bl = bl->next;
     }
 
+  /* check for singular roles */
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      if (sys->runs[run].role->singular)
+	{
+	  // This is a singular role: it therefore should not occur later on again.
+	  int run2;
+	  Term rolename;
+
+	  rolename = sys->runs[run].role->nameterm;
+	  run2 = run + 1;
+	  while (run2 < sys->maxruns)
+	    {
+	      Term rolename2;
+
+	      rolename2 = sys->runs[run2].role->nameterm;
+	      if (isTermEqual (rolename, rolename2))
+		{
+		  // This is not allowed: the singular role occurs twice in the semitrace.
+		  // Thus we prune.
+		  if (switches.output == PROOF)
+		    {
+		      indentPrint ();
+		      eprintf ("Pruned because the singular role ");
+		      termPrint (rolename);
+		      eprintf (" occurs more than once in the semitrace.\n");
+		    }
+		  return 1;
+		}
+	      run2++;
+	    }
+	}
+      run++;
+    }
+
   return 0;
 }
 
 //! Prune determination for bounds
 /**
+ * When something is pruned here, the state space is not complete anymore.
+ *
  *@returns true iff this state is invalid for some reason
  */
 int
diff --git a/src/compiler.c b/src/compiler.c
index 0413ac3..950f2ce 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -762,6 +762,12 @@ claimAddAll (const System sys, const Protocol protocol, const Role role)
   claimCreate (sys, protocol, role, CLAIM_Nisynch, NULL, NULL);
 }
 
+//! Compile a role
+/**
+ * Input: a name and a roledef tac
+ *
+ * Upon return, thisRole should contain the role definition
+ */
 void
 roleCompile (Term nameterm, Tac tc)
 {
@@ -1023,7 +1029,13 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
 	  t = levelFind (tc->t1.sym, level);
 	  if (t != NULL)
 	    {
+	      // Compile a role
 	      roleCompile (t, tc->t2.tac);
+	      // singular?
+	      if (tc->t3.value != 0)
+		{
+		  thisRole->singular = true;
+		}
 	    }
 	  else
 	    {
diff --git a/src/parser.y b/src/parser.y
index 88f72da..db82a17 100644
--- a/src/parser.y
+++ b/src/parser.y
@@ -14,6 +14,7 @@ int yylex(void);
 	char*  		str;
 	struct tacnode*	tac;
 	Symbol		symb;
+	int		value;
 }
 
 %token 	<symb>	ID
@@ -30,6 +31,7 @@ int yylex(void);
 %token 		INVERSEKEYS
 %token 		UNTRUSTED
 %token 		USERTYPE
+%token		SINGULAR
 
 %type	<tac>	spdlcomplete
 %type	<tac>	spdlrep
@@ -47,6 +49,8 @@ int yylex(void);
 %type	<tac>	key
 %type	<tac>	roleref
 
+%type   <value>	singular
+
 %type	<symb>	label
 %type	<symb>	optlabel
 
@@ -106,15 +110,23 @@ roles		: /* empty */
 		  {	$$ = tacCat($1,$2); }
 		;
 
-role		: ROLE ID '{' roledef '}' optclosing
+role		: singular ROLE ID '{' roledef '}' optclosing
       		  { 
+		  	// TODO process singular (0/1)
 		  	Tac t = tacCreate(TAC_ROLE);
-			t->t1.sym = $2;
-			t->t2.tac = $4;
+			t->t1.sym = $3;
+			t->t2.tac = $5;
+			t->t3.value = $1;
 			$$ = t;
 		  }
 		;
 
+singular	: /* empty */
+	 	  {	$$ = 0; }
+		| SINGULAR
+		  {	$$ = 1; }
+		;
+
 optclosing	: /* empty */
 		  { }
 		| ';'
diff --git a/src/role.c b/src/role.c
index 3a16b87..9caed03 100644
--- a/src/role.c
+++ b/src/role.c
@@ -243,6 +243,7 @@ roleCreate (Term name)
   r->declaredvars = NULL;
   r->declaredconsts = NULL;
   r->initiator = 1;		//! Will be determined later, if a read is the first action (in compiler.c)
+  r->singular = false;		// by default, a role is not singular
   r->next = NULL;
   return r;
 }
diff --git a/src/role.h b/src/role.h
index af09507..11675ed 100644
--- a/src/role.h
+++ b/src/role.h
@@ -132,6 +132,8 @@ struct role
   Termlist declaredvars;
   //! Flag for initiator roles
   int initiator;
+  //! Flag for singular roles
+  int singular;
   //! Pointer to next role definition.
   struct role *next;
 };
diff --git a/src/scanner.l b/src/scanner.l
index fcb2788..3d51e4d 100644
--- a/src/scanner.l
+++ b/src/scanner.l
@@ -94,6 +94,7 @@ inversekeys	{ return INVERSEKEYS; }
 untrusted	{ return UNTRUSTED; }
 compromised	{ return COMPROMISED; }
 usertype	{ return USERTYPE; }
+singular	{ return SINGULAR; }
 {id}		{	
 			yylval.symb = mkstring(yytext);
 			return ID;
diff --git a/src/tac.h b/src/tac.h
index 7a7ca07..99e42fe 100644
--- a/src/tac.h
+++ b/src/tac.h
@@ -43,18 +43,21 @@ struct tacnode
     Symbol sym;
     struct tacnode *tac;
     char *str;
+    int value;
   } t1;
   union
   {
     Symbol sym;
     struct tacnode *tac;
     char *str;
+    int value;
   } t2;
   union
   {
     Symbol sym;
     struct tacnode *tac;
     char *str;
+    int value;
   } t3;
 };
 
diff --git a/src/todo.txt b/src/todo.txt
index f5dde8c..a4c7421 100644
--- a/src/todo.txt
+++ b/src/todo.txt
@@ -1,5 +1,3 @@
-- Add 'singular' keyword for roles, and think about support for
-  strand-space like templates.
 - Simple timestamps could be added by prefixing send message before the
   role, sending any timestamp constants out first to the intruder. These
   should of course be hidden in the output somehow.