model: add infeasibility debugging

diff --git a/model.cc b/model.cc
index 954c07dd6dacdfc9473a4aa3f5e0a2f8db38bcbf..38c5d4a9396f82bde9b8341fac00f8b2d8dc63a6 100644 (file)
--- 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;
 }