From 86ca0bf04682b0011466ab49abda78acbf024c54 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 14 Nov 2012 16:46:03 -0800 Subject: [PATCH] model: routine to check if execution is complete Not used yet. --- model.cc | 15 +++++++++++++++ model.h | 1 + 2 files changed, 16 insertions(+) diff --git a/model.cc b/model.cc index e5c8a55..33fc4c3 100644 --- a/model.cc +++ b/model.cc @@ -294,6 +294,21 @@ bool ModelChecker::is_deadlocked() const return blocking_threads; } +/** + * Check if this is a complete execution. That is, have all thread completed + * execution (rather than exiting because sleep sets have forced a redundant + * execution). + * + * @return True if the execution is complete. + */ +bool ModelChecker::is_complete_execution() const +{ + for (unsigned int i = 0; i < get_num_threads(); i++) + if (is_enabled(int_to_id(i))) + return false; + return true; +} + /** * Queries the model-checker for more executions to explore and, if one * exists, resets the model-checker state to execute a new execution. diff --git a/model.h b/model.h index 85101fe..ee8026d 100644 --- a/model.h +++ b/model.h @@ -109,6 +109,7 @@ public: bool isfeasibleprefix(); void set_assert() {asserted=true;} bool is_deadlocked() const; + bool is_complete_execution() const; /** @brief Alert the model-checker that an incorrectly-ordered * synchronization was made */ -- 2.34.1