- Added functional 'knows' keyword.

src/compiler.c

@@ -44,6 +44,7 @@ Term tacTerm (Tac tc);
 Termlist tacTermlist (Tac tc);
 Term levelDeclare (Symbol s, int isVar, int level);
 void compute_role_variables (const System sys, Protocol p, Role r);
+void roleKnows (Tac tc);
 
 /*
  * Global stuff
@@ -828,6 +829,9 @@ roleCompile (Term nameterm, Tac tc)
 	  case TAC_CLAIM:
 	    commEvent (CLAIM, tc);
 	    break;
+	  case TAC_KNOWS:
+	    roleKnows (tc);
+	    break;
 	  default:
 	    if (!normalDeclaration (tc))
 	      {
@@ -859,6 +863,13 @@ roleCompile (Term nameterm, Tac tc)
   levelDone ();
 }
 
+//! Initial role knowledge declaration
+void
+roleKnows (Tac tc)
+{
+  thisRole->knows = termlistConcat (thisRole->knows, tacTermlist (tc->t1.tac));
+}
+
 void
 runInstanceCreate (Tac tc)
 {
@@ -1801,4 +1812,17 @@ preprocess (const System sys)
    * compute hidelevels
    */
   hidelevelCompute (sys);
+  /*
+   * display initial role knowledge
+   */
+
+  int showRK (Protocol p, Role r)
+  {
+    eprintf ("Role ");
+    termPrint (r->nameterm);
+    eprintf (" knows ");
+    termlistPrint (r->knows);
+    eprintf ("\n");
+  }
+  iterateRoles (sys,showRK);
 }

src/parser.y

@@ -54,6 +54,7 @@ int yylex(void);
 %type	<tac>	basictermlist
 %type	<tac>	key
 %type	<tac>	roleref
+%type	<tac>	knowsdecl
 
 %type   <value>	singular
 
@@ -145,6 +146,8 @@ roledef		: /* empty */
 		  {	$$ = tacCat($1,$2); }
 		| declaration roledef
 		  {	$$ = tacCat($1,$2); }
+		| knowsdecl roledef
+		  {	$$ = tacCat($1,$2); }
 		;
 
 event		: READT label '(' termlist ')' ';'
@@ -178,6 +181,13 @@ roleref		: ID '.' ID
 		  }
 		;
 
+knowsdecl	: KNOWS termlist ';'
+		  {	Tac t = tacCreate(TAC_KNOWS);
+		  	t->t1.tac = $2;
+			$$ = t;
+		  }
+		;
+
 declaration	: secretpref CONST basictermlist typeinfo1 ';'
 		  {	Tac t = tacCreate(TAC_CONST);
 		  	t->t1.tac = $3;

src/role.c

@@ -229,6 +229,7 @@ roleCreate (Term name)
   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;
+  r->knows = NULL;
   return r;
 }
 

src/role.h

@@ -134,6 +134,8 @@ struct role
   Termlist declaredconsts;
   //! Declared variables for this role
   Termlist declaredvars;
+  //! Initial role knowledge
+  Termlist knows;
   //! Flag for initiator roles
   int initiator;
   //! Flag for singular roles

src/system.c

@@ -1381,6 +1381,31 @@ iterateLocalToOther (const System sys, const int myrun,
   return flag;
 }
 
+//! Iterate over all roles
+int
+iterateRoles (const System sys, int (*callback) (Protocol p, Role r))
+{
+  Protocol p;
+
+  p = sys->protocols;
+  while (p != NULL)
+    {
+      Role r;
+
+      r = p->roles;
+      while (r != NULL)
+	{
+	  if (!callback (p, r))
+	    {
+	      return false;
+	    }
+	  r = r->next;
+	}
+      p = p->next;
+    }
+  return true;
+}
+
 //! Get first read/send occurrence (event index) of term t in run r
 int
 firstOccurrence (const System sys, const int r, Term t, int evtype)

src/system.h

@@ -203,6 +203,7 @@ int iterateEventsType (const System sys, const int run, const int evtype,
 		       int (*callback) (Roledef rd, int ev));
 int iterateLocalToOther (const System sys, const int myrun,
 			 int (*callback) (Term t));
+int iterateRoles (const System sys, int (*callback) (Protocol p, Role r));
 int firstOccurrence (const System sys, const int r, Term t, int evtype);
 Roledef eventRoledef (const System sys, const int run, const int ev);
 int countInitiators (const System sys);

src/tac.h

@@ -22,6 +22,7 @@ enum tactypes
   TAC_STRING,
   TAC_ROLE,
   TAC_PROTOCOL,
+  TAC_KNOWS,
   TAC_RUN,
   TAC_ROLEREF,
   TAC_SECRET,