-/* PSPP - computes sample statistics.
- Copyright (C) 2007 Free Software Foundation, Inc.
+/* PSPP - a program for statistical analysis.
+ 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 the Free Software Foundation; either version 2 of the
- License, or (at your option) any later version.
+ 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
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
- This program is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- General Public License for more details.
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
You should have received a copy of the GNU General Public License
- along with this program; if not, write to the Free Software
- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
- 02110-1301, USA. */
+ along with this program. If not, see <http://www.gnu.org/licenses/>. */
#include <config.h>
+#include <limits.h>
#include <language/tests/check-model.h>
#include <errno.h>
-#include <libpspp/model-checker.h>
#include <language/lexer/lexer.h>
+#include <libpspp/model-checker.h>
#include "error.h"
#include "fwriteerror.h"
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).
/* (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
results = checker (options, aux);
- print_results (results, output_file);
+ mc_results_print (results, output_file);
if (output_file != stdout && output_file != stderr)
{
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 *
msg (SW, _("At least one value must be specified on PATH."));
}
}
- if (cmd.max_depth != NOT_LONG)
+ if (cmd.max_depth != LONG_MIN)
mc_options_set_max_depth (options, cmd.max_depth);
- if (cmd.hash_bits != NOT_LONG)
+ if (cmd.hash_bits != LONG_MIN)
{
int hash_bits;
mc_options_set_hash_bits (options, cmd.hash_bits);
if (hash_bits != cmd.hash_bits)
msg (SW, _("Hash bits adjusted to %d."), hash_bits);
}
- if (cmd.queue_limit != NOT_LONG)
+ if (cmd.queue_limit != LONG_MIN)
mc_options_set_queue_limit (options, cmd.queue_limit);
if (cmd.drop != -1)
{
}
if (cmd.sbc_search > 0)
mc_options_set_seed (options, cmd.n_seed[0]);
- if (cmd.max_unique_states != NOT_LONG)
+ if (cmd.max_unique_states != LONG_MIN)
mc_options_set_max_unique_states (options, cmd.max_unique_states);
- if (cmd.max_errors != NOT_LONG)
+ if (cmd.max_errors != LONG_MIN)
mc_options_set_max_errors (options, cmd.max_errors);
if (cmd.time_limit != SYSMIS)
mc_options_set_time_limit (options, cmd.time_limit);
- if (cmd.verbosity != NOT_LONG)
+ if (cmd.verbosity != LONG_MIN)
mc_options_set_verbosity (options, cmd.verbosity);
- if (cmd.err_verbosity != NOT_LONG)
+ if (cmd.err_verbosity != LONG_MIN)
mc_options_set_failure_verbosity (options, cmd.err_verbosity);
if (cmd.progress != -1)
{
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)
{
mc_options_set_output_file (options, output_file);
}
- 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));
+ free_check_model (&cmd);
- 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);
+ return options;
}
/*
projects / pspp-builds.git / blobdiff