- Rewrote roleInstance to cope with Arachne needs.

- Introduced some iterators for e.g. term leaves and roledefs. These are
  not used everywhere yet.

src/arachne.c

@@ -19,8 +19,8 @@ static Protocol INTRUDER;	// Pointers, to be set by the Init
 static Role I_GOAL;		// Same here.
 
 #ifdef DEBUG
-static explanation;		// Pointer to a string that describes what we just tried to do
+static char *explanation;	// Pointer to a string that describes what we just tried to do
-static indent;			// Integer indicating iteration depth 0..
+static int indentDepth;
 #endif
 
 struct goalstruct
@@ -81,7 +81,8 @@ mgu_iterate (const Termlist tl)
 }
 
 //! Yield roledef pointer for a given index
-Roledef roledef_shift (Roledef rd, int i)
+Roledef
+roledef_shift (Roledef rd, int i)
 {
   while (i > 0 && rd != NULL)
     {
@@ -193,7 +194,7 @@ bind_existing_run (const Goal goal, const Protocol p, const Role r,
 	  if (index >= old_length)
 	    sys->runs[run].length = index + 1;
 #ifdef DEBUG
-          explanation = "Bind existing run";
+	  explanation = "Bind existing run";
 #endif
 	  flag =
 	    flag & termMguInTerm (goal.rd->message, rd->message, mgu_iterate);
@@ -213,8 +214,8 @@ bind_new_run (const Goal goal, const Protocol p, const Role r,
   Roledef rd;
 
   roleInstance (sys, p, r, NULL);
-  run = sys->maxruns-1;
+  run = sys->maxruns - 1;
-  sys->runs[run].length = index+1;
+  sys->runs[run].length = index + 1;
   goal.rd->bind_run = run;
   goal.rd->bind_index = index;
   rd = roledef_shift (sys->runs[run].start, index);
@@ -292,7 +293,7 @@ bind_goal_regular (const Goal goal)
 
       if (p == INTRUDER)
 	{
-	  return 1;	// don't abort scans
+	  return 1;		// don't abort scans
 	}
       flag = bind_existing_run (goal, p, r, index);
       if (flag)
@@ -360,7 +361,7 @@ iterate ()
 
   flag = 1;
 #ifdef DEBUG
-  indent++;
+  indentDepth++;
 #endif
   if (prune ())
     {
@@ -374,10 +375,10 @@ iterate ()
 	{
 	  int i;
 
-	  for (i = 0; i < indent; i++)
+	  for (i = 0; i < indentDepth; i++)
-	      eprintf ("   ");
+	    eprintf ("   ");
 	  eprintf ("%s\n", explanation);
-      	  explanation = NULL;
+	  explanation = NULL;
 	}
 #endif
 
@@ -402,7 +403,7 @@ iterate ()
 	}
     }
 #ifdef DEBUG
-  indent--;
+  indentDepth--;
 #endif
   return flag;
 }
@@ -419,7 +420,7 @@ arachne ()
    */
 #ifdef DEBUG
   explanation = NULL;
-  indent = -1;
+  indentDepth = -1;
 #endif
 
   /*

src/compiler.c

@@ -33,6 +33,7 @@ Term levelFind (Symbol s, int i);
 Term symbolFind (Symbol s);
 Term tacTerm (Tac tc);
 Termlist tacTermlist (Tac tc);
+void compute_role_variables (const System sys, Protocol p, Role r);
 
 #define	levelDeclareVar(s)	levelTacDeclaration(s,1)
 #define	levelDeclareConst(s)	levelTacDeclaration(s,0)
@@ -120,6 +121,7 @@ compile (Tac tc, int maxrunsset)
   /* Init globals */
   maxruns = maxrunsset;
   tac_root = tc;
+
   /* process the tac */
   tacProcess (tac_root);
 
@@ -578,6 +580,7 @@ roleCompile (Term nameterm, Tac tc)
 	}
       tc = tc->next;
     }
+  compute_role_variables (sys, thisProtocol, thisRole);
   levelDone ();
 }
 
@@ -638,7 +641,7 @@ runInstanceCreate (Tac tc)
     }
 
   /* equal numbers, so it seems to be safe */
-  roleInstance (sys, p, r, instParams);
+  roleInstance (sys, p, r, instParams);	// technically, we don't need to do this for Arachne [fix later]
 
   /* after creation analysis */
   /* AC1: untrusted agents */
