From c7d1fa37dfd38155acd2137fbeb9b7e5703fb3dc Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 10 Aug 2012 12:21:12 -0700 Subject: [PATCH] model: reformat/refactor some code --- model.cc | 31 +++++++++++++++---------------- 1 file changed, 15 insertions(+), 16 deletions(-) diff --git a/model.cc b/model.cc index 4cbcd4f..c4ee253 100644 --- a/model.cc +++ b/model.cc @@ -475,25 +475,24 @@ void ModelChecker::w_modification_order(ModelAction * curr) { /* Include at most one act per-thread that "happens before" curr */ if (act->happens_before(curr)) { - if (act->is_read()) { + if (act->is_read()) cyclegraph->addEdge(curr, act->get_reads_from()); - } else + else cyclegraph->addEdge(curr, act); break; - } else { - if (act->is_read()&&!act->is_synchronizing(curr)&&!act->same_thread(curr)) { - /* We have an action that: - (1) did not happen before us - (2) is a read and we are a write - (3) cannot synchronize with us - (4) is in a different thread - => - that read could potentially read from our write. - */ - if (act->get_node()->add_future_value(curr->get_value())&& - (!next_backtrack || *act > * next_backtrack)) - next_backtrack = act; - } + } else if (act->is_read() && !act->is_synchronizing(curr) && + !act->same_thread(curr)) { + /* We have an action that: + (1) did not happen before us + (2) is a read and we are a write + (3) cannot synchronize with us + (4) is in a different thread + => + that read could potentially read from our write. + */ + if (act->get_node()->add_future_value(curr->get_value()) && + (!next_backtrack || *act > *next_backtrack)) + next_backtrack = act; } } } -- 2.34.1