X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=cyclegraph.cc;h=479ddf852fcc0440f1f0850867fca5dd87ddfab3;hb=5467ad92b9043ee54e3c64d661277751c43a355f;hp=58cb79f22cdd573acf59e24976014c91731e6e7e;hpb=82357a7b7cc6e7395609894a8c8a705aa5af7e4e;p=model-checker.git

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 58cb79f..479ddf8 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -429,3 +429,19 @@ bool CycleNode::setRMW(CycleNode *node)
 	hasRMW = node;
 	return false;
 }
+
+/**
+ * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be
+ * used when there's no existing ModelAction CycleNode for this write.
+ *
+ * @param writer The ModelAction which wrote the future value represented by
+ * this CycleNode
+ */
+void CycleNode::resolvePromise(const ModelAction *writer)
+{
+	ASSERT(is_promise());
+	ASSERT(promise->is_compatible(writer));
+	action = writer;
+	promise = NULL;
+	ASSERT(!is_promise());
+}