add some comments

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 159dd705c8b567ae16600be6c278cf252772ce5d..02a4a6a29206b34b8b3b22308439807b1b7c1188 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -133,7 +133,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
        if (next == diverge) {
                Node *nextnode = next->get_node();
                /* Reached divergence point */
-               if (nextnode->increment_promises()) {
+               if (nextnode->increment_promise()) {
                        /* The next node will try to satisfy a different set of promises. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
@@ -141,7 +141,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
                        /* The next node will read from a different value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
-               } else if (nextnode->increment_future_values()) {
+               } else if (nextnode->increment_future_value()) {
                        /* The next node will try to read from a different future value. */
                        tid = next->get_tid();
                        node_stack->pop_restofstack(2);
@@ -354,19 +354,19 @@ void ModelChecker::check_current_action(void)
        Node *currnode = curr->get_node();
        Node *parnode = currnode->get_parent();
 
-       if (!parnode->backtrack_empty()||!currnode->readsfrom_empty()||!currnode->futurevalues_empty()||!currnode->promises_empty())
+       if (!parnode->backtrack_empty()||!currnode->read_from_empty()||!currnode->future_value_empty()||!currnode->promise_empty())
                if (!next_backtrack || *curr > *next_backtrack)
                        next_backtrack = curr;
        
        set_backtracking(curr);
 }
 
-/** @returns whether the current trace is feasible. */
+/** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
        return !cyclegraph->checkForCycles() && !failed_promise;
 }
 
-/** Returns whether the current trace is feasible. */
+/** Returns whether the current completed trace is feasible. */
 bool ModelChecker::isfinalfeasible() {
        return isfeasible() && promises->size()==0;
 }
@@ -532,7 +532,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) {
 }
 
 
-/** Resolve promises. */
+/** Resolve the given promises. */
 
 void ModelChecker::resolve_promises(ModelAction *write) {
        for(unsigned int i=0, promise_index=0;promise_index<promises->size(); i++) {
@@ -547,6 +547,9 @@ void ModelChecker::resolve_promises(ModelAction *write) {
        }
 }
 
+/** Compute the set of promises that could potentially be satisfied by
+ *  this action. */
+
 void ModelChecker::compute_promises(ModelAction *curr) {
        for(unsigned int i=0;i<promises->size();i++) {
                Promise * promise=(*promises)[i];