- Rewrite of actor/agent type consitency code: now more aware of

initiator/responder difference.

src/arachne.c

@@ -574,6 +574,71 @@ countIntruderActions ()
   return count;
 }
 
+//! Check this variables whether it is a good agent type
+/**
+ * Checks for leaf/etc and correct agent type
+ */
+int
+goodAgentType (Term agent)
+{
+  agent = deVar (agent);
+
+  if (!realTermLeaf (agent))
+    {				// not a leaf
+      return false;
+    }
+  else
+    {				// real leaf
+      if (isTermVariable (agent))
+	{
+	  // Variable: check type consistency (should have a solution)
+	  // Not yet: depends on matching mode also
+	}
+      else
+	{
+	  // Constant: allow only exact type
+	  if (!inTermlist (agent->stype, TERM_Agent))
+	    {
+	      return false;
+	    }
+	}
+    }
+
+  return true;
+}
+
+//! Check initiator roles
+/**
+ * Returns false iff an agent type is wrong
+ */
+int
+initiatorAgentsType ()
+{
+  int run;
+
+  run = 0;
+  while (run < sys->maxruns)
+    {
+      // Only for initiators
+      if (sys->runs[run].role->initiator)
+	{
+	  Termlist agents;
+
+	  agents = sys->runs[run].agents;
+	  while (agents != NULL)
+	    {
+	      if (!goodAgentType (agents->term))
+		{
+		  return false;
+		}
+	      agents = agents->next;
+	    }
+	}
+      run++;
+    }
+  return true;			// seems to be okay
+}
+
 //------------------------------------------------------------------------
 // Proof reporting
 //------------------------------------------------------------------------
@@ -2799,72 +2864,42 @@ prune_theorems ()
       return 1;
     }
 
-  // Check if all agents are agents (!)
+  // Check if all actors are agents for responders (initiators come next)
   run = 0;
   while (run < sys->maxruns)
     {
-      Termlist agl;
+      if (!sys->runs[run].role->initiator)
-
-      agl = sys->runs[run].agents;
-      while (agl != NULL)
 	{
-	  Term agent;
+	  Term actor;
 
-	  agent = deVar (agl->term);
+	  actor = agentOfRun (sys, run);
-	  if (agent == NULL)
+	  if (!goodAgentType (actor))
 	    {
-	      error ("Agent of run %i is NULL", run);
+	      if (switches.output == PROOF)
+		{
+		  indentPrint ();
+		  eprintf ("Pruned because the actor ");
+		  termPrint (actor);
+		  eprintf (" of run %i is not of a compatible type.\n", run);
+		}
+	      return 1;
 	    }
-	  /**
-	   * Check whether the agent of the run is of a sensible type.
-	   *
-	   * @TODO Note that this still needs a lemma.
-	   */
-	  {
-	    int sensibleagent;
-
-	    sensibleagent = true;
-
-	    if (!realTermLeaf (agent))
-	      {			// not a leaf
-		sensibleagent = false;
-	      }
-	    else
-	      {			// real leaf
-		if (switches.match == 0 || !isTermVariable (agent))
-		  {		// either strict matching, or not a variable, so we should check matching types
-		    if (agent->stype == NULL)
-		      {		// Too generic
-			sensibleagent = false;
-		      }
-		    else
-		      {		// Has a type
-			if (!inTermlist (agent->stype, TERM_Agent))
-			  {	// but not the right type
-			    sensibleagent = false;
-			  }
-		      }
-		  }
-	      }
-
-	    if (!sensibleagent)
-	      {
-		if (switches.output == PROOF)
-		  {
-		    indentPrint ();
-		    eprintf ("Pruned because the agent ");
-		    termPrint (agent);
-		    eprintf (" of run %i is not of a compatible type.\n",
-			     run);
-		  }
-		return 1;
-	      }
-	  }
-	  agl = agl->next;
 	}
       run++;
     }
 
+  // Prune wrong agents type for initators
+  if (!initiatorAgentsType ())
+    {
+      if (switches.output == PROOF)
+	{
+	  indentPrint ();
+	  eprintf
+	    ("Pruned: an initiator role does not have the correct type for one of its agents.\n");
+	}
+      return 1;
+    }
+
   // Check if all agents of the main run are valid
   if (!isRunTrusted (sys, 0))
     {

src/compiler.c

@@ -626,31 +626,48 @@ roleCompile (Term nameterm, Tac tc)
   /* parse the content of the role */
   levelInit ();
 
-  while (tc != NULL)
+  {
-    {
+    int firstEvent;
-      switch (tc->op)
+
-	{
+    /* initiator/responder flag not set */
-	case TAC_READ:
+    firstEvent = 1;
-	  commEvent (READ, tc);
+
-	  break;
+    while (tc != NULL)
-	case TAC_SEND:
+      {
-	  commEvent (SEND, tc);
+	switch (tc->op)
-	  break;
+	  {
-	case TAC_CLAIM:
+	  case TAC_READ:
-	  commEvent (CLAIM, tc);
+	    if (firstEvent)
-	  break;
+	      {
-	default:
+		// First a read, thus responder
-	  if (!normalDeclaration (tc))
+		/*
-	    {
+		 * Semantics: defaults (in role.c) to initiator _unless_ the first event is a read,
-	      printf ("ERROR: illegal command %i in role ", tc->op);
+		 * in which case we assume that the agent names are possibly received as variables
-	      termPrint (thisRole->nameterm);
+		 */
-	      printf (" ");
+		thisRole->initiator = 0;
-	      errorTac (tc->lineno);
+	      }
-	    }
+	    commEvent (READ, tc);
-	  break;
+	    break;
-	}
+	  case TAC_SEND:
-      tc = tc->next;
+	    commEvent (SEND, tc);
-    }
+	    break;
+	  case TAC_CLAIM:
+	    commEvent (CLAIM, tc);
+	    break;
+	  default:
+	    if (!normalDeclaration (tc))
+	      {
+		printf ("ERROR: illegal command %i in role ", tc->op);
+		termPrint (thisRole->nameterm);
+		printf (" ");
+		errorTac (tc->lineno);
+	      }
+	    break;
+	  }
+	firstEvent = 0;
+	tc = tc->next;
+      }
+  }
   compute_role_variables (sys, thisProtocol, thisRole);
   levelDone ();
 }

src/role.c

@@ -240,6 +240,7 @@ roleCreate (Term name)
   r->roledef = NULL;
   r->locals = NULL;
   r->variables = NULL;
+  r->initiator = 1;		//! Will be determined later, if a read is the first action (in compiler.c)
   r->next = NULL;
   return r;
 }

src/role.h

@@ -120,6 +120,8 @@ struct role
   Termlist locals;
   //! Local variables for this role.
   Termlist variables;
+  //! Flag for initiator roles
+  int initiator;
   //! Pointer to next role definition.
   struct role *next;
 };