@@ -685,8 +688,16 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
   pr->rolenames = NULL;
   while (tcroles != NULL)
     {
-      pr->rolenames =
+      if (sys->engine == ARACHNE_ENGINE)
-	termlistAppend (pr->rolenames, levelConst (tcroles->t1.sym));
+	{
+	  pr->rolenames =
+	    termlistAppend (pr->rolenames, levelVar (tcroles->t1.sym));
+	}
+      else
+	{
+	  pr->rolenames =
+	    termlistAppend (pr->rolenames, levelConst (tcroles->t1.sym));
+	}
       tcroles = tcroles->next;
     }
 
@@ -799,6 +810,35 @@ tacTermlist (Tac tc)
   return tl;
 }
 
+//! Compute variables for a roles (for Arachne)
+void
+compute_role_variables (const System sys, Protocol p, Role r)
+{
+  if (r->variables == NULL)
+    {
+      // Not computed before, for some reason
+      Termlist tl;
+
+      int process_event (Roledef rd)
+      {
+	tl = termlistAddVariables (tl, rd->from);
+	tl = termlistAddVariables (tl, rd->to);
+	tl = termlistAddVariables (tl, rd->message);
+	return 1;
+      }
+
+      tl = NULL;
+      roledef_iterate_events (r->roledef, process_event);
+      r->variables = tl;
+
+      eprintf ("All variables for role ");
+      termPrint (r->nameterm);
+      eprintf (" are ");
+      termlistPrint (tl);
+      eprintf ("\n");
+    }
+}
+
 //! Compute prec() sets for each claim.
 /**
  * Generates two auxiliary structures. First, a table that contains

src/role.c

@@ -193,6 +193,7 @@ roleCreate (Term name)
   r->nameterm = name;
   r->next = NULL;
   r->locals = NULL;
+  r->variables = NULL;
   r->roledef = NULL;
   return r;
 }
@@ -238,3 +239,19 @@ rolesPrint (Role r)
 	}
     }
 }
+
+//! Iterate over the events in a roledef list
+/**
+ * Function gets roledef pointer
+ */
+int
+roledef_iterate_events (Roledef rd, int (*func) ())
+{
+  while (rd != NULL)
+    {
+      if (!func (rd))
+	return 0;
+      rd = rd->next;
+    }
+  return 1;
+}

src/role.h

@@ -83,7 +83,7 @@ struct roledef
   /*
    * Bindings for Arachne engine
    */
-  int bind_run;		//!< -1 for unbound
+  int bind_run;			//!< -1 for unbound
   int bind_index;
 
   /* evt runid for synchronisation, but that is implied in the
@@ -105,6 +105,8 @@ struct role
   Roledef roledef;
   //! Local constants for this role.
   Termlist locals;
+  //! Local variables for this role.
+  Termlist variables;
   //! Pointer to next role definition.
   struct role *next;
 };
@@ -124,5 +126,6 @@ Roledef roledefAdd (Roledef rd, int type, Term label, Term from, Term to,
 Role roleCreate (Term nameterm);
 void rolePrint (Role r);
 void rolesPrint (Role r);
+int roledef_iterate_events (Roledef rd, int (*func) ());
 
 #endif

src/system.c

@@ -495,72 +495,118 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
   /* duplicate roledef in buffer rd */
   rd = roledefDuplicate (role->roledef);
 
+  /* set parameters */
+  /* generic setup */
+  runs[rid].protocol = protocol;
+  runs[rid].role = role;
+  runs[rid].step = 0;
+  runs[rid].firstReal = 0;
+
   /* scan for types in agent list */
   /* scanners */
