X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=4de6f354bfbccfbedc9061538ecb48be8e69e3e2;hb=bee1e27429b9a66e414eb83cf14e2089dd40a79e;hp=1007e762ee5258305bbd8ef5b403db5a874f17cc;hpb=c1db87fb3d52c93feb22496fe1e8513e35320c3d;p=model-checker.git

diff --git a/action.cc b/action.cc
index 1007e76..4de6f35 100644
--- a/action.cc
+++ b/action.cc
@@ -1,7 +1,6 @@
 #include <stdio.h>
 #define __STDC_FORMAT_MACROS
 #include <inttypes.h>
-#include <vector>
 
 #include "model.h"
 #include "action.h"
@@ -151,6 +150,11 @@ bool ModelAction::could_be_write() const
 	return is_write() || is_rmwr();
 }
 
+bool ModelAction::is_yield() const
+{
+	return type == THREAD_YIELD;
+}
+
 bool ModelAction::is_rmwr() const
 {
 	return type == ATOMIC_RMWR;
@@ -651,3 +655,17 @@ bool ModelAction::may_read_from(const Promise *promise) const
 			return true;
 	return false;
 }
+
+/**
+ * Only valid for LOCK, TRY_LOCK, UNLOCK, and WAIT operations.
+ * @return The mutex operated on by this action, if any; otherwise NULL
+ */
+std::mutex * ModelAction::get_mutex() const
+{
+	if (is_trylock() || is_lock() || is_unlock())
+		return (std::mutex *)get_location();
+	else if (is_wait())
+		return (std::mutex *)get_value();
+	else
+		return NULL;
+}