X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=a73765320dac47e97428390fe37bc3b06ba10483;hb=81ea453e58cbb85fddff3aa8919dfbc59c3140eb;hp=c364df9f7613178e2453d05bd667f64f44ed4fde;hpb=22bc505e43e7215a70b2ae362e0b4bbd08c09ddb;p=model-checker.git diff --git a/nodestack.cc b/nodestack.cc index c364df9..a737653 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 @@ -418,6 +424,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