X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Flibpspp%2Fmodel-checker.c;h=856e3f99d8f052fe868d74897e83a78af86dd3e3;hb=ab75250c871e5947eed7e3454bdd806ba030e9fd;hp=1026aa9c9bafd6e1ccfdb1326ead297c64b79803;hpb=43b1296aafe7582e7dbe6c2b6a8b478d7d9b0fcf;p=pspp-builds.git

diff --git a/src/libpspp/model-checker.c b/src/libpspp/model-checker.c
index 1026aa9c..856e3f99 100644
--- a/src/libpspp/model-checker.c
+++ b/src/libpspp/model-checker.c
@@ -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
@@ -29,8 +29,8 @@
 #include <libpspp/bit-vector.h>
 #include <libpspp/compiler.h>
 #include <libpspp/deque.h>
+#include <libpspp/misc.h>
 #include <libpspp/str.h>
-#include <math/moments.h>
 
 #include "error.h"
 #include "minmax.h"
@@ -619,7 +619,8 @@ struct mc_results
 
     /* Depth statistics. */
     int max_depth_reached;              /* Max depth state examined. */
-    struct moments1 *depth_moments;     /* Enables reporting mean depth. */
+    unsigned long int depth_sum;        /* Sum of depths. */
+    int n_depths;                       /* Number of depths in depth_sum. */
 
     /* If error_count > 0, path to the last error reported. */
     struct mc_path error_path;
@@ -645,7 +646,6 @@ mc_results_create (void)
 {
   struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
   results->stop_reason = MC_CONTINUING;
-  results->depth_moments = moments1_create (MOMENT_MEAN);
   gettimeofday (&results->start, NULL);
   return results;
 }
@@ -656,7 +656,6 @@ mc_results_destroy (struct mc_results *results)
 {
   if (results != NULL)
     {
-      moments1_destroy (results->depth_moments);
       mc_path_destroy (&results->error_path);
       free (results);
     }
@@ -725,9 +724,9 @@ mc_results_get_max_depth_reached (const struct mc_results *results)
 double
 mc_results_get_mean_depth_reached (const struct mc_results *results)
 {
-  double mean;
-  moments1_calculate (results->depth_moments, NULL, &mean, NULL, NULL, NULL);
-  return mean != SYSMIS ? mean : 0.0;
+  return (results->n_depths == 0
+          ? 0
+          : (double) results->depth_sum / results->n_depths);
 }
 
 /* Returns the path traversed to obtain the last error
@@ -856,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));
+}
 
 /* An active model checking run. */
 struct mc
@@ -1199,7 +1240,8 @@ enqueue_state (struct mc *mc, struct mc_state *new)
 
   if (new->path.length > mc->results->max_depth_reached)
     mc->results->max_depth_reached = new->path.length;
-  moments1_add (mc->results->depth_moments, new->path.length, 1.0);
+  mc->results->depth_sum += new->path.length;
+  mc->results->n_depths++;
 
   if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
     {