-  scanfrom = protocol->rolenames;
+  if (sys->engine != ARACHNE_ENGINE)
-  scanto = paramlist;
-  while (scanfrom != NULL && scanto != NULL)
     {
-      fromlist = termlistAdd (fromlist, scanfrom->term);
+      // Default engine adheres to scenario
-      if (scanto->term->stype != NULL &&
+      scanfrom = protocol->rolenames;
-	  inTermlist (scanto->term->stype, TERM_Type))
+      scanto = paramlist;
+      while (scanfrom != NULL && scanto != NULL)
 	{
-	  /* There is a TYPE constant in the parameter list.
+	  fromlist = termlistAdd (fromlist, scanfrom->term);
-	   * Generate a new local variable for this run, with this type */
+	  if (scanto->term->stype != NULL &&
-	  newvar = makeTermType (VARIABLE, scanfrom->term->left.symb, rid);
+	      inTermlist (scanto->term->stype, TERM_Type))
-	  artefacts = termlistAdd (artefacts, newvar);
-	  sys->variables = termlistAdd (sys->variables, newvar);
-	  newvar->stype = termlistAdd (NULL, scanto->term);
-	  tolist = termlistAdd (tolist, newvar);
-	  /* newvar is apparently new, but it might occur
-	   * in the first event if it's a read, in which
-	   * case we forget it */
-	  if (sys->switchForceChoose
-	      || !(rd->type == READ
-		   && termOccurs (rd->message, scanfrom->term)))
 	    {
-	      /* this term is forced as a choose, or it does not occur in the (first) read event */
+	      /* There is a TYPE constant in the parameter list.
-	      /* TODO scan might be more complex, but
+	       * Generate a new local variable for this run, with this type */
-	       * this will do for now. I.e. occurring
+	      newvar =
-	       * first in a read will do */
+		makeTermType (VARIABLE, scanfrom->term->left.symb, rid);
-	      extterm = makeTermTuple (newvar, extterm);
+	      artefacts = termlistAdd (artefacts, newvar);
-	      artefacts = termlistAdd (artefacts, extterm);
+	      sys->variables = termlistAdd (sys->variables, newvar);
+	      newvar->stype = termlistAdd (NULL, scanto->term);
+	      tolist = termlistAdd (tolist, newvar);
+	      /* newvar is apparently new, but it might occur
+	       * in the first event if it's a read, in which
+	       * case we forget it */
+	      if (sys->switchForceChoose
+		  || !(rd->type == READ
+		       && termOccurs (rd->message, scanfrom->term)))
+		{
+		  /* this term is forced as a choose, or it does not occur in the (first) read event */
+		  /* TODO scan might be more complex, but
+		   * this will do for now. I.e. occurring
+		   * first in a read will do */
+		  extterm = makeTermTuple (newvar, extterm);
+		  artefacts = termlistAdd (artefacts, extterm);
+		}
 	    }
+	  else
+	    {
+	      /* not a type constant, add to list */
+	      tolist = termlistAdd (tolist, scanto->term);
+	    }
+	  scanfrom = scanfrom->next;
+	  scanto = scanto->next;
 	}
-      else
+
+      /* set agent list */
+      runs[rid].agents = termlistDuplicate (tolist);
+
+      /* prefix a read for such reads. TODO: this should also cover any external stuff */
+      if (extterm != NULL)
 	{
-	  /* not a type constant, add to list */
+	  Roledef rdnew;
-	  tolist = termlistAdd (tolist, scanto->term);
+
+	  rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL);
+	  /* this is an internal action! */
+	  rdnew->internal = 1;
+	  rdnew->next = rd;
+	  rd = rdnew;
+	  /* mark the first real action */
+	  runs[rid].firstReal++;
 	}
-      scanfrom = scanfrom->next;
-      scanto = scanto->next;
-    }
-
-  /* prefix a read for such reads. TODO: this should also cover any external stuff */
-  if (extterm != NULL)
-    {
-      Roledef rdnew;
-
-      rdnew = roledefInit (READ, NULL, NULL, NULL, extterm, NULL);
-      /* this is an internal action! */
-      rdnew->internal = 1;
-      rdnew->next = rd;
-      rd = rdnew;
-      /* mark the first real action */
-      runs[rid].firstReal = 1;
     }
   else
     {
-      runs[rid].firstReal = 0;
+      // For the Arachne engine, we need to copy all these roles to new variables
+      /**
+       * Because of pre-instantiation unification, some variables might already have been filled in.
+       * Ignore agent list; instead rely on role->variables.
+       */
+      Termlist scanfrom;
+
+      runs[rid].agents = NULL;
+
+      scanfrom = role->variables;
+      while (scanfrom != NULL)
+	{
+	  Term newt, oldt;
+
+	  oldt = scanfrom->term;
+	  newt = deVar (oldt);
+	  if (realTermVariable (newt))
+	    {
+	      // Make new var for this run
+	      newt = makeTermType (VARIABLE, newt->left.symb, rid);
+	      artefacts = termlistAdd (artefacts, newt);
+	    }
+	  // Add to agent list, possibly
+	  if (inTermlist (protocol->rolenames, oldt))
+	    runs[rid].agents = termlistAdd (runs[rid].agents, newt);
+	  fromlist = termlistAdd (fromlist, oldt);
+	  tolist = termlistAdd (tolist, newt);
+
+	  eprintf ("Created for run %i: ", rid);
+	  termPrint (oldt);
+	  eprintf (" -> ");
+	  termPrint (newt);
+	  eprintf ("\n");
+
+	  scanfrom = scanfrom->next;
+	}
     }
 
