X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=b2ef73cac30108fab56745f89b0542a186fc6410;hb=82df62c2b0805848b87bb71df5b66a4a66f8e25d;hp=dd2dd855c658f7734b7024f76a973e2341ac522c;hpb=9f1ddeb2b2ba0bf52d14456c90b363daa2f09965;p=model-checker.git diff --git a/nodestack.cc b/nodestack.cc index dd2dd85..b2ef73c 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -164,7 +164,7 @@ bool Node::increment_promise() //sending our value to two rmws... not going to work..try next combination continue; } - promises[i] = (promises[i] & PROMISE_RMW) |PROMISE_FULFILLED; + promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_FULFILLED; while (i > 0) { i--; if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED) @@ -188,9 +188,9 @@ bool Node::promise_empty() const for (int i = promises.size() - 1; i >= 0; i--) { if (promises[i] == PROMISE_UNFULFILLED) return false; - if (!fulfilledrmw && ((promises[i]&PROMISE_MASK) == PROMISE_UNFULFILLED)) + if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED)) return false; - if (promises[i] == (PROMISE_FULFILLED|PROMISE_RMW)) + if (promises[i] == (PROMISE_FULFILLED | PROMISE_RMW)) fulfilledrmw = true; } return true; @@ -556,7 +556,11 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow) prevfairness = node_list[head_idx - model->params.fairwindow]; } - node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness)); + + int next_threads = model->get_num_threads(); + if (act->get_type() == THREAD_CREATE) + next_threads++; + node_list.push_back(new Node(act, head, next_threads, prevfairness)); total_nodes++; head_idx++; return NULL;