- Iteration seems to work nicely, thank you.

src/compiler.c

@@ -15,6 +15,7 @@
 #include "warshall.h"
 #include "hidelevel.h"
 #include "debug.h"
+#include "intruderknowledge.h"
 
 /*
    Simple sys pointer as a global. Yields cleaner code although it's against programming standards.
@@ -323,6 +324,7 @@ levelTacDeclaration (Tac tc, int isVar)
   Tac tscan;
   Termlist typetl = NULL;
   Term t;
+  int isAgent;
 
   // tscan contains the type list (as is const x,z: Term or var y: Term,Ding)
   tscan = tc->t2.tac;
@@ -353,6 +355,9 @@ levelTacDeclaration (Tac tc, int isVar)
       typetl = termlistAdd (typetl, t);
       tscan = tscan->next;
     }
+  /* check whether the type list contains the agent type */
+  isAgent = inTermlist (typetl, TERM_Agent);
+
   /* parse all constants and vars, because a single declaration can contain multiple ones */
   tscan = tc->t1.tac;
   while (tscan != NULL)
@@ -379,6 +384,10 @@ levelTacDeclaration (Tac tc, int isVar)
       else if (level == 0)
 	{
 	  sys->globalconstants = termlistAdd (sys->globalconstants, t);
+	  if (isAgent)
+	    {
+	      sys->agentnames = termlistAdd (sys->agentnames, t);
+	    }
 	}
       tscan = tscan->next;
     }
@@ -1813,21 +1822,8 @@ preprocess (const System sys)
    * compute hidelevels
    */
   hidelevelCompute (sys);
-
-  if (switches.check)
-    {
   /*
-       * display initial role knowledge
+   * Initial knowledge
    */
-
+  initialIntruderKnowledge (sys);
-      int showRK (Protocol p, Role r)
-      {
-	eprintf ("Role ");
-	termPrint (r->nameterm);
-	eprintf (" knows ");
-	termlistPrint (r->knows);
-	eprintf ("\n");
-      }
-      iterateRoles (sys, showRK);
-    }
 }

src/intruderknowledge.c

@@ -0,0 +1,140 @@
+/**
+ * Initial intruder knowledge computation.
+ */
+
+#include "intruderknowledge.h"
+
+//! Add a (copy of) a term to the intruder knowledge
+void
+addSTerm (const System sys, Term t, Termlist fromlist, Termlist tolist)
+{
+  Term t2;
+
+  t2 = termLocal (t, fromlist, tolist);
+  eprintf ("[ Adding ");
+  termPrint (t2);
+  eprintf (" to the initial intruder knowledge]\n");
+}
+
+//! Unfold the term for all possible options
+void
+addEnumTerm (const System sys, Term t, Term actor, Termlist todo,
+	     Termlist fromlist, Termlist tolist)
+{
+  if (todo == NULL)
+    {
+      addSTerm (sys, t, fromlist, tolist);
+    }
+  else
+    {
+      if (termSubTerm (t, todo->term))
+	{
+	  // Occurs, we have to iterate
+	  fromlist = termlistPrepend (fromlist, todo->term);
+
+	  void iterateThis (Term to)
+	  {
+	    tolist = termlistPrepend (tolist, to);
+
+	    addEnumTerm (sys, t, actor, todo->next, fromlist, tolist);
+
+	    tolist = termlistDelTerm (tolist);
+	  }
+
+	  if (isTermEqual (todo->term, actor))
+	    {
+	      // Untrusted agents only
+	      Termlist tl;
+
+	      for (tl = sys->untrusted; tl != NULL; tl = tl->next)
+		{
+		  iterateThis (tl->term);
+		}
+	    }
+	  else
+	    {
+	      // any agents
+	      Termlist tl;
+
+	      for (tl = sys->agentnames; tl != NULL; tl = tl->next)
+		{
+		  iterateThis (tl->term);
+		}
+	    }
+	  fromlist = termlistDelTerm (fromlist);
+	}
+      else
+	{
+	  // Simply proceed to next
+	  addEnumTerm (sys, t, actor, todo->next, fromlist, tolist);
+	}
+    }
+}
+
+//! Does t contain any of sublist?
+int
+anySubTerm (Term t, Termlist sublist)
+{
+  while (sublist != NULL)
+    {
+      if (termSubTerm (t, sublist->term))
+	{
+	  return true;
+	}
+      sublist = sublist->next;
+    }
+  return false;
+}
+
+void
+initialIntruderKnowledge (const System sys)
+{
+  eprintf ("Computing initial intruder knowledge.\n\n");
+  eprintf ("Agent names      : ");
+  termlistPrint (sys->agentnames);
+  eprintf ("\n");
+  eprintf ("Untrusted agents : ");
+  termlistPrint (sys->untrusted);
+  eprintf ("\n");
+
+  /*
+   * display initial role knowledge
+   */
+  int deriveFromRole (Protocol p, Role r)
+  {
+    void addListKnowledge (Termlist tl, Term actor)
+    {
+      void addTermKnowledge (Term t)
+      {
+	if (anySubTerm (t, p->rolenames))
+	  {
+	    // Has rolename subterms. We have to enumerate those.
+	    addEnumTerm (sys, t, actor, p->rolenames, NULL, NULL);
+	  }
+	else
+	  {
+	    // No actor subterm. Simply add.
+	    addSTerm (sys, t, NULL, NULL);
+	  }
+      }
+
+      while (tl != NULL)
+	{
+	  addTermKnowledge (tl->term);
+	  tl = tl->next;
+	}
+    }
+
+
+    eprintf ("Role ");
+    termPrint (r->nameterm);
+    eprintf (" knows ");
+    termlistPrint (r->knows);
+    eprintf ("\n");
+
+    addListKnowledge (r->knows, r->nameterm);
+    return true;
+  }
+
+  iterateRoles (sys, deriveFromRole);
+}

src/intruderknowledge.h

@@ -0,0 +1,8 @@
+#ifndef INTRUDERKNOWLEDGE
+#define INTRUDERKNOWLEDGE
+
+#include "system.h"
+
+void initialIntruderKnowledge (const System sys);
+
+#endif

src/system.c

@@ -59,6 +59,7 @@ systemInit ()
   sys->protocols = NULL;
   sys->locals = NULL;
   sys->variables = NULL;
+  sys->agentnames = NULL;
   sys->untrusted = NULL;
   sys->globalconstants = NULL;
   sys->hidden = NULL;

src/system.h

@@ -128,6 +128,7 @@ struct system
   Protocol protocols;		//!< List of protocols in the system
   Termlist locals;		//!< List of local terms
   Termlist variables;		//!< List of all variables
+  Termlist agentnames;		//!< List of all agent names (trusted and untrusted)
   Termlist untrusted;		//!< List of untrusted agent names
   Termlist globalconstants;	//!< List of global constants
   Hiddenterm hidden;		//!< List of hiddenterm constructs for Hidelevel lemma