X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.h;h=6d892cbfeabeb92db267f1cc718b30972560371d;hb=9a89975eb7aa3c818124382fc04cc8e8d51dbaaa;hp=c5d85a42f8010f55e47105802ef71e72083bd810;hpb=74d93da009212a1d375b4fd5baede4dde82f3115;p=model-checker.git

diff --git a/model.h b/model.h
index c5d85a4..6d892cb 100644
--- a/model.h
+++ b/model.h
@@ -187,12 +187,12 @@ private:
 	std::vector<struct PendingFutureValue> *futurevalues;
 
 	/**
-	 * List of acquire actions that might synchronize with one or more
-	 * release sequence. Release sequences might be determined lazily as
-	 * promises are fulfilled and modification orders are established. Each
-	 * ModelAction in this list must be an acquire operation.
+	 * List of pending release sequences. Release sequences might be
+	 * determined lazily as promises are fulfilled and modification orders
+	 * are established. Each entry in the list may only be partially
+	 * filled, depending on its pending status.
 	 */
-	std::vector<ModelAction *> *pending_acq_rel_seq;
+	std::vector<struct release_seq *> *pending_rel_seqs;
 
 	std::vector<ModelAction *> *thrd_last_action;
 	NodeStack *node_stack;