From 527bf8baa543ab3bf3de102a58148c84f26b797a Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Tue, 28 Feb 2006 15:33:12 +0000
Subject: [PATCH] - Better error reporting for local order constraints.

---
 src/prune_theorems.c | 72 +++++++++++++++++++++++++++++++++-----------
 src/role.h           |  2 +-
 src/system.c         |  5 ++-
 3 files changed, 59 insertions(+), 20 deletions(-)

diff --git a/src/prune_theorems.c b/src/prune_theorems.c
index d0ee503..26c29c1 100644
--- a/src/prune_theorems.c
+++ b/src/prune_theorems.c
@@ -39,34 +39,70 @@ correctLocalOrder (const System sys)
 
 	  // t is a term from r2 that occurs in r1
 	  r2 = TermRunid (t);
-	  e1 = firstOccurrence (sys, r1, t, READ);
+	  e1 = firstOccurrence (sys, r1, t, ANYEVENT);
 	  if (e1 >= 0)
 	    {
-	      e2 = firstOccurrence (sys, r2, t, SEND);
-	      if (e2 >= 0)
+	      if (roledef_shift (sys->runs[r1].start, e1)->type == READ)
 		{
-
-		  // thus, it should not be the case that e1 occurs before e2
-		  if (isDependEvent (r1, e1, r2, e2))
+		  e2 = firstOccurrence (sys, r2, t, SEND);
+		  if (e2 >= 0)
 		    {
-		      // That's not good!
-		      if (switches.output == PROOF)
+		      // thus, it should not be the case that e1 occurs before e2
+		      if (isDependEvent (r1, e1, r2, e2))
 			{
-			  indentPrint ();
-			  eprintf ("Pruned because ordering for term ");
-			  termSubstPrint (t);
-			  eprintf
-			    (" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n",
-			     r2, e2, r1, e1);
+			  // That's not good!
+			  if (switches.output == PROOF)
+			    {
+			      indentPrint ();
+			      eprintf ("Pruned because ordering for term ");
+			      termSubstPrint (t);
+			      eprintf
+				(" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n",
+				 r2, e2, r1, e1);
+			    }
+			  flag = false;
+			  return false;
 			}
-		      flag = false;
-		      return false;
+		    }
+		  else
+		    {
+		      globalError++;
+		      eprintf ("Error: term ");
+		      termSubstPrint (t);
+		      eprintf
+			(" from run %i should occur in run %i, but it doesn't.\n",
+			 r2, r2);
+		      globalError--;
+		      error ("Abort");
 		    }
 		}
+	      else
+		{
+		  // not a read first?
+		  globalError++;
+		  eprintf ("Error: term ");
+		  termSubstPrint (t);
+		  eprintf
+		    (" from run %i should occur in run %i first in a READ event, but it occurs first in another event.\n",
+		     r2, r1);
+		  globalError--;
+		  error ("Abort");
+		}
 	    }
-	}
-      return true;
+	  else
+	    {
+	      globalError++;
+	      eprintf ("Error: term ");
+	      termSubstPrint (t);
+	      eprintf
+		(" from run %i should occur in run %i, but it doesn't.\n", r2,
+		 r1);
+	      globalError--;
+	      error ("Abort");
+	    }
+	  return true;
 
+	}
     }
 
     return iterateLocalToOther (sys, r1, checkTerm);
diff --git a/src/role.h b/src/role.h
index 79ad2b7..8e3036e 100644
--- a/src/role.h
+++ b/src/role.h
@@ -9,7 +9,7 @@
 #include "states.h"
 
 enum eventtype
-{ READ, SEND, CLAIM };
+{ READ, SEND, CLAIM, ANYEVENT };
 
 //! The container for the claim info list
 /**
diff --git a/src/system.c b/src/system.c
index 2bac96f..008202e 100644
--- a/src/system.c
+++ b/src/system.c
@@ -1576,13 +1576,16 @@ iterateEvents (const System sys, const int run,
 }
 
 // Iterate over event type in a certain run (increasing through role)
+/**
+ * If evtype == ANYEVENT then it does not matter.
+ */
 int
 iterateEventsType (const System sys, const int run, const int evtype,
 		   int (*callback) (Roledef rd, int ev))
 {
   int selectEvent (Roledef rd, int e)
   {
-    if (rd->type == evtype)
+    if (evtype == ANYEVENT || rd->type == evtype)
       {
 	return callback (rd, e);
       }