From: Brian Norris <banorris@uci.edu>
Date: Mon, 15 Apr 2013 06:24:44 +0000 (-0700)
Subject: model: add too_many_steps()
X-Git-Tag: oopsla2013~77^2~3
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=5ceb41c1ae83da9e1d53e1a6c03c9c8f147543d5

model: add too_many_steps()
---

diff --git a/model.cc b/model.cc
index 3be75b2..eed548c 100644
--- a/model.cc
+++ b/model.cc
@@ -3113,6 +3113,12 @@ void user_main_wrapper(void *)
 	user_main(model->params.argc, model->params.argv);
 }
 
+/** @return True if the execution has taken too many steps */
+bool ModelChecker::too_many_steps() const
+{
+	return params.bound != 0 && priv->used_sequence_numbers > params.bound;
+}
+
 bool ModelChecker::should_terminate_execution()
 {
 	/* Infeasible -> don't take any more steps */
@@ -3123,7 +3129,7 @@ bool ModelChecker::should_terminate_execution()
 		return true;
 	}
 
-	if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
+	if (too_many_steps())
 		return true;
 	return false;
 }
diff --git a/model.h b/model.h
index b5c7c30..fba6ecc 100644
--- a/model.h
+++ b/model.h
@@ -287,6 +287,7 @@ private:
 	bool is_feasible_prefix_ignore_relseq() const;
 	bool is_infeasible() const;
 	bool is_deadlocked() const;
+	bool too_many_steps() const;
 	bool is_complete_execution() const;
 	bool have_bug_reports() const;
 	void print_bugs() const;