+ }
+}
+
+/**
+ * Check if we are in a deadlock. Should only be called at the end of an
+ * execution, although it should not give false positives in the middle of an
+ * execution (there should be some ENABLED thread).
+ *
+ * @return True if program is in a deadlock; false otherwise
+ */
+bool ModelChecker::is_deadlocked() const
+{
+ bool blocking_threads = false;
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ thread_id_t tid = int_to_id(i);
+ if (is_enabled(tid))
+ return false;
+ Thread *t = get_thread(tid);
+ if (!t->is_model_thread() && t->get_pending())
+ blocking_threads = true;
+ }
+ 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;
+}
+
+/**
+ * @brief Assert a bug in the executing program.
+ *
+ * Use this function to assert any sort of bug in the user program. If the
+ * current trace is feasible (actually, a prefix of some feasible execution),
+ * then this execution will be aborted, printing the appropriate message. If
+ * the current trace is not yet feasible, the error message will be stashed and
+ * printed if the execution ever becomes feasible.
+ *
+ * This function can also be used to immediately trigger the bug; that is, we
+ * don't wait for a feasible execution before aborting. Only use the
+ * "immediate" option when you know that the infeasibility is justified (e.g.,
+ * pending release sequences are not a problem)
+ *
+ * @param msg Descriptive message for the bug (do not include newline char)
+ * @param user_thread Was this assertion triggered from a user thread?
+ * @param immediate Should this bug be triggered immediately?
+ */
+void ModelChecker::assert_bug(const char *msg, bool user_thread, bool immediate)
+{
+ priv->bugs.push_back(new bug_message(msg));
+
+ if (immediate || isfeasibleprefix()) {
+ set_assert();
+ if (user_thread)
+ switch_to_master(NULL);
+ }
+}
+
+/**
+ * @brief Assert a bug in the executing program, with a default message
+ * @see ModelChecker::assert_bug
+ * @param user_thread Was this assertion triggered from a user thread?
+ */
+void ModelChecker::assert_bug(bool user_thread)
+{
+ assert_bug("bug detected", user_thread);
+}
+
+/**
+ * @brief Assert a bug in the executing program immediately
+ * @see ModelChecker::assert_bug
+ * @param msg Descriptive message for the bug (do not include newline char)
+ */
+void ModelChecker::assert_bug_immediate(const char *msg)
+{
+ printf("Feasible: %s\n", isfeasibleprefix() ? "yes" : "no");
+ assert_bug(msg, false, true);
+}
+
+/** @return True, if any bugs have been reported for this execution */
+bool ModelChecker::have_bug_reports() const
+{
+ return priv->bugs.size() != 0;
+}
+
+/** @brief Print bug report listing for this execution (if any bugs exist) */
+void ModelChecker::print_bugs() const
+{
+ if (have_bug_reports()) {
+ printf("Bug report: %zu bugs detected\n", priv->bugs.size());
+ for (unsigned int i = 0; i < priv->bugs.size(); i++)
+ priv->bugs[i]->print();
+ }
+}
+
+/**
+ * @brief Record end-of-execution stats
+ *
+ * Must be run when exiting an execution. Records various stats.
+ * @see struct execution_stats
+ */
+void ModelChecker::record_stats()
+{
+ stats.num_total++;
+ if (!isfinalfeasible())
+ stats.num_infeasible++;
+ else if (have_bug_reports())
+ stats.num_buggy_executions++;
+ else if (is_complete_execution())
+ stats.num_complete++;
+}
+
+/** @brief Print execution stats */
+void ModelChecker::print_stats() const
+{
+ printf("Number of complete, bug-free executions: %d\n", stats.num_complete);
+ printf("Number of buggy executions: %d\n", stats.num_buggy_executions);
+ printf("Number of infeasible executions: %d\n", stats.num_infeasible);
+ printf("Total executions: %d\n", stats.num_total);
+ printf("Total nodes created: %d\n", node_stack->get_total_nodes());