promise: add 'same_value' helper, force value-checking in CycleGraph
[model-checker.git] / promise.cc
index c695dc0ea21a4657cc04fd8601a28c77752f579b..c1f1c5c07782ffd74374d7f8cbe52613d2099fdc 100644 (file)
@@ -141,6 +141,16 @@ bool Promise::is_compatible_exclusive(const ModelAction *act) const
        return get_num_available_threads() == 1 && is_compatible(act);
 }
 
+/**
+ * @brief Check if a store's value matches this Promise
+ * @param write The store to check
+ * @return True if the store's written value matches this Promise
+ */
+bool Promise::same_value(const ModelAction *write) const
+{
+       return get_value() == write->get_write_value();
+}
+
 /**
  * @brief Check if a ModelAction's location matches this Promise
  * @param act The ModelAction to check