From: Brian Demsky <bdemsky@uci.edu>
Date: Tue, 23 Apr 2013 00:19:25 +0000 (-0700)
Subject: bug...will sometimes print SC traces in a bad order
X-Git-Tag: oopsla2013~25^2
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=272b974c7723aa1cdbd0aca911f7fd8c7bcbfcf5;p=model-checker.git

bug...will sometimes print SC traces in a bad order
---

diff --git a/scanalysis.cc b/scanalysis.cc
index f2b40d5..8aa400c 100644
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -81,7 +81,7 @@ ModelAction * SCAnalysis::getNextAction() {
 			continue;
 		ModelAction *first = threadlist->front();
 		if (act==NULL) {
-			act=first;
+			act = first;
 			continue;
 		}
 		ClockVector *cv = cvmap.get(act);
@@ -92,7 +92,6 @@ ModelAction * SCAnalysis::getNextAction() {
 	if (act == NULL)
 		return act;
 
-
 	/* Find the model action with the earliest sequence number in case of a cycle.
 	 */
 
@@ -101,11 +100,22 @@ ModelAction * SCAnalysis::getNextAction() {
 		if (threadlist->empty())
 			continue;
 		ModelAction *first = threadlist->front();
-		ClockVector *cv = cvmap.get(act);
 		ClockVector *cvfirst = cvmap.get(first);
-		if (first->get_seq_number()<act->get_seq_number()&&
-				(cv->synchronized_since(first)||!cvfirst->synchronized_since(act))) {
-			act=first;
+		if (first->get_seq_number()<act->get_seq_number()) {
+			bool candidate=true;
+			for (int j = 0; j <= maxthreads; j++) {
+				action_list_t *threadlist2 = &threadlists[j];
+				if (threadlist2->empty())
+					continue;
+				ModelAction *check = threadlist2->front();
+				if ((check!=first) &&
+						cvfirst->synchronized_since(check)) {
+					candidate=false;
+					break;
+				}
+			}
+			if (candidate)
+				act=first;
 		}
 	}