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/>. */
19 #include <data/datasheet.h>
20 #include "datasheet-check.h"
21 #include "model-checker.h"
26 #include <data/casereader-provider.h>
27 #include <data/casereader.h>
28 #include <data/casewriter.h>
29 #include <data/lazy-casereader.h>
30 #include <data/sparse-cases.h>
31 #include <libpspp/array.h>
32 #include <libpspp/assertion.h>
33 #include <libpspp/range-map.h>
34 #include <libpspp/range-set.h>
35 #include <libpspp/taint.h>
36 #include <libpspp/tower.h>
42 /* lazy_casereader callback function to instantiate a casereader
43 from the datasheet. */
44 static struct casereader *
45 lazy_callback (void *ds_)
47 struct datasheet *ds = ds_;
48 return datasheet_make_reader (ds);
52 /* Maximum size of datasheet supported for model checking
58 /* Checks that READER contains the ROW_CNT rows and COLUMN_CNT
59 columns of data in ARRAY, reporting any errors via MC. */
61 check_datasheet_casereader (struct mc *mc, struct casereader *reader,
62 double array[MAX_ROWS][MAX_COLS],
63 size_t row_cnt, size_t column_cnt)
65 if (casereader_get_case_cnt (reader) != row_cnt)
67 if (casereader_get_case_cnt (reader) == CASENUMBER_MAX
68 && casereader_count_cases (reader) == row_cnt)
69 mc_error (mc, "datasheet casereader has unknown case count");
71 mc_error (mc, "casereader row count (%lu) does not match "
73 (unsigned long int) casereader_get_case_cnt (reader),
76 else if (casereader_get_value_cnt (reader) != column_cnt)
77 mc_error (mc, "casereader column count (%zu) does not match "
79 casereader_get_value_cnt (reader), column_cnt);
85 for (row = 0; row < row_cnt; row++)
89 c = casereader_read (reader);
92 mc_error (mc, "casereader_read failed reading row %zu of %zu "
93 "(%zu columns)", row, row_cnt, column_cnt);
97 for (col = 0; col < column_cnt; col++)
98 if (case_num_idx (c, col) != array[row][col])
99 mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: "
101 row, col, row_cnt, column_cnt,
102 case_num_idx (c, col), array[row][col]);
107 c = casereader_read (reader);
109 mc_error (mc, "casereader has extra cases (expected %zu)", row_cnt);
113 /* Checks that datasheet DS contains has ROW_CNT rows, COLUMN_CNT
114 columns, and the same contents as ARRAY, reporting any
115 mismatches via mc_error. Then, adds DS to MC as a new state. */
117 check_datasheet (struct mc *mc, struct datasheet *ds,
118 double array[MAX_ROWS][MAX_COLS],
119 size_t row_cnt, size_t column_cnt)
121 struct datasheet *ds2;
122 struct casereader *reader;
123 unsigned long int serial = 0;
125 assert (row_cnt < MAX_ROWS);
126 assert (column_cnt < MAX_COLS);
128 /* If it is a duplicate hash, discard the state before checking
129 its consistency, to save time. */
130 if (mc_discard_dup_state (mc, hash_datasheet (ds)))
132 datasheet_destroy (ds);
136 /* Check contents of datasheet via datasheet functions. */
137 if (row_cnt != datasheet_get_row_cnt (ds))
138 mc_error (mc, "row count (%lu) does not match expected (%zu)",
139 (unsigned long int) datasheet_get_row_cnt (ds), row_cnt);
140 else if (column_cnt != datasheet_get_column_cnt (ds))
141 mc_error (mc, "column count (%zu) does not match expected (%zu)",
142 datasheet_get_column_cnt (ds), column_cnt);
147 for (row = 0; row < row_cnt; row++)
148 for (col = 0; col < column_cnt; col++)
151 if (!datasheet_get_value (ds, row, col, &v, 1))
153 if (v.f != array[row][col])
154 mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: %g != %g",
155 row, col, row_cnt, column_cnt, v.f, array[row][col]);
159 /* Check that datasheet contents are correct when read through
161 ds2 = clone_datasheet (ds);
162 reader = datasheet_make_reader (ds2);
163 check_datasheet_casereader (mc, reader, array, row_cnt, column_cnt);
164 casereader_destroy (reader);
166 /* Check that datasheet contents are correct when read through
167 casereader with lazy_casereader wrapped around it. This is
168 valuable because otherwise there is no non-GUI code that
169 uses the lazy_casereader. */
170 ds2 = clone_datasheet (ds);
171 reader = lazy_casereader_create (column_cnt, row_cnt,
172 lazy_callback, ds2, &serial);
173 check_datasheet_casereader (mc, reader, array, row_cnt, column_cnt);
174 if (lazy_casereader_destroy (reader, serial))
176 /* Lazy casereader was never instantiated. This will
177 only happen if there are no rows (because in that case
178 casereader_read never gets called). */
179 datasheet_destroy (ds2);
181 mc_error (mc, "lazy casereader not instantiated, but should "
182 "have been (size %zu,%zu)", row_cnt, column_cnt);
186 /* Lazy casereader was instantiated. This is the common
187 case, in which some casereader operation
188 (casereader_read in this case) was performed on the
190 casereader_destroy (reader);
192 mc_error (mc, "lazy casereader instantiated, but should not "
193 "have been (size %zu,%zu)", row_cnt, column_cnt);
196 mc_add_state (mc, ds);
199 /* Extracts the contents of DS into DATA. */
201 extract_data (const struct datasheet *ds, double data[MAX_ROWS][MAX_COLS])
203 size_t column_cnt = datasheet_get_column_cnt (ds);
204 size_t row_cnt = datasheet_get_row_cnt (ds);
207 assert (row_cnt < MAX_ROWS);
208 assert (column_cnt < MAX_COLS);
209 for (row = 0; row < row_cnt; row++)
210 for (col = 0; col < column_cnt; col++)
213 if (!datasheet_get_value (ds, row, col, &v, 1))
215 data[row][col] = v.f;
219 /* Clones the structure and contents of ODS into *DS,
220 and the contents of ODATA into DATA. */
222 clone_model (const struct datasheet *ods, double odata[MAX_ROWS][MAX_COLS],
223 struct datasheet **ds, double data[MAX_ROWS][MAX_COLS])
225 *ds = clone_datasheet (ods);
226 memcpy (data, odata, MAX_ROWS * MAX_COLS * sizeof **data);
229 /* "init" function for struct mc_class. */
231 datasheet_mc_init (struct mc *mc)
233 struct datasheet_test_params *params = mc_get_aux (mc);
234 struct datasheet *ds;
236 if (params->backing_rows == 0 && params->backing_cols == 0)
238 /* Create unbacked datasheet. */
239 ds = datasheet_create (NULL);
240 mc_name_operation (mc, "empty datasheet");
241 check_datasheet (mc, ds, NULL, 0, 0);
245 /* Create datasheet with backing. */
246 struct casewriter *writer;
247 struct casereader *reader;
248 double data[MAX_ROWS][MAX_COLS];
251 assert (params->backing_rows > 0 && params->backing_rows <= MAX_ROWS);
252 assert (params->backing_cols > 0 && params->backing_cols <= MAX_COLS);
254 writer = mem_writer_create (params->backing_cols);
255 for (row = 0; row < params->backing_rows; row++)
260 c = case_create (params->backing_cols);
261 for (col = 0; col < params->backing_cols; col++)
263 double value = params->next_value++;
264 data[row][col] = value;
265 case_data_rw_idx (c, col)->f = value;
267 casewriter_write (writer, c);
269 reader = casewriter_make_reader (writer);
270 assert (reader != NULL);
272 ds = datasheet_create (reader);
273 mc_name_operation (mc, "datasheet with (%d,%d) backing",
274 params->backing_rows, params->backing_cols);
275 check_datasheet (mc, ds, data,
276 params->backing_rows, params->backing_cols);
280 /* "mutate" function for struct mc_class. */
282 datasheet_mc_mutate (struct mc *mc, const void *ods_)
284 struct datasheet_test_params *params = mc_get_aux (mc);
286 const struct datasheet *ods = ods_;
287 double odata[MAX_ROWS][MAX_COLS];
288 double data[MAX_ROWS][MAX_COLS];
289 size_t column_cnt = datasheet_get_column_cnt (ods);
290 size_t row_cnt = datasheet_get_row_cnt (ods);
291 size_t pos, new_pos, cnt;
293 extract_data (ods, odata);
295 /* Insert all possible numbers of columns in all possible
297 for (pos = 0; pos <= column_cnt; pos++)
298 for (cnt = 0; cnt <= params->max_cols - column_cnt; cnt++)
299 if (mc_include_state (mc))
301 struct datasheet *ds;
302 union value new[MAX_COLS];
305 mc_name_operation (mc, "insert %zu columns at %zu", cnt, pos);
306 clone_model (ods, odata, &ds, data);
308 for (i = 0; i < cnt; i++)
309 new[i].f = params->next_value++;
311 if (!datasheet_insert_columns (ds, new, cnt, pos))
312 mc_error (mc, "datasheet_insert_columns failed");
314 for (i = 0; i < row_cnt; i++)
316 insert_range (&data[i][0], column_cnt, sizeof data[i][0],
318 for (j = 0; j < cnt; j++)
319 data[i][pos + j] = new[j].f;
322 check_datasheet (mc, ds, data, row_cnt, column_cnt + cnt);
325 /* Delete all possible numbers of columns from all possible
327 for (pos = 0; pos < column_cnt; pos++)
328 for (cnt = 0; cnt < column_cnt - pos; cnt++)
329 if (mc_include_state (mc))
331 struct datasheet *ds;
334 mc_name_operation (mc, "delete %zu columns at %zu", cnt, pos);
335 clone_model (ods, odata, &ds, data);
337 datasheet_delete_columns (ds, pos, cnt);
339 for (i = 0; i < row_cnt; i++)
340 remove_range (&data[i], column_cnt, sizeof *data[i], pos, cnt);
342 check_datasheet (mc, ds, data, row_cnt, column_cnt - cnt);
345 /* Move all possible numbers of columns from all possible
346 existing positions to all possible new positions. */
347 for (pos = 0; pos < column_cnt; pos++)
348 for (cnt = 0; cnt < column_cnt - pos; cnt++)
349 for (new_pos = 0; new_pos < column_cnt - cnt; new_pos++)
350 if (mc_include_state (mc))
352 struct datasheet *ds;
355 clone_model (ods, odata, &ds, data);
356 mc_name_operation (mc, "move %zu columns from %zu to %zu",
359 datasheet_move_columns (ds, pos, new_pos, cnt);
361 for (i = 0; i < row_cnt; i++)
362 move_range (&data[i], column_cnt, sizeof data[i][0],
365 check_datasheet (mc, ds, data, row_cnt, column_cnt);
368 /* Insert all possible numbers of rows in all possible
370 for (pos = 0; pos <= row_cnt; pos++)
371 for (cnt = 0; cnt <= params->max_rows - row_cnt; cnt++)
372 if (mc_include_state (mc))
374 struct datasheet *ds;
375 struct ccase *c[MAX_ROWS];
378 clone_model (ods, odata, &ds, data);
379 mc_name_operation (mc, "insert %zu rows at %zu", cnt, pos);
381 for (i = 0; i < cnt; i++)
383 c[i] = case_create (column_cnt);
384 for (j = 0; j < column_cnt; j++)
385 case_data_rw_idx (c[i], j)->f = params->next_value++;
388 insert_range (data, row_cnt, sizeof data[pos], pos, cnt);
389 for (i = 0; i < cnt; i++)
390 for (j = 0; j < column_cnt; j++)
391 data[i + pos][j] = case_num_idx (c[i], j);
393 if (!datasheet_insert_rows (ds, pos, c, cnt))
394 mc_error (mc, "datasheet_insert_rows failed");
396 check_datasheet (mc, ds, data, row_cnt + cnt, column_cnt);
399 /* Delete all possible numbers of rows from all possible
401 for (pos = 0; pos < row_cnt; pos++)
402 for (cnt = 0; cnt < row_cnt - pos; cnt++)
403 if (mc_include_state (mc))
405 struct datasheet *ds;
407 clone_model (ods, odata, &ds, data);
408 mc_name_operation (mc, "delete %zu rows at %zu", cnt, pos);
410 datasheet_delete_rows (ds, pos, cnt);
412 remove_range (&data[0], row_cnt, sizeof data[0], pos, cnt);
414 check_datasheet (mc, ds, data, row_cnt - cnt, column_cnt);
417 /* Move all possible numbers of rows from all possible existing
418 positions to all possible new positions. */
419 for (pos = 0; pos < row_cnt; pos++)
420 for (cnt = 0; cnt < row_cnt - pos; cnt++)
421 for (new_pos = 0; new_pos < row_cnt - cnt; new_pos++)
422 if (mc_include_state (mc))
424 struct datasheet *ds;
426 clone_model (ods, odata, &ds, data);
427 mc_name_operation (mc, "move %zu rows from %zu to %zu",
430 datasheet_move_rows (ds, pos, new_pos, cnt);
432 move_range (&data[0], row_cnt, sizeof data[0],
435 check_datasheet (mc, ds, data, row_cnt, column_cnt);
439 /* "destroy" function for struct mc_class. */
441 datasheet_mc_destroy (const struct mc *mc UNUSED, void *ds_)
443 struct datasheet *ds = ds_;
444 datasheet_destroy (ds);
447 /* Executes the model checker on the datasheet test driver with
448 the given OPTIONS and passing in the given PARAMS, which must
449 point to a modifiable "struct datasheet_test_params". If any
450 value in PARAMS is out of range, it will be adjusted into the
451 valid range before running the test.
453 Returns the results of the model checking run. */
455 datasheet_test (struct mc_options *options, void *params_)
457 struct datasheet_test_params *params = params_;
458 static const struct mc_class datasheet_mc_class =
462 datasheet_mc_destroy,
465 params->next_value = 1;
466 params->max_rows = MIN (params->max_rows, MAX_ROWS);
467 params->max_cols = MIN (params->max_cols, MAX_COLS);
468 params->backing_rows = MIN (params->backing_rows, params->max_rows);
469 params->backing_cols = MIN (params->backing_cols, params->max_cols);
471 mc_options_set_aux (options, params);
472 return mc_run (&datasheet_mc_class, options);