-/** 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;
-}
-