X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=fb2423f3dfe12a29090ae647194b8a2adbc5bfc6;hb=76205f5d9b62f73ea01f7e55765a043a8333a455;hp=50317d07daa539d8f6643f16c3892c89aaddf60e;hpb=59b62a130c9615c9ccd23c4354c7bc827d5eda3b;p=model-checker.git

diff --git a/model.cc b/model.cc
index 50317d0..fb2423f 100644
--- a/model.cc
+++ b/model.cc
@@ -259,7 +259,6 @@ ModelAction * ModelChecker::get_next_backtrack()
 	return next;
 }
 
-
 /**
  * Processes a read or rmw model action.
  * @param curr is the read model action to process.
@@ -267,7 +266,6 @@ ModelAction * ModelChecker::get_next_backtrack()
  * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
  * @return True if processing this read updates the mo_graph.
  */
-
 bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) {
 	uint64_t value;
 	bool updated=false;
@@ -428,7 +426,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 		add_action_to_lists(curr);
 
 	check_curr_backtracking(curr);
-	
+
 	set_backtracking(curr);
 
 	return get_next_thread(curr);
@@ -437,7 +435,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
-	
+
 	if ((!parnode->backtrack_empty() ||
 			 !currnode->read_from_empty() ||
 			 !currnode->future_value_empty() ||
@@ -448,7 +446,6 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
 	}
 }
 
-
 bool ModelChecker::promises_expired() {
 	for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
 		Promise *promise = (*promises)[promise_index];
@@ -762,7 +759,6 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
 	return true;
 }
 
-
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
  * The ModelAction under consideration is expected to be taking part in
@@ -1056,8 +1052,6 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 	return resolved;
 }
 
-
-
 /**
  * Compute the set of promises that could potentially be satisfied by this
  * action. Note that the set computation actually appears in the Node, not in