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.
}
}
-bool ModelChecker::promises_expired() {
+bool ModelChecker::promises_expired() const
+{
for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
Promise *promise = (*promises)[promise_index];
if (promise->get_expiration()<priv->used_sequence_numbers) {
/** @return whether the current partial trace must be a prefix of a
* feasible trace. */
-bool ModelChecker::isfeasibleprefix() {
+bool ModelChecker::isfeasibleprefix() const
+{
return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
}
/** @return whether the current partial trace is feasible. */
-bool ModelChecker::isfeasible() {
+bool ModelChecker::isfeasible() const
+{
if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
DEBUG("Infeasible: RMW violation\n");
/** @return whether the current partial trace is feasible other than
* multiple RMW reading from the same store. */
-bool ModelChecker::isfeasibleotherthanRMW() {
+bool ModelChecker::isfeasibleotherthanRMW() const
+{
if (DBG_ENABLED()) {
if (mo_graph->checkForCycles())
DEBUG("Infeasible: modification order cycles\n");
}
/** Returns whether the current completed trace is feasible. */
-bool ModelChecker::isfinalfeasible() {
+bool ModelChecker::isfinalfeasible() const
+{
if (DBG_ENABLED() && promises->size() != 0)
DEBUG("Infeasible: unrevolved promises\n");