- Better error reporting for local order constraints.

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 (roledef_shift (sys->runs[r1].start, e1)->type == READ)
-	      if (e2 >= 0)
 		{
-
+		  e2 = firstOccurrence (sys, r2, t, SEND);
-		  // thus, it should not be the case that e1 occurs before e2
+		  if (e2 >= 0)
-		  if (isDependEvent (r1, e1, r2, e2))
 		    {
-		      // That's not good!
+		      // thus, it should not be the case that e1 occurs before e2
-		      if (switches.output == PROOF)
+		      if (isDependEvent (r1, e1, r2, e2))
 			{
-			  indentPrint ();
+			  // That's not good!
-			  eprintf ("Pruned because ordering for term ");
+			  if (switches.output == PROOF)
-			  termSubstPrint (t);
+			    {
-			  eprintf
+			      indentPrint ();
-			    (" cannot be correct: the first send r%ii%i occurs after the read r%ii%i.\n",
+			      eprintf ("Pruned because ordering for term ");
-			     r2, e2, r1, e1);
+			      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");
+		}
 	    }
-	}
+	  else
-      return true;
+	    {
+	      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);

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
 /**

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);
       }