From: Ben Pfaff <blp@gnu.org>
Date: Tue, 5 May 2009 05:20:42 +0000 (-0700)
Subject: model-checker: Add more progress functions.
X-Git-Tag: v0.7.3~92
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=72f4ef01cee853fd8e5bca96afad06397326ec76;p=pspp-builds.git

model-checker: Add more progress functions.

The model checker supports "progress functions" that report the current
status of the model checking run.  Until now the implementation only
exported a single progress function that printed a line of dots across
stderr.  This commit moves the "fancy" progress function that was
previously part of the PSPP language code into the model checker itself
and adds an even more verbose progress function as well.
---

diff --git a/src/language/tests/check-model.q b/src/language/tests/check-model.q
index 888557a9..f9ab6f2e 100644
--- a/src/language/tests/check-model.q
+++ b/src/language/tests/check-model.q
@@ -45,7 +45,7 @@
     stop=:states(n:max_unique_states,"%s>0"),
          :errors(n:max_errors),
          :timeout(d:time_limit,"%s>0");
-    progress=progress:none/dots/fancy;
+    progress=progress:none/dots/fancy/verbose;
     output=:verbosity(n:verbosity),
            :errverbosity(n:err_verbosity),
            :file(s:output_file).
@@ -97,22 +97,6 @@ check_model (struct lexer *lexer,
   return ok;
 }
 
-/* Fancy progress function for mc_options_set_progress_func. */
-static bool
-fancy_progress (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;
-}
-
 /* Parses options from LEXER and returns a corresponding
    mc_options, or a null pointer if parsing fails. */
 static struct mc_options *
@@ -193,11 +177,11 @@ parse_options (struct lexer *lexer)
       if (cmd.progress == CHM_NONE)
         mc_options_set_progress_usec (options, 0);
       else if (cmd.progress == CHM_DOTS)
-        {
-          /* Nothing to do: that's the default anyway. */
-        }
+        mc_options_set_progress_func (options, mc_progress_dots);
       else if (cmd.progress == CHM_FANCY)
-        mc_options_set_progress_func (options, fancy_progress);
+        mc_options_set_progress_func (options, mc_progress_fancy);
+      else if (cmd.progress == CHM_VERBOSE)
+        mc_options_set_progress_func (options, mc_progress_verbose);
     }
   if (cmd.output_file != NULL)
     {
diff --git a/src/libpspp/model-checker.c b/src/libpspp/model-checker.c
index 856e3f99..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;
 
diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h
index f7b3bd64..1e756119 100644
--- a/src/libpspp/model-checker.h
+++ b/src/libpspp/model-checker.h
@@ -1,5 +1,5 @@
 /* PSPP - a program for statistical analysis.
-   Copyright (C) 2007 Free Software Foundation, Inc.
+   Copyright (C) 2007, 2009 Free Software Foundation, Inc.
 
    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
@@ -418,6 +418,10 @@ FILE *mc_options_get_output_file (const struct mc_options *);
 void mc_options_set_output_file (struct mc_options *, FILE *);
 
 typedef bool mc_progress_func (struct mc *);
+mc_progress_func mc_progress_dots;
+mc_progress_func mc_progress_fancy;
+mc_progress_func mc_progress_verbose;
+
 int mc_options_get_progress_usec (const struct mc_options *);
 void mc_options_set_progress_usec (struct mc_options *, int progress_usec);
 mc_progress_func *mc_options_get_progress_func (const struct mc_options *);