1 /* PSPP - a program for statistical analysis.
2 Copyright (C) 2007, 2009 Free Software Foundation, Inc.
4 This program is free software: you can redistribute it and/or modify
5 it under the terms of the GNU General Public License as published by
6 the Free Software Foundation, either version 3 of the License, or
7 (at your option) any later version.
9 This program is distributed in the hope that it will be useful,
10 but WITHOUT ANY WARRANTY; without even the implied warranty of
11 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
12 GNU 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, see <http://www.gnu.org/licenses/>. */
20 #include <language/tests/check-model.h>
24 #include <language/lexer/lexer.h>
25 #include <libpspp/model-checker.h>
28 #include "fwriteerror.h"
31 #define _(msgid) gettext (msgid)
32 #define N_(msgid) msgid
38 search=strategy:broad/deep/random,
42 queue=:limit(n:queue_limit,"%s>0"),
43 drop:newest/oldest/random;
45 stop=:states(n:max_unique_states,"%s>0"),
46 :errors(n:max_errors),
47 :timeout(d:time_limit,"%s>0");
48 progress=progress:none/dots/fancy;
49 output=:verbosity(n:verbosity),
50 :errverbosity(n:err_verbosity),
56 static struct mc_options *parse_options (struct lexer *);
58 /* Parses a syntax description of model checker options from
59 LEXER and passes them, along with AUX, to the CHECKER
60 function, which must wrap a call to mc_run and return the
61 mc_results that it returned. This function then prints a
62 description of the mc_results to the output file. Returns
63 true if the model checker run found no errors, false
66 check_model (struct lexer *lexer,
67 struct mc_results *(*checker) (struct mc_options *, void *aux),
70 struct mc_options *options;
71 struct mc_results *results;
75 options = parse_options (lexer);
78 output_file = mc_options_get_output_file (options);
80 results = checker (options, aux);
82 mc_results_print (results, output_file);
84 if (output_file != stdout && output_file != stderr)
86 if (fwriteerror (output_file) < 0)
88 /* We've already discarded the name of the output file.
90 error (0, errno, "error closing output file");
94 ok = mc_results_get_error_count (results) == 0;
95 mc_results_destroy (results);
100 /* Fancy progress function for mc_options_set_progress_func. */
102 fancy_progress (struct mc *mc)
104 const struct mc_results *results = mc_get_results (mc);
105 if (mc_results_get_stop_reason (results) == MC_CONTINUING)
106 fprintf (stderr, "Processed %d unique states, max depth %d, "
107 "dropped %d duplicates...\r",
108 mc_results_get_unique_state_count (results),
109 mc_results_get_max_depth_reached (results),
110 mc_results_get_duplicate_dropped_states (results));
116 /* Parses options from LEXER and returns a corresponding
117 mc_options, or a null pointer if parsing fails. */
118 static struct mc_options *
119 parse_options (struct lexer *lexer)
121 struct cmd_check_model cmd;
122 struct mc_options *options;
124 if (!parse_check_model (lexer, NULL, &cmd, NULL))
127 options = mc_options_create ();
128 if (cmd.strategy != -1)
129 mc_options_set_strategy (options,
130 cmd.strategy == CHM_BROAD ? MC_BROAD
131 : cmd.strategy == CHM_DEEP ? MC_DEEP
132 : cmd.strategy == CHM_RANDOM ? MC_RANDOM
134 if (cmd.sbc_path > 0)
136 if (cmd.sbc_search > 0)
137 msg (SW, _("PATH and SEARCH subcommands are mutually exclusive. "
141 struct subc_list_int *list = &cmd.il_path[0];
142 int count = subc_list_int_count (list);
148 mc_path_init (&path);
149 for (i = 0; i < count; i++)
150 mc_path_push (&path, subc_list_int_at (list, i));
151 mc_options_set_follow_path (options, &path);
152 mc_path_destroy (&path);
155 msg (SW, _("At least one value must be specified on PATH."));
158 if (cmd.max_depth != LONG_MIN)
159 mc_options_set_max_depth (options, cmd.max_depth);
160 if (cmd.hash_bits != LONG_MIN)
163 mc_options_set_hash_bits (options, cmd.hash_bits);
164 hash_bits = mc_options_get_hash_bits (options);
165 if (hash_bits != cmd.hash_bits)
166 msg (SW, _("Hash bits adjusted to %d."), hash_bits);
168 if (cmd.queue_limit != LONG_MIN)
169 mc_options_set_queue_limit (options, cmd.queue_limit);
172 enum mc_queue_limit_strategy drop
173 = (cmd.drop == CHM_NEWEST ? MC_DROP_NEWEST
174 : cmd.drop == CHM_OLDEST ? MC_DROP_OLDEST
175 : cmd.drop == CHM_RANDOM ? MC_DROP_RANDOM
177 mc_options_set_queue_limit_strategy (options, drop);
179 if (cmd.sbc_search > 0)
180 mc_options_set_seed (options, cmd.n_seed[0]);
181 if (cmd.max_unique_states != LONG_MIN)
182 mc_options_set_max_unique_states (options, cmd.max_unique_states);
183 if (cmd.max_errors != LONG_MIN)
184 mc_options_set_max_errors (options, cmd.max_errors);
185 if (cmd.time_limit != SYSMIS)
186 mc_options_set_time_limit (options, cmd.time_limit);
187 if (cmd.verbosity != LONG_MIN)
188 mc_options_set_verbosity (options, cmd.verbosity);
189 if (cmd.err_verbosity != LONG_MIN)
190 mc_options_set_failure_verbosity (options, cmd.err_verbosity);
191 if (cmd.progress != -1)
193 if (cmd.progress == CHM_NONE)
194 mc_options_set_progress_usec (options, 0);
195 else if (cmd.progress == CHM_DOTS)
197 /* Nothing to do: that's the default anyway. */
199 else if (cmd.progress == CHM_FANCY)
200 mc_options_set_progress_func (options, fancy_progress);
202 if (cmd.output_file != NULL)
204 FILE *output_file = fopen (cmd.output_file, "w");
205 if (output_file == NULL)
207 error (0, errno, _("error opening \"%s\" for writing"),
209 free_check_model (&cmd);
210 mc_options_destroy (options);
213 mc_options_set_output_file (options, output_file);
217 free_check_model (&cmd);