From 6dff931dbcb0b31e8a602cc9c30f3325bb184e74 Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 25 Apr 2006 13:58:14 +0000
Subject: [PATCH] - Term identifiers can now contain primes (SM) - If labels
 start with a bang (!), they are ignored in synch/agree   claims.

---
 src/binding.c | 19 +++++++++++--------
 src/claim.c   | 25 ++++++++++++++-----------
 src/label.c   | 26 ++++++++++++++++++++++++++
 src/label.h   |  1 +
 src/scanner.l |  2 +-
 src/todo.txt  |  2 --
 6 files changed, 53 insertions(+), 22 deletions(-)

diff --git a/src/binding.c b/src/binding.c
index ef687c7..ba2197a 100644
--- a/src/binding.c
+++ b/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;
     }
diff --git a/src/claim.c b/src/claim.c
index 57701c2..fcbb333 100644
--- a/src/claim.c
+++ b/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;
diff --git a/src/label.c b/src/label.c
index 7d5d5cf..20a2fad 100644
--- a/src/label.c
+++ b/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;
 }
 
diff --git a/src/label.h b/src/label.h
index 434a1e3..ee80809 100644
--- a/src/label.h
+++ b/src/label.h
@@ -11,6 +11,7 @@
 struct labelinfo
 {
   Term label;
+  int ignore;
   Protocol protocol;
   Term sendrole;
   Term readrole;
diff --git a/src/scanner.l b/src/scanner.l
index 5219934..1c0cfc4 100644
--- a/src/scanner.l
+++ b/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
  */
diff --git a/src/todo.txt b/src/todo.txt
index 2f0f623..d13af21 100644
--- a/src/todo.txt
+++ b/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