From: Brian Norris <banorris@uci.edu>
Date: Sat, 16 Feb 2013 02:09:03 +0000 (-0800)
Subject: model: end-of-execution print
X-Git-Tag: oopsla2013~245
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8d9a43be3bc794d7c9096dbda88640eb2fa99ee6;p=model-checker.git

model: end-of-execution print

For readability of a "verbose" execution log (and even for the shorter,
non-verbose log), it helps to visually separate the final statistics
from any previously-printed statistics. For instance, in the following
verbose snippet from the end of an execution history, it's confusing why
there are two identical copies of the statistics:

... <other execution history> ...
Number of complete, bug-free executions: 4
Number of redundant executions: 0
Number of buggy executions: 0
Number of infeasible executions: 5
Total executions: 9
Total nodes created: 48

Execution 9:
---------------------------------------------------------------------
... <snipped trace info> ...
---------------------------------------------------------------------

Number of complete, bug-free executions: 4
Number of redundant executions: 0
Number of buggy executions: 0
Number of infeasible executions: 5
Total executions: 9
Total nodes created: 48
---

diff --git a/model.cc b/model.cc
index 655c511..0bccd83 100644
--- a/model.cc
+++ b/model.cc
@@ -2807,5 +2807,6 @@ void ModelChecker::run()
 		};
 	} while (next_execution());
 
+	model_print("******* Model-checking complete: *******\n");
 	print_stats();
 }