From 5ceb41c1ae83da9e1d53e1a6c03c9c8f147543d5 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sun, 14 Apr 2013 23:24:44 -0700 Subject: [PATCH 1/1] model: add too_many_steps() --- model.cc | 8 +++++++- model.h | 1 + 2 files changed, 8 insertions(+), 1 deletion(-) 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; -- 2.34.1