X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Flibpspp%2Fmodel-checker.c;h=6068713c812b923dece90fb47cf9b8e6838223f5;hb=72f4ef01cee853fd8e5bca96afad06397326ec76;hp=1f83266a9133aac52333d574160e612edf128ee8;hpb=3db80dc65b18355b719e8d56032400c753aa4eb7;p=pspp-builds.git

diff --git a/src/libpspp/model-checker.c b/src/libpspp/model-checker.c
index 1f83266a..6068713c 100644
--- a/src/libpspp/model-checker.c
+++ b/src/libpspp/model-checker.c
@@ -161,8 +161,8 @@ struct mc_options
   };
 
 /* Default progress function. */
-static bool
-default_progress (struct mc *mc)
+bool
+mc_progress_dots (struct mc *mc)
 {
   if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
     putc ('.', stderr);
@@ -171,6 +171,39 @@ default_progress (struct mc *mc)
   return true;
 }
 
+/* Progress function that prints a one-line summary of the
+   current state on stderr. */
+bool
+mc_progress_fancy (struct mc *mc)
+{
+  const struct mc_results *results = mc_get_results (mc);
+  if (mc_results_get_stop_reason (results) == MC_CONTINUING)
+    fprintf (stderr, "Processed %d unique states, max depth %d, "
+             "dropped %d duplicates...\r",
+             mc_results_get_unique_state_count (results),
+             mc_results_get_max_depth_reached (results),
+             mc_results_get_duplicate_dropped_states (results));
+  else
+    putc ('\n', stderr);
+  return true;
+}
+
+/* Progress function that displays a detailed summary of the
+   current state on stderr. */
+bool
+mc_progress_verbose (struct mc *mc)
+{
+  const struct mc_results *results = mc_get_results (mc);
+
+  /* VT100 clear screen and home cursor. */
+  fprintf (stderr, "\033[H\033[2J");
+
+  if (mc_results_get_stop_reason (results) == MC_CONTINUING)
+    mc_results_print (results, stderr);
+
+  return true;
+}
+
 /* Do-nothing progress function. */
 static bool
 null_progress (struct mc *mc UNUSED)
@@ -202,7 +235,7 @@ mc_options_create (void)
   options->failure_verbosity = 2;
   options->output_file = stdout;
   options->progress_usec = 250000;
-  options->progress_func = default_progress;
+  options->progress_func = mc_progress_dots;
 
   options->aux = NULL;
 
@@ -855,6 +888,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));
+}
 
 /* An active model checking run. */
 struct mc