From: Brian Norris <banorris@uci.edu>
Date: Tue, 18 Sep 2012 19:00:30 +0000 (-0700)
Subject: model: add infeasibility debugging
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=3864415594472a6a9b2b09bb0e0f846f056b7a47

model: add infeasibility debugging
---

diff --git a/model.cc b/model.cc
index 954c07dd..38c5d4a9 100644
--- a/model.cc
+++ b/model.cc
@@ -500,11 +500,24 @@ bool ModelChecker::isfeasible() {
 /** @returns whether the current partial trace is feasible other than
  * multiple RMW reading from the same store. */
 bool ModelChecker::isfeasibleotherthanRMW() {
+	if (DBG_ENABLED()) {
+		if (mo_graph->checkForCycles())
+			DEBUG("Infeasible: modification order cycles\n");
+		if (failed_promise)
+			DEBUG("Infeasible: failed promise\n");
+		if (too_many_reads)
+			DEBUG("Infeasible: too many reads\n");
+		if (promises_expired())
+			DEBUG("Infeasible: promises expired\n");
+	}
 	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
 bool ModelChecker::isfinalfeasible() {
+	if (DBG_ENABLED() && promises->size() != 0)
+		DEBUG("Infeasible: unrevolved promises\n");
+
 	return isfeasible() && promises->size() == 0;
 }