1 /* PSPP - computes sample statistics.
2 Copyright (C) 2007 Free Software Foundation, Inc.
4 This program is free software; you can redistribute it and/or
5 modify it under the terms of the GNU General Public License as
6 published by the Free Software Foundation; either version 2 of the
7 License, or (at your option) any later version.
9 This program is distributed in the hope that it will be useful, but
10 WITHOUT ANY WARRANTY; without even the implied warranty of
11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
12 General Public License for more details.
14 You should have received a copy of the GNU General Public License
15 along with this program; if not, write to the Free Software
16 Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
21 #include <language/tests/check-model.h>
25 #include <libpspp/model-checker.h>
26 #include <language/lexer/lexer.h>
29 #include "fwriteerror.h"
32 #define _(msgid) gettext (msgid)
33 #define N_(msgid) msgid
39 search=strategy:broad/deep/random,
43 queue=:limit(n:queue_limit,"%s>0"),
44 drop:newest/oldest/random;
46 stop=:states(n:max_unique_states,"%s>0"),
47 :errors(n:max_errors),
48 :timeout(d:time_limit,"%s>0");
49 progress=progress:none/dots/fancy;
50 output=:verbosity(n:verbosity),
51 :errverbosity(n:err_verbosity),
57 static struct mc_options *parse_options (struct lexer *);
58 static void print_results (const struct mc_results *, FILE *);
60 /* Parses a syntax description of model checker options from
61 LEXER and passes them, along with AUX, to the CHECKER
62 function, which must wrap a call to mc_run and return the
63 mc_results that it returned. This function then prints a
64 description of the mc_results to the output file. Returns
65 true if the model checker run found no errors, false
68 check_model (struct lexer *lexer,
69 struct mc_results *(*checker) (struct mc_options *, void *aux),
72 struct mc_options *options;
73 struct mc_results *results;
77 options = parse_options (lexer);
80 output_file = mc_options_get_output_file (options);
82 results = checker (options, aux);
84 print_results (results, output_file);
86 if (output_file != stdout && output_file != stderr)
88 if (fwriteerror (output_file) < 0)
90 /* We've already discarded the name of the output file.
92 error (0, errno, "error closing output file");
96 ok = mc_results_get_error_count (results) == 0;
97 mc_results_destroy (results);
102 /* Fancy progress function for mc_options_set_progress_func. */
104 fancy_progress (struct mc *mc)
106 const struct mc_results *results = mc_get_results (mc);
107 if (mc_results_get_stop_reason (results) == MC_CONTINUING)
108 fprintf (stderr, "Processed %d unique states, max depth %d, "
109 "dropped %d duplicates...\r",
110 mc_results_get_unique_state_count (results),
111 mc_results_get_max_depth_reached (results),
112 mc_results_get_duplicate_dropped_states (results));
118 /* Parses options from LEXER and returns a corresponding
119 mc_options, or a null pointer if parsing fails. */
120 static struct mc_options *
121 parse_options (struct lexer *lexer)
123 struct cmd_check_model cmd;
124 struct mc_options *options;
126 if (!parse_check_model (lexer, NULL, &cmd, NULL))
129 options = mc_options_create ();
130 if (cmd.strategy != -1)
131 mc_options_set_strategy (options,
132 cmd.strategy == CHM_BROAD ? MC_BROAD
133 : cmd.strategy == CHM_DEEP ? MC_DEEP
134 : cmd.strategy == CHM_RANDOM ? MC_RANDOM
136 if (cmd.sbc_path > 0)
138 if (cmd.sbc_search > 0)
139 msg (SW, _("PATH and SEARCH subcommands are mutually exclusive. "
143 struct subc_list_int *list = &cmd.il_path[0];
144 int count = subc_list_int_count (list);
150 mc_path_init (&path);
151 for (i = 0; i < count; i++)
152 mc_path_push (&path, subc_list_int_at (list, i));
153 mc_options_set_follow_path (options, &path);
154 mc_path_destroy (&path);
157 msg (SW, _("At least one value must be specified on PATH."));
160 if (cmd.max_depth != NOT_LONG)
161 mc_options_set_max_depth (options, cmd.max_depth);
162 if (cmd.hash_bits != NOT_LONG)
165 mc_options_set_hash_bits (options, cmd.hash_bits);
166 hash_bits = mc_options_get_hash_bits (options);
167 if (hash_bits != cmd.hash_bits)
168 msg (SW, _("Hash bits adjusted to %d."), hash_bits);
170 if (cmd.queue_limit != NOT_LONG)
171 mc_options_set_queue_limit (options, cmd.queue_limit);
174 enum mc_queue_limit_strategy drop
175 = (cmd.drop == CHM_NEWEST ? MC_DROP_NEWEST
176 : cmd.drop == CHM_OLDEST ? MC_DROP_OLDEST
177 : cmd.drop == CHM_RANDOM ? MC_DROP_RANDOM
179 mc_options_set_queue_limit_strategy (options, drop);
181 if (cmd.sbc_search > 0)
182 mc_options_set_seed (options, cmd.n_seed[0]);
183 if (cmd.max_unique_states != NOT_LONG)
184 mc_options_set_max_unique_states (options, cmd.max_unique_states);
185 if (cmd.max_errors != NOT_LONG)
186 mc_options_set_max_errors (options, cmd.max_errors);
187 if (cmd.time_limit != SYSMIS)
188 mc_options_set_time_limit (options, cmd.time_limit);
189 if (cmd.verbosity != NOT_LONG)
190 mc_options_set_verbosity (options, cmd.verbosity);
191 if (cmd.err_verbosity != NOT_LONG)
192 mc_options_set_failure_verbosity (options, cmd.err_verbosity);
193 if (cmd.progress != -1)
195 if (cmd.progress == CHM_NONE)
196 mc_options_set_progress_usec (options, 0);
197 else if (cmd.progress == CHM_DOTS)
199 /* Nothing to do: that's the default anyway. */
201 else if (cmd.progress == CHM_FANCY)
202 mc_options_set_progress_func (options, fancy_progress);
204 if (cmd.output_file != NULL)
206 FILE *output_file = fopen (cmd.output_file, "w");
207 if (output_file == NULL)
209 error (0, errno, _("error opening \"%s\" for writing"),
211 free_check_model (&cmd);
212 mc_options_destroy (options);
215 mc_options_set_output_file (options, output_file);
221 /* Prints a description of RESULTS to stream F. */
223 print_results (const struct mc_results *results, FILE *f)
225 enum mc_stop_reason reason = mc_results_get_stop_reason (results);
228 "MODEL CHECKING SUMMARY\n"
229 "----------------------\n\n", f);
231 fprintf (f, "Stopped by: %s\n",
232 reason == MC_SUCCESS ? "state space exhaustion"
233 : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
234 : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
235 : reason == MC_END_OF_PATH ? "reached end of specified path"
236 : reason == MC_TIMEOUT ? "reaching time limit"
237 : reason == MC_INTERRUPTED ? "user interruption"
239 fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
241 fprintf (f, "Unique states checked: %d\n",
242 mc_results_get_unique_state_count (results));
243 fprintf (f, "Maximum depth reached: %d\n",
244 mc_results_get_max_depth_reached (results));
245 fprintf (f, "Mean depth reached: %.2f\n\n",
246 mc_results_get_mean_depth_reached (results));
248 fprintf (f, "Dropped duplicate states: %d\n",
249 mc_results_get_duplicate_dropped_states (results));
250 fprintf (f, "Dropped off-path states: %d\n",
251 mc_results_get_off_path_dropped_states (results));
252 fprintf (f, "Dropped too-deep states: %d\n",
253 mc_results_get_depth_dropped_states (results));
254 fprintf (f, "Dropped queue-overflow states: %d\n",
255 mc_results_get_queue_dropped_states (results));
256 fprintf (f, "Checked states still queued when stopped: %d\n",
257 mc_results_get_queued_unprocessed_states (results));
258 fprintf (f, "Maximum queue length reached: %d\n\n",
259 mc_results_get_max_queue_length (results));
261 fprintf (f, "Runtime: %.2f seconds\n",
262 mc_results_get_duration (results));