#include "model.h"
#include "threads-model.h"
#include "modeltypes.h"
+#include "execution.h"
/**
* @brief Node constructor
/******************* end breaking release sequences ***************************/
+/**
+ * Increments some behavior's index, if a new behavior is available
+ * @return True if there is a new behavior available; otherwise false
+ */
+bool Node::increment_behaviors()
+{
+ /* satisfy a different misc_index values */
+ if (increment_misc())
+ return true;
+ /* satisfy a different set of promises */
+ if (increment_promise())
+ return true;
+ /* read from a different value */
+ if (increment_read_from())
+ return true;
+ /* resolve a release sequence differently */
+ if (increment_relseq_break())
+ return true;
+ return false;
+}
+
NodeStack::NodeStack() :
node_list(),
head_idx(-1),
delete node_list[i];
}
+/**
+ * @brief Register the model-checker object with this NodeStack
+ * @param exec The execution structure for the ModelChecker
+ */
+void NodeStack::register_engine(const ModelExecution *exec)
+{
+ this->execution = exec;
+}
+
void NodeStack::print() const
{
model_print("............................................\n");
prevfairness = node_list[head_idx - model->params.fairwindow];
}
- int next_threads = model->get_num_threads();
+ int next_threads = execution->get_num_threads();
if (act->get_type() == THREAD_CREATE)
next_threads++;
node_list.push_back(new Node(act, head, next_threads, prevfairness));