-  /* set parameters */
+  /* possibly shifted rd */
-  runs[rid].protocol = protocol;
-  runs[rid].role = role;
-  runs[rid].agents = termlistDuplicate (tolist);
   runs[rid].start = rd;
   runs[rid].index = rd;
-  runs[rid].step = 0;
 
   /* duplicate all locals form this run */
   scanto = role->locals;
@@ -601,10 +647,9 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
   rd = runs[rid].start;
   while (rd != NULL)
     {
-      rd->from = termLocal (rd->from, fromlist, tolist, role->locals, rid);
+      rd->from = termLocal (rd->from, fromlist, tolist, rid);
-      rd->to = termLocal (rd->to, fromlist, tolist, role->locals, rid);
+      rd->to = termLocal (rd->to, fromlist, tolist, rid);
-      rd->message =
+      rd->message = termLocal (rd->message, fromlist, tolist, rid);
-	termLocal (rd->message, fromlist, tolist, role->locals, rid);
       rd = rd->next;
     }
   termlistDelete (fromlist);
@@ -632,30 +677,39 @@ roleInstanceDestroy (const System sys)
   if (runid >= 0)
     {
       struct run myrun;
-      Termlist artefacts;
 
       myrun = sys->runs[runid];
 
       // Destroy roledef
       roledefDestroy (myrun.start);
+
       // Destroy artefacts
-      termlistDelete (myrun.artefacts);
-      termlistDelete (myrun.locals);
-      termlistDelete (myrun.agents);
       /*
        * Arachne does real-time reduction of memory, POR does not
        * Artefact removal can only be done if knowledge sets are empty, as with Arachne
        */
       if (sys->engine == ARACHNE_ENGINE)
 	{
+	  Termlist artefacts;
 	  // Remove artefacts
 	  artefacts = myrun.artefacts;
+	  while (artefacts != NULL)
+	    {
+	      eprintf ("Artefact term to delete: ");
+	      termPrint (artefacts->term);
+	      eprintf ("\n");
+	      artefacts = artefacts->next;
+	    }
+	  artefacts = myrun.artefacts;
 	  while (artefacts != NULL)
 	    {
 	      memFree (artefacts->term, sizeof (struct term));
 	      artefacts = artefacts->next;
 	    }
 	}
+      termlistDelete (myrun.artefacts);
+      termlistDelete (myrun.locals);
+      termlistDelete (myrun.agents);
       // Destroy run struct allocation in array using realloc
       sys->runs = (Run) memRealloc (sys->runs, sizeof (struct run) * (runid));
       // Reduce run count
@@ -1011,3 +1065,30 @@ scenarioPrint (const System sys)
 	}
     }
 }
+
+//! Iterate over all roles (AND)
+/**
+ * Function called gets (sys,protocol,role)
+ * If it returns 0, iteration aborts.
+ */
+int
+system_iterate_roles (const System sys, int (*func) ())
+{
+  Protocol p;
+
+  p = sys->protocols;
+  while (p != NULL)
+    {
+      Role r;
+
+      r = p->roles;
+      while (r != NULL)
+	{
+	  if (!func (sys, p, r))
+	    return 0;
+	  r = r->next;
+	}
+      p = p->next;
+    }
+  return 1;
+}

src/system.h

@@ -232,5 +232,6 @@ int compute_rolecount (const System sys);
 int compute_roleeventmax (const System sys);
 
 void scenarioPrint (const System sys);
+int system_iterate_roles (const System sys, int (*func) ());
 
 #endif

src/term.c

@@ -884,3 +884,50 @@ termOrder (Term t1, Term t2)
 	return compR;
     }
 }
