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=cb51c485df27ae983104b7540888c1b6492bb16d;hpb=a9acce47d67e0ab35ce1690e4f1b1ac0121c2d78;p=pspp-builds.git diff --git a/src/libpspp/model-checker.c b/src/libpspp/model-checker.c index cb51c485..6068713c 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 @@ -26,12 +26,11 @@ #include #include -#include #include #include #include +#include #include -#include #include "error.h" #include "minmax.h" @@ -162,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); @@ -172,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) @@ -203,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; @@ -620,7 +652,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; @@ -646,7 +679,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; } @@ -657,7 +689,6 @@ mc_results_destroy (struct mc_results *results) { if (results != NULL) { - moments1_destroy (results->depth_moments); mc_path_destroy (&results->error_path); free (results); } @@ -726,9 +757,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 @@ -857,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 @@ -1200,7 +1273,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) {