projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
84d49e8
)
promise: add is_compatible()
author
Brian Norris
<banorris@uci.edu>
Fri, 1 Feb 2013 23:07:56 +0000
(15:07 -0800)
committer
Brian Norris
<banorris@uci.edu>
Wed, 6 Feb 2013 21:44:38 +0000
(13:44 -0800)
promise.cc
patch
|
blob
|
history
promise.h
patch
|
blob
|
history
diff --git
a/promise.cc
b/promise.cc
index 2bd6637352195a41029b96f220d88b1bff809403..fdd45791f40657556f344c96b579ade87bc90736 100644
(file)
--- a/
promise.cc
+++ b/
promise.cc
@@
-76,3
+76,12
@@
bool Promise::has_failed() const
{
return num_available_threads == 0;
}
{
return num_available_threads == 0;
}
+
+/**
+ * @param write A store which could satisfy this Promise
+ * @return True if the store can satisfy this Promise; false otherwise
+ */
+bool Promise::is_compatible(const ModelAction *write) const
+{
+ return thread_is_available(write->get_tid());
+}
diff --git
a/promise.h
b/promise.h
index 8ff8c3e319bd5b2f4a4b758be51c8adb7a5dbeb6..8eec87bd4dbf7f32ec3ecdb95b4bf611f5559bf9 100644
(file)
--- a/
promise.h
+++ b/
promise.h
@@
-41,6
+41,7
@@
class Promise {
void set_write(const ModelAction *act) { write = act; }
const ModelAction * get_write() { return write; }
int get_num_available_threads() { return num_available_threads; }
void set_write(const ModelAction *act) { write = act; }
const ModelAction * get_write() { return write; }
int get_num_available_threads() { return num_available_threads; }
+ bool is_compatible(const ModelAction *write) const;
void print() const;
void print() const;