X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=scanalysis.cc;h=8aa400c239223a8d90ef1119126bdd87cb163b8f;hb=272b974c7723aa1cdbd0aca911f7fd8c7bcbfcf5;hp=f2b40d5d1a4e6dbbaba13c489ad1469648baf876;hpb=df90b0b969acc3002305692532efab2f0a5a9f49;p=model-checker.git

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