X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=6b1d4ef9c86929fdd14d14172149abaacec96133;hb=f8990cc12e0a21702f9af0b017518fba0b279668;hp=c364df9f7613178e2453d05bd667f64f44ed4fde;hpb=22bc505e43e7215a70b2ae362e0b4bbd08c09ddb;p=model-checker.git diff --git a/nodestack.cc b/nodestack.cc index c364df9..6b1d4ef 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -4,6 +4,7 @@ #include "action.h" #include "common.h" #include "model.h" +#include "threads.h" /** * @brief Node constructor @@ -273,6 +274,11 @@ bool Node::is_enabled(thread_id_t tid) return thread_id < num_threads && enabled_array[thread_id]; } +bool Node::has_priority(thread_id_t tid) +{ + return fairness[id_to_int(tid)].priority; +} + /** * Add an action to the may_read_from set. * @param act is the action to add @@ -356,16 +362,18 @@ void Node::explore(thread_id_t tid) explored_children[i] = true; } -NodeStack::NodeStack() - : total_nodes(0) +NodeStack::NodeStack() : + node_list(1, new Node()), + iter(0), + total_nodes(0) { - node_list.push_back(new Node()); total_nodes++; - iter = 0; } NodeStack::~NodeStack() { + for (unsigned int i = 0; i < node_list.size(); i++) + delete node_list[i]; } void NodeStack::print() @@ -418,6 +426,8 @@ void NodeStack::pop_restofstack(int numAhead) { /* Diverging from previous execution; clear out remainder of list */ unsigned int it=iter+numAhead; + for(unsigned int i=it;i