+
+//! Iterate over the leaves in a term
+/**
+ * Note that this function iterates over real leaves; thus closed variables can occur as
+ * well. It is up to func to decide wether or not to recurse.
+ */
+int
+term_iterate_leaves (const Term term, int (*func) ())
+{
+  if (term != NULL)
+    {
+      if (realTermLeaf (term))
+	{
+	  if (!func (term))
+	    return 0;
+	}
+      else
+	{
+	  if (realTermTuple (term))
+	    return (term_iterate_leaves (term->left.op1, func)
+		    && term_iterate_leaves (term->right.op2, func));
+	  else
+	    return (term_iterate_leaves (term->left.op, func)
+		    && term_iterate_leaves (term->right.key, func));
+	}
+    }
+  return 1;
+}
+
+//! Iterate over open leaves (i.e. respect variable closure)
+int
+term_iterate_open_leaves (const Term term, int (*func) ())
+{
+  int testleaf (const Term t)
+  {
+    if (substVar (t))
+      {
+	return term_iterate_open_leaves (t, func);
+      }
+    else
+      {
+	return func (t);
+      }
+  }
+
+  return term_iterate_leaves (term, testleaf);
+}

src/term.h

@@ -164,5 +164,7 @@ Term tupleProject (Term tt, int n);
 int termSize (Term t);
 float termDistance (Term t1, Term t2);
 int termOrder (Term t1, Term t2);
+int term_iterate_leaves (const Term t, int (*func) ());
+int term_iterate_open_leaves (const Term term, int (*func) ());
 
 #endif

src/termlist.c

@@ -592,12 +592,11 @@ inverseKey (Termlist inverses, Term key)
 //! Create a term local to a run.
 /*
  * We assume that at this point, no variables have been instantiated yet that occur in this term.
- * We also assume that fromlist, tolist and locals only hold real leaves.
+ * We also assume that fromlist, tolist only hold real leaves.
  *\sa termlistLocal()
  */
 Term
-termLocal (Term t, Termlist fromlist, Termlist tolist,
+termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid)
-	   const Termlist locals, const int runid)
 {
   if (t == NULL)
     return NULL;
@@ -615,10 +614,6 @@ termLocal (Term t, Termlist fromlist, Termlist tolist,
 	  fromlist = fromlist->next;
 	  tolist = tolist->next;
 	}
-      if (inTermlist (locals, t))
-	{
-	  // return termRunid(t,runid);
-	}
       return t;
     }
   else
@@ -626,17 +621,13 @@ termLocal (Term t, Termlist fromlist, Termlist tolist,
       Term newt = termDuplicate (t);
       if (realTermTuple (t))
 	{
-	  newt->left.op1 =
+	  newt->left.op1 = termLocal (t->left.op1, fromlist, tolist, runid);
-	    termLocal (t->left.op1, fromlist, tolist, locals, runid);
+	  newt->right.op2 = termLocal (t->right.op2, fromlist, tolist, runid);
-	  newt->right.op2 =
-	    termLocal (t->right.op2, fromlist, tolist, locals, runid);
 	}
       else
 	{
-	  newt->left.op =
+	  newt->left.op = termLocal (t->left.op, fromlist, tolist, runid);
-	    termLocal (t->left.op, fromlist, tolist, locals, runid);
+	  newt->right.key = termLocal (t->right.key, fromlist, tolist, runid);
-	  newt->right.key =
-	    termLocal (t->right.key, fromlist, tolist, locals, runid);
 	}
       return newt;
     }
@@ -649,15 +640,14 @@ termLocal (Term t, Termlist fromlist, Termlist tolist,
  */
 Termlist
 termlistLocal (Termlist tl, const Termlist fromlist, const Termlist tolist,
-	       const Termlist locals, int runid)
+	       int runid)
 {
   Termlist newtl = NULL;
 
   while (tl != NULL)
     {
       newtl =
-	termlistAdd (newtl,
+	termlistAdd (newtl, termLocal (tl->term, fromlist, tolist, runid));
-		     termLocal (tl->term, fromlist, tolist, locals, runid));
       tl = tl->next;
     }
   return newtl;

src/termlist.h

@@ -46,10 +46,9 @@ Termlist termlistMinusTerm (Termlist tl, Term t);
 int termlistLength (Termlist tl);
 Term inverseKey (Termlist inverses, Term key);
 Term termLocal (const Term t, Termlist fromlist, Termlist tolist,
-		const Termlist locals, const int runid);
+		const int runid);
 Termlist termlistLocal (Termlist tl, const Termlist fromlist,
-			const Termlist tolist, const Termlist locals,
+			const Termlist tolist, const int runid);
-			const int runid);
 int termlistContained (const Termlist tlbig, Termlist tlsmall);
 int validSubst (const int matchmode, const Term term);
 Term termFunction (Termlist fromlist, Termlist tolist, Term tx);