model: refactor end-of-execution output

[model-checker.git] / model.h

diff --git a/model.h b/model.h
index 86fa3e6ab901364c1b7f1df2214c568529fe238a..0d27d5a305d1830b75ac3519e294816f85bc88de 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 */
@@ -84,8 +87,7 @@ public:
        /** @returns the context for the main model-checking system thread */
        ucontext_t * get_system_context() { return &system_context; }
 
-       /** Prints an execution summary with trace information. */
-       void print_summary();
+       void print_summary() const;
 #if SUPPORT_MOD_ORDER_DUMP
        void dumpGraph(char *filename);
 #endif
@@ -250,6 +252,7 @@ private:
 
        bool have_bug_reports() const;
        void print_bugs() const;
+       void print_execution(bool printbugs) const;
 };
 
 extern ModelChecker *model;