From 88e927cbc95771540c3ff7b905a84dbd8f37323c Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 19 Apr 2012 11:00:55 -0700 Subject: [PATCH] model: flesh out check_current_action() Relies on a stub set_backtracking() function. --- model.cc | 12 +++++++++--- model.h | 1 + 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/model.cc b/model.cc index 88f6b33..67222e9 100644 --- a/model.cc +++ b/model.cc @@ -37,10 +37,16 @@ void ModelChecker::add_system_thread(Thread *t) void ModelChecker::check_current_action(void) { - if (this->current_action) - this->action_trace.push_back(this->current_action); - else + ModelAction *next = this->current_action; + + if (!next) { DEBUG("trying to push NULL action...\n"); + return; + } + next->set_node(currentNode); + set_backtracking(next); + currentNode = currentNode->exploreChild(next->get_tid()); + this->action_trace.push_back(next); } void ModelChecker::print_trace(void) diff --git a/model.h b/model.h index 2762e10..b6a0004 100644 --- a/model.h +++ b/model.h @@ -52,6 +52,7 @@ public: void set_current_action(ModelAction *act) { current_action = act; } void check_current_action(void); + void set_backtracking(ModelAction *act); void print_trace(void); int add_thread(Thread *t); -- 2.34.1