model-checker: Move summary printing function into model checker.

There is no reason that the model checker itself should not be able to
print a summary of its results.  Until now, this code was buried in the
PSPP language code, but the model checker itself is a better place for it.

diff --git a/src/language/tests/check-model.q b/src/language/tests/check-model.q
index 2f7b34df4b63821aea1ea331cb6ba637eafa10d2..888557a91e438b3a5a05a3d7db75ac7713cc5e18 100644 (file)
--- a/src/language/tests/check-model.q
+++ b/src/language/tests/check-model.q
@@ -54,7 +54,6 @@
 /* (functions) */
 
 static struct mc_options *parse_options (struct lexer *);
-static void print_results (const struct mc_results *, FILE *);
 
 /* Parses a syntax description of model checker options from
    LEXER and passes them, along with AUX, to the CHECKER
@@ -80,7 +79,7 @@ check_model (struct lexer *lexer,
 
   results = checker (options, aux);
 
-  print_results (results, output_file);
+  mc_results_print (results, output_file);
 
   if (output_file != stdout && output_file != stderr)
     {
@@ -220,52 +219,6 @@ parse_options (struct lexer *lexer)
   return options;
 }
 
-/* Prints a description of RESULTS to stream F. */
-static void
-print_results (const struct mc_results *results, FILE *f)
-{
-  enum mc_stop_reason reason = mc_results_get_stop_reason (results);
-
-  fputs ("\n"
-         "MODEL CHECKING SUMMARY\n"
-         "----------------------\n\n", f);
-
-  fprintf (f, "Stopped by: %s\n",
-           reason == MC_SUCCESS ? "state space exhaustion"
-           : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
-           : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
-           : reason == MC_END_OF_PATH ? "reached end of specified path"
-           : reason == MC_TIMEOUT ? "reaching time limit"
-           : reason == MC_INTERRUPTED ? "user interruption"
-           : "unknown reason");
-  fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
-
-  fprintf (f, "Unique states checked: %d\n",
-           mc_results_get_unique_state_count (results));
-  fprintf (f, "Maximum depth reached: %d\n",
-           mc_results_get_max_depth_reached (results));
-  fprintf (f, "Mean depth reached: %.2f\n\n",
-           mc_results_get_mean_depth_reached (results));
-
-  fprintf (f, "Dropped duplicate states: %d\n",
-           mc_results_get_duplicate_dropped_states (results));
-  fprintf (f, "Dropped off-path states: %d\n",
-           mc_results_get_off_path_dropped_states (results));
-  fprintf (f, "Dropped too-deep states: %d\n",
-           mc_results_get_depth_dropped_states (results));
-  fprintf (f, "Dropped queue-overflow states: %d\n",
-           mc_results_get_queue_dropped_states (results));
-  fprintf (f, "Checked states still queued when stopped: %d\n",
-           mc_results_get_queued_unprocessed_states (results));
-  fprintf (f, "Maximum queue length reached: %d\n\n",
-           mc_results_get_max_queue_length (results));
-
-  fprintf (f, "Runtime: %.2f seconds\n",
-           mc_results_get_duration (results));
-
-  putc ('\n', f);
-}
-
 /*
   Local Variables:
   mode: c

diff --git a/src/libpspp/model-checker.c b/src/libpspp/model-checker.c
index 1f83266a9133aac52333d574160e612edf128ee8..856e3f99d8f052fe868d74897e83a78af86dd3e3 100644 (file)
--- a/src/libpspp/model-checker.c
+++ b/src/libpspp/model-checker.c
@@ -855,6 +855,48 @@ mc_results_get_duration (const struct mc_results *results)
   assert (results->stop_reason != MC_CONTINUING);
   return timeval_subtract (results->end, results->start);
 }
+
+/* Prints a description of RESULTS to stream F. */
+void
+mc_results_print (const struct mc_results *results, FILE *f)
+{
+  enum mc_stop_reason reason = mc_results_get_stop_reason (results);
+
+  if (reason != MC_CONTINUING)
+    fprintf (f, "Stopped by: %s\n",
+             reason == MC_SUCCESS ? "state space exhaustion"
+             : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
+             : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
+             : reason == MC_END_OF_PATH ? "reached end of specified path"
+             : reason == MC_TIMEOUT ? "reaching time limit"
+             : reason == MC_INTERRUPTED ? "user interruption"
+             : "unknown reason");
+  fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
+
+  fprintf (f, "Unique states checked: %d\n",
+           mc_results_get_unique_state_count (results));
+  fprintf (f, "Maximum depth reached: %d\n",
+           mc_results_get_max_depth_reached (results));
+  fprintf (f, "Mean depth reached: %.2f\n\n",
+           mc_results_get_mean_depth_reached (results));
+
+  fprintf (f, "Dropped duplicate states: %d\n",
+           mc_results_get_duplicate_dropped_states (results));
+  fprintf (f, "Dropped off-path states: %d\n",
+           mc_results_get_off_path_dropped_states (results));
+  fprintf (f, "Dropped too-deep states: %d\n",
+           mc_results_get_depth_dropped_states (results));
+  fprintf (f, "Dropped queue-overflow states: %d\n",
+           mc_results_get_queue_dropped_states (results));
+  fprintf (f, "Checked states still queued when stopped: %d\n",
+           mc_results_get_queued_unprocessed_states (results));
+  fprintf (f, "Maximum queue length reached: %d\n",
+           mc_results_get_max_queue_length (results));
+
+  if (reason != MC_CONTINUING)
+    fprintf (f, "\nRuntime: %.2f seconds\n",
+             mc_results_get_duration (results));
+}
 \f
 /* An active model checking run. */
 struct mc

diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h
index 8c86fae61d3eb99f1a3956fbaebad6f0a15be0f5..f7b3bd64f5bc2ae2d9eabfc941047c27a040c40d 100644 (file)
--- a/src/libpspp/model-checker.h
+++ b/src/libpspp/model-checker.h
@@ -460,4 +460,6 @@ struct timeval mc_results_get_start (const struct mc_results *);
 struct timeval mc_results_get_end (const struct mc_results *);
 double mc_results_get_duration (const struct mc_results *);
 
+void mc_results_print (const struct mc_results *, FILE *);
+
 #endif /* libpspp/model-checker.h */