X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=57058921d95726fb5c8f305b5316e34a80e6d39d;hb=ffc110b3aaa80564dbf85f3c6a9049efd40571f1;hp=44a6d9ad6948c116e3305bd955e204825f01bc96;hpb=a2176c7545c29b28598bb252718cf080a3463665;p=model-checker.git

diff --git a/action.cc b/action.cc
index 44a6d9a..5705892 100644
--- a/action.cc
+++ b/action.cc
@@ -76,7 +76,7 @@ bool ModelAction::is_relseq_fixup() const
 
 bool ModelAction::is_mutex_op() const
 {
-	return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
+	return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
 }
 
 bool ModelAction::is_lock() const
@@ -84,6 +84,18 @@ bool ModelAction::is_lock() const
 	return type == ATOMIC_LOCK;
 }
 
+bool ModelAction::is_wait() const {
+	return type == ATOMIC_WAIT;
+}
+
+bool ModelAction::is_notify() const {
+	return type==ATOMIC_NOTIFY_ONE || type==ATOMIC_NOTIFY_ALL;
+}
+
+bool ModelAction::is_notify_one() const {
+	return type==ATOMIC_NOTIFY_ONE;
+}
+
 bool ModelAction::is_unlock() const
 {
 	return type == ATOMIC_UNLOCK;
@@ -250,6 +262,10 @@ bool ModelAction::is_conflicting_lock(const ModelAction *act) const
 	if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS)
 		return true;
 
+	//Try to push a successful trylock past a wait
+	if (act->is_wait() && is_trylock() && value == VALUE_TRYSUCCESS)
+		return true;
+
 	return false;
 }