a2654717888d5232f679eacb57190b2284587b50
[pspp-builds.git] / src / language / tests / check-model.q
1 /* PSPP - a program for statistical analysis.
2    Copyright (C) 2007 Free Software Foundation, Inc.
3
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.
8
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.
13
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/>. */
16
17 #include <config.h>
18 #include <limits.h>
19
20 #include <language/tests/check-model.h>
21
22 #include <errno.h>
23
24 #include <libpspp/model-checker.h>
25 #include <language/lexer/lexer.h>
26
27 #include "error.h"
28 #include "fwriteerror.h"
29
30 #include "gettext.h"
31 #define _(msgid) gettext (msgid)
32 #define N_(msgid) msgid
33
34 /* (headers) */
35
36 /* (specification)
37    "CHECK MODEL" (chm_):
38     search=strategy:broad/deep/random,
39            :mxd(n:max_depth),
40            :hash(n:hash_bits);
41     path=integer list;
42     queue=:limit(n:queue_limit,"%s>0"),
43           drop:newest/oldest/random;
44     seed=integer;
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),
51            :file(s:output_file).
52 */
53 /* (declarations) */
54 /* (functions) */
55
56 static struct mc_options *parse_options (struct lexer *);
57 static void print_results (const struct mc_results *, FILE *);
58
59 /* Parses a syntax description of model checker options from
60    LEXER and passes them, along with AUX, to the CHECKER
61    function, which must wrap a call to mc_run and return the
62    mc_results that it returned.  This function then prints a
63    description of the mc_results to the output file.  Returns
64    true if the model checker run found no errors, false
65    otherwise. */
66 bool
67 check_model (struct lexer *lexer,
68              struct mc_results *(*checker) (struct mc_options *, void *aux),
69              void *aux)
70 {
71   struct mc_options *options;
72   struct mc_results *results;
73   FILE *output_file;
74   bool ok;
75
76   options = parse_options (lexer);
77   if (options == NULL)
78     return false;
79   output_file = mc_options_get_output_file (options);
80
81   results = checker (options, aux);
82
83   print_results (results, output_file);
84
85   if (output_file != stdout && output_file != stderr)
86     {
87       if (fwriteerror (output_file) < 0)
88         {
89           /* We've already discarded the name of the output file.
90              Oh well. */
91           error (0, errno, "error closing output file");
92         }
93     }
94
95   ok = mc_results_get_error_count (results) == 0;
96   mc_results_destroy (results);
97
98   return ok;
99 }
100
101 /* Fancy progress function for mc_options_set_progress_func. */
102 static bool
103 fancy_progress (struct mc *mc)
104 {
105   const struct mc_results *results = mc_get_results (mc);
106   if (mc_results_get_stop_reason (results) == MC_CONTINUING)
107     fprintf (stderr, "Processed %d unique states, max depth %d, "
108              "dropped %d duplicates...\r",
109              mc_results_get_unique_state_count (results),
110              mc_results_get_max_depth_reached (results),
111              mc_results_get_duplicate_dropped_states (results));
112   else
113     putc ('\n', stderr);
114   return true;
115 }
116
117 /* Parses options from LEXER and returns a corresponding
118    mc_options, or a null pointer if parsing fails. */
119 static struct mc_options *
120 parse_options (struct lexer *lexer)
121 {
122   struct cmd_check_model cmd;
123   struct mc_options *options;
124
125   if (!parse_check_model (lexer, NULL, &cmd, NULL))
126     return NULL;
127
128   options = mc_options_create ();
129   if (cmd.strategy != -1)
130     mc_options_set_strategy (options,
131                              cmd.strategy == CHM_BROAD ? MC_BROAD
132                              : cmd.strategy == CHM_DEEP ? MC_DEEP
133                              : cmd.strategy == CHM_RANDOM ? MC_RANDOM
134                              : -1);
135   if (cmd.sbc_path > 0)
136     {
137       if (cmd.sbc_search > 0)
138         msg (SW, _("PATH and SEARCH subcommands are mutually exclusive.  "
139                    "Ignoring PATH."));
140       else
141         {
142           struct subc_list_int *list = &cmd.il_path[0];
143           int count = subc_list_int_count (list);
144           if (count > 0)
145             {
146               struct mc_path path;
147               int i;
148
149               mc_path_init (&path);
150               for (i = 0; i < count; i++)
151                 mc_path_push (&path, subc_list_int_at (list, i));
152               mc_options_set_follow_path (options, &path);
153               mc_path_destroy (&path);
154             }
155           else
156             msg (SW, _("At least one value must be specified on PATH."));
157         }
158     }
159   if (cmd.max_depth != LONG_MIN)
160     mc_options_set_max_depth (options, cmd.max_depth);
161   if (cmd.hash_bits != LONG_MIN)
162     {
163       int hash_bits;
164       mc_options_set_hash_bits (options, cmd.hash_bits);
165       hash_bits = mc_options_get_hash_bits (options);
166       if (hash_bits != cmd.hash_bits)
167         msg (SW, _("Hash bits adjusted to %d."), hash_bits);
168     }
169   if (cmd.queue_limit != LONG_MIN)
170     mc_options_set_queue_limit (options, cmd.queue_limit);
171   if (cmd.drop != -1)
172     {
173       enum mc_queue_limit_strategy drop
174         = (cmd.drop == CHM_NEWEST ? MC_DROP_NEWEST
175            : cmd.drop == CHM_OLDEST ? MC_DROP_OLDEST
176            : cmd.drop == CHM_RANDOM ? MC_DROP_RANDOM
177            : -1);
178       mc_options_set_queue_limit_strategy (options, drop);
179     }
180   if (cmd.sbc_search > 0)
181     mc_options_set_seed (options, cmd.n_seed[0]);
182   if (cmd.max_unique_states != LONG_MIN)
183     mc_options_set_max_unique_states (options, cmd.max_unique_states);
184   if (cmd.max_errors != LONG_MIN)
185     mc_options_set_max_errors (options, cmd.max_errors);
186   if (cmd.time_limit != SYSMIS)
187     mc_options_set_time_limit (options, cmd.time_limit);
188   if (cmd.verbosity != LONG_MIN)
189     mc_options_set_verbosity (options, cmd.verbosity);
190   if (cmd.err_verbosity != LONG_MIN)
191     mc_options_set_failure_verbosity (options, cmd.err_verbosity);
192   if (cmd.progress != -1)
193     {
194       if (cmd.progress == CHM_NONE)
195         mc_options_set_progress_usec (options, 0);
196       else if (cmd.progress == CHM_DOTS)
197         {
198           /* Nothing to do: that's the default anyway. */
199         }
200       else if (cmd.progress == CHM_FANCY)
201         mc_options_set_progress_func (options, fancy_progress);
202     }
203   if (cmd.output_file != NULL)
204     {
205       FILE *output_file = fopen (cmd.output_file, "w");
206       if (output_file == NULL)
207         {
208           error (0, errno, _("error opening \"%s\" for writing"),
209                  cmd.output_file);
210           free_check_model (&cmd);
211           mc_options_destroy (options);
212           return NULL;
213         }
214       mc_options_set_output_file (options, output_file);
215     }
216
217
218   free_check_model (&cmd);
219
220   return options;
221 }
222
223 /* Prints a description of RESULTS to stream F. */
224 static void
225 print_results (const struct mc_results *results, FILE *f)
226 {
227   enum mc_stop_reason reason = mc_results_get_stop_reason (results);
228
229   fputs ("\n"
230          "MODEL CHECKING SUMMARY\n"
231          "----------------------\n\n", f);
232
233   fprintf (f, "Stopped by: %s\n",
234            reason == MC_SUCCESS ? "state space exhaustion"
235            : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
236            : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
237            : reason == MC_END_OF_PATH ? "reached end of specified path"
238            : reason == MC_TIMEOUT ? "reaching time limit"
239            : reason == MC_INTERRUPTED ? "user interruption"
240            : "unknown reason");
241   fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
242
243   fprintf (f, "Unique states checked: %d\n",
244            mc_results_get_unique_state_count (results));
245   fprintf (f, "Maximum depth reached: %d\n",
246            mc_results_get_max_depth_reached (results));
247   fprintf (f, "Mean depth reached: %.2f\n\n",
248            mc_results_get_mean_depth_reached (results));
249
250   fprintf (f, "Dropped duplicate states: %d\n",
251            mc_results_get_duplicate_dropped_states (results));
252   fprintf (f, "Dropped off-path states: %d\n",
253            mc_results_get_off_path_dropped_states (results));
254   fprintf (f, "Dropped too-deep states: %d\n",
255            mc_results_get_depth_dropped_states (results));
256   fprintf (f, "Dropped queue-overflow states: %d\n",
257            mc_results_get_queue_dropped_states (results));
258   fprintf (f, "Checked states still queued when stopped: %d\n",
259            mc_results_get_queued_unprocessed_states (results));
260   fprintf (f, "Maximum queue length reached: %d\n\n",
261            mc_results_get_max_queue_length (results));
262
263   fprintf (f, "Runtime: %.2f seconds\n",
264            mc_results_get_duration (results));
265
266   putc ('\n', f);
267 }
268
269 /*
270   Local Variables:
271   mode: c
272   End:
273 */