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>
43 /* lazy_casereader callback function to instantiate a casereader
44 from the datasheet. */
45 static struct casereader *
46 lazy_callback (void *ds_)
48 struct datasheet *ds = ds_;
49 return datasheet_make_reader (ds);
53 /* Maximum size of datasheet supported for model checking
59 /* Checks that READER contains the ROW_CNT rows and COLUMN_CNT
60 columns of data in ARRAY, reporting any errors via MC. */
62 check_datasheet_casereader (struct mc *mc, struct casereader *reader,
63 double array[MAX_ROWS][MAX_COLS],
64 size_t row_cnt, size_t column_cnt)
66 if (casereader_get_case_cnt (reader) != row_cnt)
68 if (casereader_get_case_cnt (reader) == CASENUMBER_MAX
69 && casereader_count_cases (reader) == row_cnt)
70 mc_error (mc, "datasheet casereader has unknown case count");
72 mc_error (mc, "casereader row count (%lu) does not match "
74 (unsigned long int) casereader_get_case_cnt (reader),
77 else if (casereader_get_value_cnt (reader) != column_cnt)
78 mc_error (mc, "casereader column count (%zu) does not match "
80 casereader_get_value_cnt (reader), column_cnt);
86 for (row = 0; row < row_cnt; row++)
90 c = casereader_read (reader);
93 mc_error (mc, "casereader_read failed reading row %zu of %zu "
94 "(%zu columns)", row, row_cnt, column_cnt);
98 for (col = 0; col < column_cnt; col++)
99 if (case_num_idx (c, col) != array[row][col])
100 mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: "
102 row, col, row_cnt, column_cnt,
103 case_num_idx (c, col), array[row][col]);
108 c = casereader_read (reader);
110 mc_error (mc, "casereader has extra cases (expected %zu)", row_cnt);
114 /* Checks that datasheet DS contains has ROW_CNT rows, COLUMN_CNT
115 columns, and the same contents as ARRAY, reporting any
116 mismatches via mc_error. Then, adds DS to MC as a new state. */
118 check_datasheet (struct mc *mc, struct datasheet *ds,
119 double array[MAX_ROWS][MAX_COLS],
120 size_t row_cnt, size_t column_cnt)
122 struct datasheet *ds2;
123 struct casereader *reader;
124 unsigned long int serial = 0;
126 assert (row_cnt < MAX_ROWS);
127 assert (column_cnt < MAX_COLS);
129 /* If it is a duplicate hash, discard the state before checking
130 its consistency, to save time. */
131 if (mc_discard_dup_state (mc, hash_datasheet (ds)))
133 datasheet_destroy (ds);
137 /* Check contents of datasheet via datasheet functions. */
138 if (row_cnt != datasheet_get_row_cnt (ds))
139 mc_error (mc, "row count (%lu) does not match expected (%zu)",
140 (unsigned long int) datasheet_get_row_cnt (ds), row_cnt);
141 else if (column_cnt != datasheet_get_column_cnt (ds))
142 mc_error (mc, "column count (%zu) does not match expected (%zu)",
143 datasheet_get_column_cnt (ds), column_cnt);
148 for (row = 0; row < row_cnt; row++)
149 for (col = 0; col < column_cnt; col++)
152 if (!datasheet_get_value (ds, row, col, &v, 1))
154 if (v.f != array[row][col])
155 mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: %g != %g",
156 row, col, row_cnt, column_cnt, v.f, array[row][col]);
160 /* Check that datasheet contents are correct when read through
162 ds2 = clone_datasheet (ds);
163 reader = datasheet_make_reader (ds2);
164 check_datasheet_casereader (mc, reader, array, row_cnt, column_cnt);
165 casereader_destroy (reader);
167 /* Check that datasheet contents are correct when read through
168 casereader with lazy_casereader wrapped around it. This is
169 valuable because otherwise there is no non-GUI code that
170 uses the lazy_casereader. */
171 ds2 = clone_datasheet (ds);
172 reader = lazy_casereader_create (column_cnt, row_cnt,
173 lazy_callback, ds2, &serial);
174 check_datasheet_casereader (mc, reader, array, row_cnt, column_cnt);
175 if (lazy_casereader_destroy (reader, serial))
177 /* Lazy casereader was never instantiated. This will
178 only happen if there are no rows (because in that case
179 casereader_read never gets called). */
180 datasheet_destroy (ds2);
182 mc_error (mc, "lazy casereader not instantiated, but should "
183 "have been (size %zu,%zu)", row_cnt, column_cnt);
187 /* Lazy casereader was instantiated. This is the common
188 case, in which some casereader operation
189 (casereader_read in this case) was performed on the
191 casereader_destroy (reader);
193 mc_error (mc, "lazy casereader instantiated, but should not "
194 "have been (size %zu,%zu)", row_cnt, column_cnt);
197 mc_add_state (mc, ds);
200 /* Extracts the contents of DS into DATA. */
202 extract_data (const struct datasheet *ds, double data[MAX_ROWS][MAX_COLS])
204 size_t column_cnt = datasheet_get_column_cnt (ds);
205 size_t row_cnt = datasheet_get_row_cnt (ds);
208 assert (row_cnt < MAX_ROWS);
209 assert (column_cnt < MAX_COLS);
210 for (row = 0; row < row_cnt; row++)
211 for (col = 0; col < column_cnt; col++)
214 if (!datasheet_get_value (ds, row, col, &v, 1))
216 data[row][col] = v.f;
220 /* Clones the structure and contents of ODS into *DS,
221 and the contents of ODATA into DATA. */
223 clone_model (const struct datasheet *ods, double odata[MAX_ROWS][MAX_COLS],
224 struct datasheet **ds, double data[MAX_ROWS][MAX_COLS])
226 *ds = clone_datasheet (ods);
227 memcpy (data, odata, MAX_ROWS * MAX_COLS * sizeof **data);
230 /* "init" function for struct mc_class. */
232 datasheet_mc_init (struct mc *mc)
234 struct datasheet_test_params *params = mc_get_aux (mc);
235 struct datasheet *ds;
237 if (params->backing_rows == 0 && params->backing_cols == 0)
239 /* Create unbacked datasheet. */
240 ds = datasheet_create (NULL);
241 mc_name_operation (mc, "empty datasheet");
242 check_datasheet (mc, ds, NULL, 0, 0);
246 /* Create datasheet with backing. */
247 struct casewriter *writer;
248 struct casereader *reader;
249 double data[MAX_ROWS][MAX_COLS];
252 assert (params->backing_rows > 0 && params->backing_rows <= MAX_ROWS);
253 assert (params->backing_cols > 0 && params->backing_cols <= MAX_COLS);
255 writer = mem_writer_create (params->backing_cols);
256 for (row = 0; row < params->backing_rows; row++)
261 c = case_create (params->backing_cols);
262 for (col = 0; col < params->backing_cols; col++)
264 double value = params->next_value++;
265 data[row][col] = value;
266 case_data_rw_idx (c, col)->f = value;
268 casewriter_write (writer, c);
270 reader = casewriter_make_reader (writer);
271 assert (reader != NULL);
273 ds = datasheet_create (reader);
274 mc_name_operation (mc, "datasheet with (%d,%d) backing",
275 params->backing_rows, params->backing_cols);
276 check_datasheet (mc, ds, data,
277 params->backing_rows, params->backing_cols);
281 /* "mutate" function for struct mc_class. */
283 datasheet_mc_mutate (struct mc *mc, const void *ods_)
285 struct datasheet_test_params *params = mc_get_aux (mc);
287 const struct datasheet *ods = ods_;
288 double odata[MAX_ROWS][MAX_COLS];
289 double data[MAX_ROWS][MAX_COLS];
290 size_t column_cnt = datasheet_get_column_cnt (ods);
291 size_t row_cnt = datasheet_get_row_cnt (ods);
292 size_t pos, new_pos, cnt;
294 extract_data (ods, odata);
296 /* Insert all possible numbers of columns in all possible
298 for (pos = 0; pos <= column_cnt; pos++)
299 for (cnt = 0; cnt <= params->max_cols - column_cnt; cnt++)
300 if (mc_include_state (mc))
302 struct datasheet *ds;
303 union value new[MAX_COLS];
306 mc_name_operation (mc, "insert %zu columns at %zu", cnt, pos);
307 clone_model (ods, odata, &ds, data);
309 for (i = 0; i < cnt; i++)
310 new[i].f = params->next_value++;
312 if (!datasheet_insert_columns (ds, new, cnt, pos))
313 mc_error (mc, "datasheet_insert_columns failed");
315 for (i = 0; i < row_cnt; i++)
317 insert_range (&data[i][0], column_cnt, sizeof data[i][0],
319 for (j = 0; j < cnt; j++)
320 data[i][pos + j] = new[j].f;
323 check_datasheet (mc, ds, data, row_cnt, column_cnt + cnt);
326 /* Delete all possible numbers of columns from all possible
328 for (pos = 0; pos < column_cnt; pos++)
329 for (cnt = 0; cnt < column_cnt - pos; cnt++)
330 if (mc_include_state (mc))
332 struct datasheet *ds;
335 mc_name_operation (mc, "delete %zu columns at %zu", cnt, pos);
336 clone_model (ods, odata, &ds, data);
338 datasheet_delete_columns (ds, pos, cnt);
340 for (i = 0; i < row_cnt; i++)
341 remove_range (&data[i], column_cnt, sizeof *data[i], pos, cnt);
343 check_datasheet (mc, ds, data, row_cnt, column_cnt - cnt);
346 /* Move all possible numbers of columns from all possible
347 existing positions to all possible new positions. */
348 for (pos = 0; pos < column_cnt; pos++)
349 for (cnt = 0; cnt < column_cnt - pos; cnt++)
350 for (new_pos = 0; new_pos < column_cnt - cnt; new_pos++)
351 if (mc_include_state (mc))
353 struct datasheet *ds;
356 clone_model (ods, odata, &ds, data);
357 mc_name_operation (mc, "move %zu columns from %zu to %zu",
360 datasheet_move_columns (ds, pos, new_pos, cnt);
362 for (i = 0; i < row_cnt; i++)
363 move_range (&data[i], column_cnt, sizeof data[i][0],
366 check_datasheet (mc, ds, data, row_cnt, column_cnt);
369 /* Insert all possible numbers of rows in all possible
371 for (pos = 0; pos <= row_cnt; pos++)
372 for (cnt = 0; cnt <= params->max_rows - row_cnt; cnt++)
373 if (mc_include_state (mc))
375 struct datasheet *ds;
376 struct ccase *c[MAX_ROWS];
379 clone_model (ods, odata, &ds, data);
380 mc_name_operation (mc, "insert %zu rows at %zu", cnt, pos);
382 for (i = 0; i < cnt; i++)
384 c[i] = case_create (column_cnt);
385 for (j = 0; j < column_cnt; j++)
386 case_data_rw_idx (c[i], j)->f = params->next_value++;
389 insert_range (data, row_cnt, sizeof data[pos], pos, cnt);
390 for (i = 0; i < cnt; i++)
391 for (j = 0; j < column_cnt; j++)
392 data[i + pos][j] = case_num_idx (c[i], j);
394 if (!datasheet_insert_rows (ds, pos, c, cnt))
395 mc_error (mc, "datasheet_insert_rows failed");
397 check_datasheet (mc, ds, data, row_cnt + cnt, column_cnt);
400 /* Delete all possible numbers of rows from all possible
402 for (pos = 0; pos < row_cnt; pos++)
403 for (cnt = 0; cnt < row_cnt - pos; cnt++)
404 if (mc_include_state (mc))
406 struct datasheet *ds;
408 clone_model (ods, odata, &ds, data);
409 mc_name_operation (mc, "delete %zu rows at %zu", cnt, pos);
411 datasheet_delete_rows (ds, pos, cnt);
413 remove_range (&data[0], row_cnt, sizeof data[0], pos, cnt);
415 check_datasheet (mc, ds, data, row_cnt - cnt, column_cnt);
418 /* Move all possible numbers of rows from all possible existing
419 positions to all possible new positions. */
420 for (pos = 0; pos < row_cnt; pos++)
421 for (cnt = 0; cnt < row_cnt - pos; cnt++)
422 for (new_pos = 0; new_pos < row_cnt - cnt; new_pos++)
423 if (mc_include_state (mc))
425 struct datasheet *ds;
427 clone_model (ods, odata, &ds, data);
428 mc_name_operation (mc, "move %zu rows from %zu to %zu",
431 datasheet_move_rows (ds, pos, new_pos, cnt);
433 move_range (&data[0], row_cnt, sizeof data[0],
436 check_datasheet (mc, ds, data, row_cnt, column_cnt);
440 /* "destroy" function for struct mc_class. */
442 datasheet_mc_destroy (const struct mc *mc UNUSED, void *ds_)
444 struct datasheet *ds = ds_;
445 datasheet_destroy (ds);
448 /* Executes the model checker on the datasheet test driver with
449 the given OPTIONS and passing in the given PARAMS, which must
450 point to a modifiable "struct datasheet_test_params". If any
451 value in PARAMS is out of range, it will be adjusted into the
452 valid range before running the test.
454 Returns the results of the model checking run. */
456 datasheet_test (struct mc_options *options, void *params_)
458 struct datasheet_test_params *params = params_;
459 static const struct mc_class datasheet_mc_class =
463 datasheet_mc_destroy,
466 params->next_value = 1;
467 params->max_rows = MIN (params->max_rows, MAX_ROWS);
468 params->max_cols = MIN (params->max_cols, MAX_COLS);
469 params->backing_rows = MIN (params->backing_rows, params->max_rows);
470 params->backing_cols = MIN (params->backing_cols, params->max_cols);
472 mc_options_set_aux (options, params);
473 return mc_run (&datasheet_mc_class, options);