model: add too_many_reads flag

diff --git a/model.cc b/model.cc
index c8af6cc4f5bfb2d2c878e6aa035e2cf712d56e29..c77d4e17d4627213d2510774fe9c5d853b91257e 100644 (file)
--- 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 990f559cc5af67fd368d5355bb890fc975a2c13d..5d34b4aa3e2694bcfd725e4170131592b884eba0 100644 (file)
--- a/model.h
+++ b/model.h
@@ -177,6 +177,7 @@ private:
         */
        CycleGraph *mo_graph;
        bool failed_promise;
+       bool too_many_reads;
        bool asserted;
 };