+ if (parent)
+ cv = new ClockVector(parent->cv, this);
+ else
+ cv = new ClockVector(NULL, this);
+}
+
+void ModelAction::set_try_lock(bool obtainedlock) {
+ if (obtainedlock)
+ value = VALUE_TRYSUCCESS;
+ else
+ value = VALUE_TRYFAILED;
+}
+
+/** @return The Node associated with this ModelAction */
+Node * ModelAction::get_node() const
+{
+ /* UNINIT actions do not have a Node */
+ ASSERT(!is_uninitialized());
+ return node;
+}
+
+/**
+ * Update the model action's read_from action
+ * @param act The action to read from; should be a write
+ */
+void ModelAction::set_read_from(const ModelAction *act)
+{
+ reads_from = act;
+ reads_from_promise = NULL;
+ if (act && act->is_uninitialized())
+ model->assert_bug("May read from uninitialized atomic\n");
+}
+
+/**
+ * Set this action's read-from promise
+ * @param promise The promise to read from
+ */
+void ModelAction::set_read_from_promise(const Promise *promise)
+{
+ ASSERT(is_read());
+ reads_from_promise = promise;
+ reads_from = NULL;
+}
+
+/**
+ * Synchronize the current thread with the thread corresponding to the
+ * ModelAction parameter.
+ * @param act The ModelAction to synchronize with
+ * @return True if this is a valid synchronization; false otherwise
+ */
+bool ModelAction::synchronize_with(const ModelAction *act)
+{
+ if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK)
+ return false;
+ model->check_promises(act->get_tid(), cv, act->cv);
+ cv->merge(act->cv);
+ return true;
+}
+
+bool ModelAction::has_synchronized_with(const ModelAction *act) const
+{
+ return cv->synchronized_since(act);
+}
+
+/**
+ * Check whether 'this' happens before act, according to the memory-model's
+ * happens before relation. This is checked via the ClockVector constructs.
+ * @return true if this action's thread has synchronized with act's thread
+ * since the execution of act, false otherwise.
+ */
+bool ModelAction::happens_before(const ModelAction *act) const
+{
+ return act->cv->synchronized_since(this);
+}
+
+/** @brief Print nicely-formatted info about this ModelAction */
+void ModelAction::print() const
+{
+ const char *type_str, *mo_str;