X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=7f1e49dc0ee0fbce09ecda84a3b044dfec311bbe;hb=942ca53513b4c50f3f73bc4b123c3552dbc71ca6;hp=9faf4e2a28eb26b7c7891114f86592aee80480b9;hpb=3262ae1f816dea735cab52d6940523f52ca80fe1;p=model-checker.git

diff --git a/model.cc b/model.cc
index 9faf4e2..7f1e49d 100644
--- a/model.cc
+++ b/model.cc
@@ -447,8 +447,24 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		case WORK_CHECK_RELEASE_SEQ:
 			resolve_release_sequences(work.location, &work_queue);
 			break;
-		case WORK_CHECK_MO_EDGES:
-			/** @todo Perform follow-up mo_graph checks */
+		case WORK_CHECK_MO_EDGES: {
+			/** @todo Complete verification of work_queue */
+			ModelAction *act = work.action;
+			bool updated = false;
+
+			if (act->is_read()) {
+				if (r_modification_order(act, act->get_reads_from()))
+					updated = true;
+			}
+			if (act->is_write()) {
+				if (w_modification_order(act))
+					updated = true;
+			}
+
+			if (updated)
+				work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
+			break;
+		}
 		default:
 			ASSERT(false);
 			break;