+
+/** Checks whether making the ModelAction read read_from the
+ ModelAction write will introduce a cycle in the reads_from
+ relation.
+
+@return true if making it read from will be fine, false otherwise.
+
+*/
+
+bool ModelChecker::ensure_rmw_acyclic(const ModelAction * read, const ModelAction *write) {
+ if (!read->is_rmw())
+ return true;
+ if (!write->is_rmw())
+ return true;
+ while(write!=NULL) {
+ if (write==read) {
+ rmw_cycle=true;
+ return false;
+ }
+ write=write->get_reads_from();
+ }
+ return true;
+}
+