- Made the label naming unique, by adding tuple info with the protocol

name. Now, we can simply test multiple protocol names by
  concatenation.
- Removed the pointer equality leaf hypothesis, as it didn't hold
  anymore.

src/compiler.c

@@ -20,6 +20,11 @@
 static System sys;
 static Tac tac_root;
 
+/*
+ * Declaration from system.c
+ */
+extern int protocolCount;
+
 /*
    Forward declarations.
 */
@@ -386,7 +391,9 @@ commEvent (int event, Tac tc)
 	{
 	  /* effectively, labels are bound to the protocol */
 	  level--;
-	  label = levelConst (tc->t1.sym);
+	  /* leaves a garbage tuple. dunnoh what to do with it */
+	  label =
+	    makeTermTuple (thisProtocol->nameterm, levelConst (tc->t1.sym));
 	  level++;
 	}
     }
@@ -712,6 +719,7 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
   /* add protocol to list */
   pr->next = sys->protocols;
   sys->protocols = pr;
+  protocolCount++;
 
   levelInit ();
   /* add the role names */

src/role.c

@@ -17,6 +17,7 @@
 #include "role.h"
 
 extern int globalLatex;		// from system.c
+extern int protocolCount;	// from system.c
 
 //! Allocate memory the size of a roledef struct.
 Roledef
@@ -50,16 +51,27 @@ roledefPrint (Roledef rd)
     eprintf ("CLAIM");
   if (rd->label != NULL)
     {
+      //! Print label
+      Term label;
+
+      label = deVar (rd->label);
+      if (protocolCount < 2 && realTermTuple (label))
+	{
+	  // Only one protocol, so we don't need to show the extra label info
+	  label = label->right.op2;
+	}
+
+      //! Print latex/normal
       if (globalLatex)
 	{
 	  eprintf ("$_{");
-	  termPrint (rd->label);
+	  termPrint (label);
 	  eprintf ("}$");
 	}
       else
 	{
 	  eprintf ("_");
-	  termPrint (rd->label);
+	  termPrint (label);
 	}
     }
   if (globalLatex)

src/system.c

@@ -25,6 +25,9 @@ extern Term TERM_Type;
  */
 int globalLatex;
 
+//! Global count of protocols
+int protocolCount;
+
 //! Switch for indent or not.
 static int indentState = 0;
 //! Current indent depth.
@@ -82,6 +85,7 @@ systemInit ()
   sys->maxruns = 0;
   sys->runs = NULL;
   /* no protocols yet */
+  protocolCount = 0;
   sys->protocols = NULL;
   sys->locals = NULL;
   sys->variables = NULL;

src/term.c

@@ -176,23 +176,7 @@ hasTermVariable (Term term)
 int
 isTermEqualDebug (Term t1, Term t2)
 {
-  int test1, test2;
+  return isTermEqualFn (t1, t2);
-
-  t1 = deVar (t1);
-  t2 = deVar (t2);
-
-  test1 = isTermEqualFn (t1, t2);
-  if (!(realTermLeaf (t1) && realTermLeaf (t2)))
-    {
-      return test1;
-    }
-
-  test2 = (t1 == t2);
-  if (test1 != test2)
-    {
-      error ("Pointer equality hypothesis for leaves does not hold!");
-    }
-  return test1;
 }
 
 //!Tests whether two terms are completely identical.
@@ -222,19 +206,8 @@ isTermEqualFn (Term term1, Term term2)
     }
   if (realTermLeaf (term1))
     {
-#ifdef DEBUG
+      return (term1->left.symb == term2->left.symb
-      int test;
-
-      test = (term1->left.symb == term2->left.symb
 	      && term1->right.runid == term2->right.runid);
-      if (test)
-	{
-	  error ("Strange node equality detected, should not occur.");
-	}
-      return test;
-#else
-      return 0;
-#endif
     }
   else
     {

src/term.h

@@ -89,7 +89,7 @@ int isTermEqualDebug (Term t1, Term t2);
 						?	0 \
 						:	( \
 							realTermLeaf(t1) \
-							?	0 \
+							?	isTermEqualFn(t1,t2) \
 							:	( \
 								realTermEncrypt(t2) \
 								?	(isTermEqualFn(t1->right.key, t2->right.key) && \
@@ -112,7 +112,7 @@ int isTermEqualDebug (Term t1, Term t2);
 						?	0 \
 						:	( \
 							realTermLeaf(t1) \
-							?	0 \
+							?	isTermEqualFn(t1,t2) \
 							:	( \
 								realTermEncrypt(t2) \
 								?	(isTermEqual1(t1->right.key, t2->right.key) && \
@@ -135,7 +135,7 @@ int isTermEqualDebug (Term t1, Term t2);
 						?	0 \
 						:	( \
 							realTermLeaf(t1) \
-							?	0 \
+							?	isTermEqualFn(t1,t2) \
 							:	( \
 								realTermEncrypt(t2) \
 								?	(isTermEqual2(t1->right.key, t2->right.key) && \