Implemented well-formedness check as in the 2012 book.

We check that variables occur first in receive events.

src/compiler.c

@@ -2263,62 +2263,74 @@ checkUnusedVariables (const System sys)
     }
 }
 
-//! Is a complete role well-formed
+//! Is a role well-formed?
+/**
+ * In line with the 2012 book, we check only that variables occur first in
+ * receives. This is needed to guarantee that the instantiated terms are ground
+ * (and hence, traces contain run terms).
+ *
+ * Returns true if the role is well-formed, false otherwise.
+ *
+ * The function outputs its own error messages, but does not (sys.)exit. This
+ * should be done by the calling function, in order to collect a complete error
+ * report for all roles.
+ */
 int
 WellFormedRole (const System sys, Protocol p, Role r)
 {
-  Knowledge know;
-  int okay;
-  Roledef rd;
+  Termlist tl;
+  int allOkay;
 
-  okay = true;
-  know = emptyKnowledge ();
-  // Transfer inverses
-  know->inverses = sys->know->inverses;
-  // Add role knowledge
-  knowledgeAddTermlist (know, r->knows);
-  // Add role names
-  //@TODO this is not in the semantics as such, often implicit
-  knowledgeAddTermlist (know, p->rolenames);
-  // Add local constants
-  //@TODO this is not in the semantics as such, often implicit
-  knowledgeAddTermlist (know, r->declaredconsts);
-
-  // Test
-  rd = r->roledef;
-  while (rd != NULL)
+  allOkay = true;
+  for (tl = r->variables; tl != NULL; tl = tl->next)
     {
-      Knowledge knowres;
+      if (!inTermlist (p->rolenames, tl->term))
+	{
+	  Roledef rd;
 
-      knowres = WellFormedEvent (r->nameterm, know, rd);
-      if (knowres == NULL)
-	{
-	  okay = false;
-	  break;
-	}
-      else
-	{
-	  know = knowres;
-	  rd = rd->next;
+	  rd = firstEventWithTerm (r->roledef, tl->term);
+	  if (rd->type != RECV)
+	    {
+	      // Not well-formed
+	      globalError++;
+	      error_pre ();
+	      eprintf ("Protocol ");
+	      termPrint (p->nameterm);
+	      eprintf (", role ");
+	      termPrint (r->nameterm);
+	      eprintf (" is not well-formed: the variable '");
+	      termPrint (tl->term);
+	      eprintf ("' should occur first in a receive event.\n");
+	      globalError--;
+
+	      // Store
+	      allOkay = false;
+	    }
 	}
     }
-
-  // clean up
-  knowledgeDelete (know);
-  return okay;
+  return allOkay;
 }
 
 //! Well-formedness check
 void
 checkWellFormed (const System sys)
 {
+  int allOkay;
+
+  allOkay = true;
+
   int thisRole (Protocol p, Role r)
   {
-    WellFormedRole (sys, p, r);
+    allOkay = allOkay && WellFormedRole (sys, p, r);
     return true;
   }
 
   iterateRoles (sys, thisRole);
+  if (allOkay == false)
+    {
+      error
+	("The protocol specification does not meet the well-formedness condition.");
+    }
 }
 
 //! Check matching role defs
@@ -2542,10 +2554,5 @@ preprocess (const System sys)
   /*
    * Check well-formedness
    */
-  /* TODO Temporarily disabled wellformedness check (well-formedness) after Simon bug reporting.
-     if (sys->knowledgedefined)
-     {
-     checkWellFormed (sys);
-     }
-   */
+  checkWellFormed (sys);
 }

src/role.c

@@ -459,76 +459,17 @@ wfeError (Knowledge know, Roledef rd, char *errorstring, Term was,
 }
 
 
-//! Is an event well-formed
-/**
- * Returns the new knowledge or NULL if it was not well-formed.
- */
-Knowledge
-WellFormedEvent (Term role, Knowledge know, Roledef rd)
+//! Return the first event (or NULL) in which a term occurs
+Roledef
+firstEventWithTerm (Roledef rd, Term t)
 {
-  if (rd == NULL)
+  while (rd != NULL)
     {
-      return know;
+      if (termSubTerm (rd->message, t))
+	{
+	  return rd;
+	}
+      rd = rd->next;
     }
-  if (rd->type == RECV)
-    {
-      // Read
-      if (!isTermEqual (role, rd->to))
-	{
-	  wfeError (know, rd, "Receiving role incorrect.", rd->to, role);
-	  return NULL;
-	}
-      if (!inKnowledge (know, rd->from))
-	{
-	  wfeError (know, rd, "Unknown sender role.", rd->from, NULL);
-	  return NULL;
-
-	}
-      if (!Readable (know, rd->message))
-	{
-	  wfeError (know, rd, "Cannot read message pattern.", rd->message,
-		    NULL);
-	  return NULL;
-	}
-      knowledgeAddTerm (know, rd->message);
-      return know;
-    }
-  if (rd->type == SEND)
-    {
-      // Send
-      if (!isTermEqual (role, rd->from))
-	{
-	  wfeError (know, rd, "Sending role incorrect.", rd->from, role);
-	  return NULL;
-	}
-      if (!inKnowledge (know, rd->to))
-	{
-	  wfeError (know, rd, "Unknown receiving role.", rd->to, NULL);
-	  return NULL;
-
-	}
-      if (!inKnowledge (know, rd->message))
-	{
-	  wfeError (know, rd, "Unable to construct message.", rd->message,
-		    NULL);
-	  return NULL;
-	}
-      return know;
-    }
-  if (rd->type == CLAIM)
-    {
-      // Claim
-      if (!isTermEqual (role, rd->from))
-	{
-	  wfeError (know, rd, "Claiming role incorrect.", rd->from, role);
-	  return NULL;
-	}
-      return know;
-    }
-  // Unknown, false
-  globalError++;
-  roledefPrint (rd);
-  globalError--;
-  error ("I don't know this event");
   return NULL;
 }

src/role.h

@@ -188,6 +188,6 @@ int roledef_iterate_events (Roledef rd, int (*func) ());
 int roledef_length (const Roledef rd);
 Roledef roledef_shift (Roledef rd, int i);
 int roledefSubTerm (Roledef rd, Term tsub);
-Knowledge WellFormedEvent (Term role, Knowledge know, Roledef rd);
+Roledef firstEventWithTerm (Roledef rd, Term t);
 
 #endif