- Fixed role comparison bug.

src/compiler.c

@@ -1950,7 +1950,8 @@ checkWellFormed (const System sys)
 
 //! Check matching role defs
 int
-checkEventMatch (const Roledef rd1, const Roledef rd2)
+checkEventMatch (const Roledef rd1, const Roledef rd2,
+		 const Termlist rolenames)
 {
   if (!isTermEqual (rd1->from, rd2->from))
     {
@@ -1960,7 +1961,7 @@ checkEventMatch (const Roledef rd1, const Roledef rd2)
     {
       return false;
     }
-  if (!checkRoletermMatch (rd1->message, rd2->message))
+  if (!checkRoletermMatch (rd1->message, rd2->message, rolenames))
     {
       return false;
     }
@@ -1992,7 +1993,7 @@ checkLabelMatchThis (const System sys, const Protocol p, const Role readrole,
 	      if (isTermEqual (event->label, readevent->label))
 		{
 		  // Same labels, so they should match up!
-		  if (!checkEventMatch (event, readevent))
+		  if (!checkEventMatch (event, readevent, p->rolenames))
 		    {
 		      globalError++;
 		      eprintf ("error: [%i]", readevent->lineno);

src/mgu.c

@@ -581,9 +581,12 @@ termMguSubTerm (Term smallterm, Term bigterm,
   return flag;
 }
 
-//! Check if terms might match in some way
+//! Check if role terms might match in some way
+/**
+ * Interesting case: role names are variables here, so they always match. We catch that case by inspecting the variable list.
+ */
 int
-checkRoletermMatch (const Term t1, const Term t2)
+checkRoletermMatch (const Term t1, const Term t2, const Termlist notmapped)
 {
   Termlist tl;
 
@@ -595,10 +598,27 @@ checkRoletermMatch (const Term t1, const Term t2)
     }
   else
     {
+      int result;
+      Termlist vl;
+
+      result = true;
       // Reset variables
       termlistSubstReset (tl);
+      // Check variable list etc: should not contain mapped role names
+      vl = tl;
+      while (vl != NULL)
+	{
+	  // This term should not be in the notmapped list
+	  if (inTermlist (notmapped, vl->term))
+	    {
+	      result = false;
+	      break;
+	    }
+	  vl = vl->next;
+
+	}
       // Remove list
       termlistDelete (tl);
-      return true;
+      return result;
     }
 }

src/mgu.h

@@ -19,7 +19,7 @@ int termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist));
 int termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
 		    Termlist inverses, Termlist keylist);
 void termlistSubstReset (Termlist tl);
-int checkRoletermMatch (Term t1, Term t2);
+int checkRoletermMatch (const Term t1, const Term t2, const Termlist tl);
 
 // The new iteration methods
 int unify (Term t1, Term t2, Termlist tl, int (*callback) (Termlist));

src/parser.y

@@ -318,7 +318,7 @@ int yyerror(char *s)
 	extern int yylineno;	//!< defined and maintained in lex.c
 	extern char *yytext;	//!< defined and maintained in lex.c
   
-	error ("%s at symbol '%s' on line %i.\n", s, yytext, yylineno);
+	error ("[%i] %s at symbol '%s'.\n", yylineno, s, yytext);
 	return 0;
 }