From def20b2249cf6902b4170965cd30a8e27ecc24f1 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 11 Sep 2012 10:19:46 -0700
Subject: [PATCH] model: add too_many_reads flag

---
 model.cc | 4 +++-
 model.h  | 1 +
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/model.cc b/model.cc
index c8af6cc..c77d4e1 100644
--- a/model.cc
+++ b/model.cc
@@ -33,6 +33,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	node_stack(new NodeStack()),
 	mo_graph(new CycleGraph()),
 	failed_promise(false),
+	too_many_reads(false),
 	asserted(false)
 {
 	/* Allocate this "size" on the snapshotting heap */
@@ -75,6 +76,7 @@ void ModelChecker::reset_to_initial_state()
 	DEBUG("+++ Resetting to initial state +++\n");
 	node_stack->reset_execution();
 	failed_promise = false;
+	too_many_reads = false;
 	reset_asserted();
 	snapshotObject->backTrackBeforeStep(0);
 }
@@ -380,7 +382,7 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
-	return !mo_graph->checkForCycles() && !failed_promise;
+	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads;
 }
 
 /** Returns whether the current completed trace is feasible. */
diff --git a/model.h b/model.h
index 990f559..5d34b4a 100644
--- a/model.h
+++ b/model.h
@@ -177,6 +177,7 @@ private:
 	 */
 	CycleGraph *mo_graph;
 	bool failed_promise;
+	bool too_many_reads;
 	bool asserted;
 };
 
-- 
2.34.1