support for locks... untested, but doesn't break quick run of a sample of test cases
[model-checker.git] / action.cc
index bf55d0091a2fdb368f5a2caf9727c3f2aab61d6f..f7ca249f965e6b351cd9763f382f9c792d586182 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -27,6 +27,22 @@ ModelAction::~ModelAction()
                delete cv;
 }
 
+bool ModelAction::is_mutex_op() const {
+       return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
+}
+
+bool ModelAction::is_lock() const {
+       return type == ATOMIC_LOCK;
+}
+
+bool ModelAction::is_unlock() const {
+       return type == ATOMIC_UNLOCK;
+}
+
+bool ModelAction::is_trylock() const {
+       return type == ATOMIC_TRYLOCK;
+}
+
 bool ModelAction::is_success_lock() const {
        return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
 }
@@ -175,6 +191,13 @@ void ModelAction::create_cv(const ModelAction *parent)
                cv = new ClockVector(NULL, this);
 }
 
+void ModelAction::set_try_lock(bool obtainedlock) {
+       if (obtainedlock)
+               value=VALUE_TRYSUCCESS;
+       else
+               value=VALUE_TRYFAILED;
+}
+
 /** Update the model action's read_from action */
 void ModelAction::read_from(const ModelAction *act)
 {