/* 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
#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"
};
/* 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);
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)
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;
/* 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;
{
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;
}
{
if (results != NULL)
{
- moments1_destroy (results->depth_moments);
mc_path_destroy (&results->error_path);
free (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
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
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)
{
projects / pspp-builds.git / blobdiff