X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=scanalysis.cc;h=abed220873450b67ad5776509a8210f2c5457c51;hb=5566833b04fb088b315dcde5148e05a9ea80c2df;hp=daf41f8a19ba4395d61dff065f71422a422547dc;hpb=50e0465f724dc182d5d7504004e93f1a1b4644b9;p=model-checker.git

diff --git a/scanalysis.cc b/scanalysis.cc
index daf41f8..abed220 100644
--- a/scanalysis.cc
+++ b/scanalysis.cc
@@ -51,13 +51,14 @@ bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, ClockVector *cv2
 
 ModelAction * SCAnalysis::getNextAction() {
 	ModelAction *act = NULL;
+	/* Find the earliest in SC ordering */
 	for (int i = 0; i <= maxthreads; i++) {
 		action_list_t *threadlist = &threadlists[i];
 		if (threadlist->empty())
 			continue;
 		ModelAction *first = threadlist->front();
-		if (act == NULL) {
-			act = first;
+		if (act==NULL) {
+			act=first;
 			continue;
 		}
 		ClockVector *cv = cvmap.get(act);
@@ -67,29 +68,35 @@ ModelAction * SCAnalysis::getNextAction() {
 	}
 	if (act == NULL)
 		return act;
-	//print cycles in a nice way to avoid confusion
-	//make sure thread starts appear after the create
-	if (act->is_thread_start()) {
-		ModelAction *createact = execution->get_thread(act)->get_creation();
-		if (createact) {
-			action_list_t *threadlist = &threadlists[id_to_int(createact->get_tid())];
-			if (!threadlist->empty()) {
-				ModelAction *first = threadlist->front();
-				if (first->get_seq_number() <= createact->get_seq_number())
-					act = first;
-			}
+
+
+	/* Find the model action with the earliest sequence number in case of a cycle.
+	 */
+
+	for (int i = 0; i <= maxthreads; i++) {
+		action_list_t *threadlist = &threadlists[i];
+		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;
 		}
 	}
 
-	//make sure that joins appear after the thread is finished
-	if (act->is_thread_join()) {
-		int jointhread = id_to_int(act->get_thread_operand()->get_id());
-		action_list_t *threadlist = &threadlists[jointhread];
-		if (!threadlist->empty()) {
-			act = threadlist->front();
+	/* See if hb demands an earlier action. */
+	for (int i = 0; i <= maxthreads; i++) {
+		action_list_t *threadlist = &threadlists[i];
+		if (threadlist->empty())
+			continue;
+		ModelAction *first = threadlist->front();
+		ClockVector *cv = act->get_cv();
+		if (cv->synchronized_since(first)) {
+			act = first;
 		}
 	}
-
 	return act;
 }