model/main: disable most printing by default, add verbosity

Adds a '-v' parameter for printing verbose info on a non-DEBUG build.
This effectively creates 3 classes of runs:

 - Default build, no -v: only prints info when discovering a buggy
   execution
 - Default build, -v: prints more verbose information, on all feasible
   executions (buggy or non-buggy)
 - Debug build: Built with 'make debug'. Most verbose; prints everything
   for every execution, including infeasible executions. Also prints
   DEBUG() prints (as usual).

diff --git a/main.cc b/main.cc
index f79366fb2d8450bcbbe69373ac45db600aec8caa..f6ab259a64bb1ddfe85ec092518fdb091f23849a 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -23,6 +23,7 @@ static void param_defaults(struct model_params * params) {
        params->bound = 0;
        params->maxfuturevalues = 0;
        params->expireslop = 10;
+       params->verbose = 0;
 }
 
 static void print_usage(struct model_params *params) {
@@ -47,13 +48,14 @@ static void print_usage(struct model_params *params) {
 "                      priority for execution. Default: %d\n"
 "-e                    Enabled count. Default: %d\n"
 "-b                    Upper length bound. Default: %d\n"
+"-v                    Print verbose execution information.\n"
 "--                    Program arguments follow.\n\n",
 params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->enabledcount, params->bound);
        exit(EXIT_SUCCESS);
 }
 
 static void parse_options(struct model_params *params, int *argc, char ***argv) {
-       const char *shortopts = "hm:M:s:S:f:e:b:";
+       const char *shortopts = "hm:M:s:S:f:e:b:v";
        int opt;
        bool error = false;
        while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) {
@@ -82,6 +84,9 @@ static void parse_options(struct model_params *params, int *argc, char ***argv)
                case 'M':
                        params->maxfuturevalues = atoi(optarg);
                        break;
+               case 'v':
+                       params->verbose = 1;
+                       break;
                default: /* '?' */
                        error = true;
                        break;

diff --git a/model.cc b/model.cc
index 9ed6d423452a52e5c4ee006fa624fad809bdebc3..199a8fc3505f7273a8cab4dedcbb64db693d96cf 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -425,24 +425,39 @@ bool ModelChecker::next_execution()
        DBG();
 
        if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
-               model_print("Earliest divergence point since last feasible execution:\n");
-               if (earliest_diverge)
-                       earliest_diverge->print();
-               else
-                       model_print("(Not set)\n");
-
-               earliest_diverge = NULL;
-
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
                checkDataRaces();
-               print_bugs();
-               model_print("\n");
-               print_summary();
+
+               if (DBG_ENABLED() || params.verbose || have_bug_reports()) {
+                       print_program_output();
+
+                       if (DBG_ENABLED() || params.verbose) {
+                               model_print("Earliest divergence point since last feasible execution:\n");
+                               if (earliest_diverge)
+                                       earliest_diverge->print();
+                               else
+                                       model_print("(Not set)\n");
+
+                               model_print("\n");
+                               print_stats();
+                       }
+
+                       print_bugs();
+                       model_print("\n");
+                       print_summary();
+               } else
+                       clear_program_output();
+
+               earliest_diverge = NULL;
        } else if (DBG_ENABLED()) {
+               print_program_output();
                model_print("\n");
+               print_stats();
                print_summary();
+       } else {
+               clear_program_output();
        }
 
        record_stats();

diff --git a/model.h b/model.h
index 86fa3e6ab901364c1b7f1df2214c568529fe238a..bbad36e40ae727a93fe0e8e927aeb0ebe4b91da5 100644 (file)
--- a/model.h
+++ b/model.h
@@ -47,6 +47,9 @@ struct model_params {
         *  expiration time exceeds the existing one by more than the slop
         *  value */
        unsigned int expireslop;
+
+       /** @brief Verbosity (0 = quiet; 1 = noisy) */
+       int verbose;
 };
 
 /** @brief Model checker execution stats */