if (prevfi) {
*fi = *prevfi;
}
- if (parent->is_enabled(int_to_id(i))) {
+ if (parent && parent->is_enabled(int_to_id(i))) {
fi->enabled_count++;
}
if (i == currtid) {
/** Prints debugging info for the ModelAction associated with this Node */
void Node::print()
{
- if (action)
+ if (action) {
action->print();
- else
+ model_print(" backtrack: %s\n", backtrack_empty() ? "empty" : "non-empty");
+ model_print(" future values: %s\n", future_value_empty() ? "empty" : "non-empty");
+ model_print(" read-from: %s\n", read_from_empty() ? "empty" : "non-empty");
+ model_print(" promises: %s\n", promise_empty() ? "empty" : "non-empty");
+ model_print(" misc: %s\n", misc_empty() ? "empty" : "non-empty");
+ model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
+ } else
model_print("******** empty action ********\n");
}
}
NodeStack::NodeStack() :
- node_list(1, new Node()),
- head_idx(0),
+ node_list(),
+ head_idx(-1),
total_nodes(0)
{
total_nodes++;
{
DBG();
- ASSERT(!node_list.empty());
-
if ((head_idx + 1) < (int)node_list.size()) {
head_idx++;
return node_list[head_idx]->get_action();
}
/* Record action */
- get_head()->explore_child(act, is_enabled);
+ Node *head = get_head();
Node *prevfairness = NULL;
- 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, get_head(), model->get_num_threads(), prevfairness));
+ if (head) {
+ head->explore_child(act, is_enabled);
+ 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));
total_nodes++;
head_idx++;
return NULL;
Node * NodeStack::get_head() const
{
- if (node_list.empty())
+ if (node_list.empty() || head_idx < 0)
return NULL;
return node_list[head_idx];
}
void NodeStack::reset_execution()
{
- head_idx = 0;
+ head_idx = -1;
}