projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Merge branch 'master' of /home/git/model-checker
[model-checker.git]
/
nodestack.cc
diff --git
a/nodestack.cc
b/nodestack.cc
index 28bba4d003176c405f0ed65720639052aa6c3929..a73765320dac47e97428390fe37bc3b06ba10483 100644
(file)
--- a/
nodestack.cc
+++ b/
nodestack.cc
@@
-4,6
+4,7
@@
#include "action.h"
#include "common.h"
#include "model.h"
#include "action.h"
#include "common.h"
#include "model.h"
+#include "threads.h"
/**
* @brief Node constructor
/**
* @brief Node constructor
@@
-273,6
+274,11
@@
bool Node::is_enabled(thread_id_t tid)
return thread_id < num_threads && enabled_array[thread_id];
}
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
/**
* Add an action to the may_read_from set.
* @param act is the action to add
@@
-325,9
+331,9
@@
const ModelAction * Node::get_read_from() {
bool Node::increment_read_from() {
DBG();
promises.clear();
bool Node::increment_read_from() {
DBG();
promises.clear();
- if (
(read_from_index+1)
< may_read_from.size()) {
+ if (
read_from_index
< may_read_from.size()) {
read_from_index++;
read_from_index++;
- return
true
;
+ return
read_from_index < may_read_from.size()
;
}
return false;
}
}
return false;
}
@@
-339,9
+345,9
@@
bool Node::increment_read_from() {
bool Node::increment_future_value() {
DBG();
promises.clear();
bool Node::increment_future_value() {
DBG();
promises.clear();
- if (
(future_index+1)
< ((int)future_values.size())) {
+ if (
future_index
< ((int)future_values.size())) {
future_index++;
future_index++;
- return
true
;
+ return
(future_index < ((int)future_values.size()))
;
}
return false;
}
}
return false;
}
@@
-418,6
+424,8
@@
void NodeStack::pop_restofstack(int numAhead)
{
/* Diverging from previous execution; clear out remainder of list */
unsigned int it=iter+numAhead;
{
/* Diverging from previous execution; clear out remainder of list */
unsigned int it=iter+numAhead;
+ for(unsigned int i=it;i<node_list.size();i++)
+ delete node_list[i];
node_list.resize(it);
}
node_list.resize(it);
}