- Term identifiers can now contain primes (SM)

- If labels start with a bang (!), they are ignored in synch/agree
  claims.

src/binding.c

@@ -343,16 +343,19 @@ labels_ordered (Termmap runs, Termlist labels)
       }
 
       linfo = label_find (sys->labellist, labels->term);
-      send_run = termmapGet (runs, linfo->sendrole);
-      read_run = termmapGet (runs, linfo->readrole);
-      send_ev = get_index (send_run);
-      read_ev = get_index (read_run);
-      if (!isDependEvent (send_run, send_ev, read_run, read_ev))
+      if (!linfo->ignore)
 	{
-	  // Not ordered; false
-	  return false;
-	}
+	  send_run = termmapGet (runs, linfo->sendrole);
+	  read_run = termmapGet (runs, linfo->readrole);
+	  send_ev = get_index (send_run);
+	  read_ev = get_index (read_run);
+	  if (!isDependEvent (send_run, send_ev, read_run, read_ev))
+	    {
+	      // Not ordered; false
+	      return false;
+	    }
 
+	}
       // Proceed
       labels = labels->next;
     }

src/claim.c

@@ -569,22 +569,25 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs)
 
       // Main
       linfo = label_find (sys->labellist, labels->term);
-      rd_send = get_label_event (linfo->sendrole, labels->term);
-      rd_read = get_label_event (linfo->readrole, labels->term);
+      if (!linfo->ignore)
+	{
+	  rd_send = get_label_event (linfo->sendrole, labels->term);
+	  rd_read = get_label_event (linfo->readrole, labels->term);
 
-      if (rd_send == NULL || rd_read == NULL)
-	{
-	  // False!
-	  flag = 0;
-	}
-      else
-	{
-	  // Compare
-	  if (events_match_rd (rd_send, rd_read) != MATCH_CONTENT)
+	  if (rd_send == NULL || rd_read == NULL)
 	    {
 	      // False!
 	      flag = 0;
 	    }
+	  else
+	    {
+	      // Compare
+	      if (events_match_rd (rd_send, rd_read) != MATCH_CONTENT)
+		{
+		  // False!
+		  flag = 0;
+		}
+	    }
 	}
 
       labels = labels->next;

src/label.c

@@ -8,17 +8,43 @@
 #include "list.h"
 #include "system.h"
 
+//! Retrieve rightmost thing of label
+Term
+rightMostTerm (Term t)
+{
+  if (t != NULL)
+    {
+      t = deVar (t);
+      if (realTermTuple (t))
+	{
+	  return rightMostTerm (TermOp2 (t));
+	}
+    }
+  return t;
+}
+
 //! Create a new labelinfo node
 Labelinfo
 label_create (const Term label, const Protocol protocol)
 {
   Labelinfo li;
+  Term tl;
 
   li = (Labelinfo) malloc (sizeof (struct labelinfo));
   li->label = label;
   li->protocol = protocol;
   li->sendrole = NULL;
   li->readrole = NULL;
+  // Should we ignore it?
+  li->ignore = false;
+  tl = rightMostTerm (label);
+  if (tl != NULL)
+    {
+      if (TermSymb (tl)->text[0] == '!')
+	{
+	  li->ignore = true;
+	}
+    }
   return li;
 }
 

src/label.h

@@ -11,6 +11,7 @@
 struct labelinfo
 {
   Term label;
+  int ignore;
   Protocol protocol;
   Term sendrole;
   Term readrole;

src/scanner.l

@@ -45,7 +45,7 @@ ascii_char	[^\"\n]
 escaped_char	\\n|\\\"
 integer		{digit}+
 text		\"({ascii_char}|{escaped_char})*\"
-id		@?({letter}|{digit}|[\^\-])+
+id		@?({letter}|{digit}|[\^\-!'])+
 
 /* the "incl" state is used for picking up the name of an include file
  */

src/todo.txt

@@ -6,8 +6,6 @@
 - Test 'sk(x)' in goals, somewhere before assessing a state (dus at the
   beginning of iterate), immediately reduce to 'sk(Eve)'. Test with
   --experimental. To that end, reintroduce a state-reporting switch.
-- Scyther mailing list especially for students, this is where they
-  should report any questions, when Erik starts the course.
 - It is currently not well-defined to define inversekeys within a role:
   this requires some work at instantiation, because instantiated term
   couples should be added to the inverses list, and removed at