From: Ben Pfaff Date: Tue, 5 May 2009 05:33:48 +0000 (-0700) Subject: model-checker: Move summary printing function into model checker. X-Git-Tag: v0.7.3~93 X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pspp-builds.git;a=commitdiff_plain;h=ab75250c871e5947eed7e3454bdd806ba030e9fd model-checker: Move summary printing function into model checker. There is no reason that the model checker itself should not be able to print a summary of its results. Until now, this code was buried in the PSPP language code, but the model checker itself is a better place for it. --- diff --git a/src/language/tests/check-model.q b/src/language/tests/check-model.q index 2f7b34df..888557a9 100644 --- a/src/language/tests/check-model.q +++ b/src/language/tests/check-model.q @@ -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) { @@ -220,52 +219,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 diff --git a/src/libpspp/model-checker.c b/src/libpspp/model-checker.c index 1f83266a..856e3f99 100644 --- a/src/libpspp/model-checker.c +++ b/src/libpspp/model-checker.c @@ -855,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 diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h index 8c86fae6..f7b3bd64 100644 --- a/src/libpspp/model-checker.h +++ b/src/libpspp/model-checker.h @@ -460,4 +460,6 @@ struct timeval mc_results_get_start (const struct mc_results *); struct timeval mc_results_get_end (const struct mc_results *); double mc_results_get_duration (const struct mc_results *); +void mc_results_print (const struct mc_results *, FILE *); + #endif /* libpspp/model-checker.h */