From: Brian Norris <banorris@uci.edu>
Date: Thu, 19 Apr 2012 18:00:55 +0000 (-0700)
Subject: model: flesh out check_current_action()
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=88e927cbc95771540c3ff7b905a84dbd8f37323c;p=cdsspec-compiler.git

model: flesh out check_current_action()

Relies on a stub set_backtracking() function.
---

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);