From: Brian Norris <banorris@uci.edu>
Date: Tue, 20 Nov 2012 04:29:34 +0000 (-0800)
Subject: model: replace isfinalfeasible() with stronger check
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=9fb0b534cd05f395ab508a30624997e43ef0cfc9

model: replace isfinalfeasible() with stronger check

The stronger isfeasibleprefix() check is not strictly necessary in these
cases, since we can ensure that promises are resolved before executing
these, but it make sense to have a well-defined "strength" to these
feasibility properties, then use the strongest strength that is useful.
---

diff --git a/model.cc b/model.cc
index 8453f2e5..d829582e 100644
--- a/model.cc
+++ b/model.cc
@@ -424,7 +424,7 @@ void ModelChecker::print_bugs() const
 void ModelChecker::record_stats()
 {
 	stats.num_total++;
-	if (!isfinalfeasible())
+	if (!isfeasibleprefix())
 		stats.num_infeasible++;
 	else if (have_bug_reports())
 		stats.num_buggy_executions++;
@@ -483,7 +483,7 @@ bool ModelChecker::next_execution()
 {
 	DBG();
 	/* Is this execution a feasible execution that's worth bug-checking? */
-	bool complete = isfinalfeasible() && (is_complete_execution() ||
+	bool complete = isfeasibleprefix() && (is_complete_execution() ||
 			have_bug_reports());
 
 	/* End-of-execution bug checks */
@@ -1210,8 +1210,11 @@ bool ModelChecker::promises_expired() const
 	return false;
 }
 
-/** @return whether the current partial trace must be a prefix of a
- * feasible trace. */
+/**
+ * This is the strongest feasibility check available.
+ * @return whether the current trace (partial or complete) must be a prefix of
+ * a feasible trace.
+ * */
 bool ModelChecker::isfeasibleprefix() const
 {
 	return promises->size() == 0 && pending_rel_seqs->size() == 0 && !is_infeasible();
@@ -2358,7 +2361,7 @@ void ModelChecker::print_summary() const
 	dumpGraph(buffername);
 #endif
 
-	if (!isfinalfeasible())
+	if (!isfeasibleprefix())
 		model_print("INFEASIBLE EXECUTION!\n");
 	print_list(action_trace, stats.num_total);
 	model_print("\n");