X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Flanguage%2Ftests%2Fcheck-model.q;h=f9ab6f2e4c0d127356f2bf7fc7fa5bbd06d078a2;hb=69dadb9ec8ffda14e4e1758b4cd32b210bd24649;hp=b1f44ffa6bef06ad0a3e6c927281e6762c6f02c0;hpb=9a331fe64eb814ae5c1322e21717a04fb254bf65;p=pspp-builds.git

diff --git a/src/language/tests/check-model.q b/src/language/tests/check-model.q
index b1f44ffa..f9ab6f2e 100644
--- a/src/language/tests/check-model.q
+++ b/src/language/tests/check-model.q
@@ -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
@@ -21,8 +21,8 @@
 
 #include <errno.h>
 
-#include <language/tests/model-checker.h>
 #include <language/lexer/lexer.h>
+#include <libpspp/model-checker.h>
 
 #include "error.h"
 #include "fwriteerror.h"
@@ -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).
@@ -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)
     {
@@ -98,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 *
@@ -194,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)
     {
@@ -220,52 +203,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