X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=scanalysis.cc;h=d4102fe8b6a20148ff30ae5a83cdaf506f2753df;hp=75aed1aa80ed994985fee2b67ff69e83b37a67cb;hb=d28d1a3b7aafbcd2caf80de26721293126830fa8;hpb=71d6e3e2eaa2d8653fa4d9cf9dd57b745f07321d

diff --git a/scanalysis.cc b/scanalysis.cc
index 75aed1a..d4102fe 100644
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -29,9 +29,8 @@ void SCAnalysis::print_list(action_list_t *list) {
 			if (badrfset.contains(act))
 				model_print("BRF ");
 			act->print();
-			cvmap.get(act)->print();
 			if (badrfset.contains(act)) {
-				model_print("DESIRED %u \n",badrfset.get(act)->get_seq_number());
+				model_print("Desired Rf: %u \n",badrfset.get(act)->get_seq_number());
 			}
 		}
 		hash = hash ^ (hash << 3) ^ ((*it)->hash());
@@ -82,7 +81,7 @@ ModelAction * SCAnalysis::getNextAction() {
 			continue;
 		ModelAction *first = threadlist->front();
 		if (act==NULL) {
-			act=first;
+			act = first;
 			continue;
 		}
 		ClockVector *cv = cvmap.get(act);
@@ -93,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.
 	 */
 
@@ -102,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;
 		}
 	}
 
@@ -136,7 +145,10 @@ action_list_t * SCAnalysis::generateSC(action_list_t *list) {
 		//add ordering constraints from this choice
 		if (updateConstraints(act)) {
 			//propagate changes if we have them
+			bool oc=cyclic;
 			computeCV(list);
+			if (!oc && cyclic)
+				model_print("XXXXXXXXXXXXXX\n");
 		}
 		//add action to end
 		sclist->push_back(act);