- Better filter.

src/compiler.c

@@ -421,10 +421,15 @@ isClaimlabelUsed (const System sys, const Term label)
 
 //! Generate a fresh claim label
 Term
-generateFreshClaimlabel (const System sys, const Role role, const Term claim)
+generateFreshClaimlabel (const System sys, const Protocol protocol,
+			 const Role role, const Term claim)
 {
+  Term label;
+
   /* Simply use the role as a prefix */
-  return freshTermPrefix (role->nameterm);
+  label = freshTermPrefix (role->nameterm);
+  label = makeTermTuple (protocol->nameterm, label);
+  return label;
 }
 
 //! Create a claim and add it to the claims list, and add the role event.
@@ -435,6 +440,14 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
   Claimlist cl;
   Term labeltuple;
 
+  /* generate full unique label */
+  /* is the label empty or used? */
+  if (label == NULL || isClaimlabelUsed (sys, label))
+    {
+      /* simply generate a fresh one */
+      label = generateFreshClaimlabel (sys, protocol, role, claim);
+    }
+
   if (switches.filterProtocol != NULL)
     {
       // only this protocol
@@ -447,27 +460,26 @@ claimCreate (const System sys, const Protocol protocol, const Role role,
       // and maybe also a specific label?
       if (switches.filterLabel != NULL)
 	{
-	  Term t;
+	  if (label == NULL)
-
-	  t = label;
-	  while (isTermTuple (t))
 	    {
-	      t = TermOp2 (t);
-	    }
-	  if (strcmp (switches.filterLabel, TermSymb (t)->text) != 0)
-	    {
-	      // not this label; return
 	      return NULL;
 	    }
-	}
+	  else
-    }
+	    {
+	      Term t;
 
-  /* generate full unique label */
+	      t = label;
-  /* is the label empty or used? */
+	      while (isTermTuple (t))
-  if (label == NULL || isClaimlabelUsed (sys, label))
+		{
-    {
+		  t = TermOp2 (t);
-      /* simply generate a fresh one */
+		}
-      label = generateFreshClaimlabel (sys, role, claim);
+	      if (strcmp (switches.filterLabel, TermSymb (t)->text) != 0)
+		{
+		  // not this label; return
+		  return NULL;
+		}
+	    }
+	}
     }
 
   // Assert: label is unique, add claimlist info
@@ -710,6 +722,7 @@ commEvent (int event, Tac tc)
 		    ("Claim label is not unique at line %i, generating fresh label.",
 		     tc->lineno);
 		}
+	      // the reported new label will be generated later in claimCreate()
 	    }
 
 	  if (!isTermEqual (fromrole, thisRole->nameterm))

src/switches.c

@@ -495,12 +495,12 @@ switcher (const int process, int index, int commandline)
 	}
     }
 
-  if (detect (' ', "claim", 1))
+  if (detect (' ', "filter", 1))
     {
       if (!process)
 	{
-	  helptext ("--claim=<protocol>[,<label>]",
+	  helptext ("--filter=<protocol>[,<label>]",
-		    "check only a certain claim");
+		    "check only certain claims");
 	}
       else
 	{

src/todo.txt

@@ -1,3 +1,5 @@
+- There is something weird when automatically generating claim labels
+  and trying to filter on them (try eg duplicates)
 - --check is slightly f***ed up because there is no good semantics for
   the --disable intruder check. As a result, it is now too strict can
   cause correct protocols to fail. Fix.