model/schedule: comput "reduadant" measurement, print along with traces

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 591d42a1ab3dbbc9aae2b8ea152e252c58379fd5..fa4dcc6fd3976281633317152bd4450d636fcc0c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -483,8 +483,10 @@ void ModelChecker::record_stats()
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;

-       else
+       else if (scheduler->all_threads_sleeping())

                stats.num_redundant++;
                stats.num_redundant++;

+       else
+               ASSERT(false);

 }
 
 /** @brief Print execution stats */
 }
 
 /** @brief Print execution stats */


@@ -2792,9 +2794,11 @@ void ModelChecker::print_summary() const
 #endif
 
        model_print("Execution %d:", stats.num_total);
 #endif
 
        model_print("Execution %d:", stats.num_total);

-       if (isfeasibleprefix())
+       if (isfeasibleprefix()) {
+               if (scheduler->all_threads_sleeping())
+                       model_print(" SLEEP-SET REDUNDANT");

                model_print("\n");
                model_print("\n");

-       else
+       } else

                print_infeasibility(" INFEASIBLE");
        print_list(action_trace);
        model_print("\n");
                print_infeasibility(" INFEASIBLE");
        print_list(action_trace);
        model_print("\n");