fbacce2d8e63fdeaabc742676b32d4d5fb8e1ba0
[pspp-builds.git] / src / language / tests / check-model.q
1 /* PSPP - computes sample statistics.
2    Copyright (C) 2007 Free Software Foundation, Inc.
3
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.
8
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.
13
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
17    02110-1301, USA. */
18
19 #include <config.h>
20
21 #include <language/tests/check-model.h>
22
23 #include <errno.h>
24
25 #include <libpspp/model-checker.h>
26 #include <language/lexer/lexer.h>
27
28 #include "error.h"
29 #include "fwriteerror.h"
30
31 #include "gettext.h"
32 #define _(msgid) gettext (msgid)
33 #define N_(msgid) msgid
34
35 /* (headers) */
36
37 /* (specification)
38    "CHECK MODEL" (chm_):
39     search=strategy:broad/deep/random,
40            :mxd(n:max_depth),
41            :hash(n:hash_bits);
42     path=integer list;
43     queue=:limit(n:queue_limit,"%s>0"),
44           drop:newest/oldest/random;
45     seed=integer;
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),
52            :file(s:output_file).
53 */
54 /* (declarations) */
55 /* (functions) */
56
57 static struct mc_options *parse_options (struct lexer *);
58 static void print_results (const struct mc_results *, FILE *);
59
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
66    otherwise. */
67 bool
68 check_model (struct lexer *lexer,
69              struct mc_results *(*checker) (struct mc_options *, void *aux),
70              void *aux)
71 {
72   struct mc_options *options;
73   struct mc_results *results;
74   FILE *output_file;
75   bool ok;
76
77   options = parse_options (lexer);
78   if (options == NULL)
79     return false;
80   output_file = mc_options_get_output_file (options);
81
82   results = checker (options, aux);
83
84   print_results (results, output_file);
85
86   if (output_file != stdout && output_file != stderr)
87     {
88       if (fwriteerror (output_file) < 0)
89         {
90           /* We've already discarded the name of the output file.
91              Oh well. */
92           error (0, errno, "error closing output file");
93         }
94     }
95
96   ok = mc_results_get_error_count (results) == 0;
97   mc_results_destroy (results);
98
99   return ok;
100 }
101
102 /* Fancy progress function for mc_options_set_progress_func. */
103 static bool
104 fancy_progress (struct mc *mc)
105 {
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));
113   else
114     putc ('\n', stderr);
115   return true;
116 }
117
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)
122 {
123   struct cmd_check_model cmd;
124   struct mc_options *options;
125
126   if (!parse_check_model (lexer, NULL, &cmd, NULL))
127     return NULL;
128
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
135                              : -1);
136   if (cmd.sbc_path > 0)
137     {
138       if (cmd.sbc_search > 0)
139         msg (SW, _("PATH and SEARCH subcommands are mutually exclusive.  "
140                    "Ignoring PATH."));
141       else
142         {
143           struct subc_list_int *list = &cmd.il_path[0];
144           int count = subc_list_int_count (list);
145           if (count > 0)
146             {
147               struct mc_path path;
148               int i;
149
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);
155             }
156           else
157             msg (SW, _("At least one value must be specified on PATH."));
158         }
159     }
160   if (cmd.max_depth != NOT_LONG)
161     mc_options_set_max_depth (options, cmd.max_depth);
162   if (cmd.hash_bits != NOT_LONG)
163     {
164       int hash_bits;
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);
169     }
170   if (cmd.queue_limit != NOT_LONG)
171     mc_options_set_queue_limit (options, cmd.queue_limit);
172   if (cmd.drop != -1)
173     {
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
178            : -1);
179       mc_options_set_queue_limit_strategy (options, drop);
180     }
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)
194     {
195       if (cmd.progress == CHM_NONE)
196         mc_options_set_progress_usec (options, 0);
197       else if (cmd.progress == CHM_DOTS)
198         {
199           /* Nothing to do: that's the default anyway. */
200         }
201       else if (cmd.progress == CHM_FANCY)
202         mc_options_set_progress_func (options, fancy_progress);
203     }
204   if (cmd.output_file != NULL)
205     {
206       FILE *output_file = fopen (cmd.output_file, "w");
207       if (output_file == NULL)
208         {
209           error (0, errno, _("error opening \"%s\" for writing"),
210                  cmd.output_file);
211           free_check_model (&cmd);
212           mc_options_destroy (options);
213           return NULL;
214         }
215       mc_options_set_output_file (options, output_file);
216     }
217
218   return options;
219 }
220
221 /* Prints a description of RESULTS to stream F. */
222 static void
223 print_results (const struct mc_results *results, FILE *f)
224 {
225   enum mc_stop_reason reason = mc_results_get_stop_reason (results);
226
227   fputs ("\n"
228          "MODEL CHECKING SUMMARY\n"
229          "----------------------\n\n", f);
230
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"
238            : "unknown reason");
239   fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
240
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));
247
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));
260
261   fprintf (f, "Runtime: %.2f seconds\n",
262            mc_results_get_duration (results));
263
264   putc ('\n', f);
265 }
266
267 /*
268   Local Variables:
269   mode: c
270   End:
271 */