-}
-
-/* "mutate" function for struct mc_class. */
-static void
-datasheet_mc_mutate (struct mc *mc, const void *ods_)
-{
- struct datasheet_test_params *params = mc_get_aux (mc);
-
- const struct datasheet *ods = ods_;
- double odata[MAX_ROWS][MAX_COLS];
- double data[MAX_ROWS][MAX_COLS];
- size_t column_cnt = datasheet_get_column_cnt (ods);
- size_t row_cnt = datasheet_get_row_cnt (ods);
- size_t pos, new_pos, cnt;
-
- extract_data (ods, odata);
-
- /* Insert all possible numbers of columns in all possible
- positions. */
- for (pos = 0; pos <= column_cnt; pos++)
- for (cnt = 0; cnt <= params->max_cols - column_cnt; cnt++)
- if (mc_include_state (mc))
- {
- struct datasheet *ds;
- union value new[MAX_COLS];
- size_t i, j;
-
- mc_name_operation (mc, "insert %zu columns at %zu", cnt, pos);
- clone_model (ods, odata, &ds, data);
-
- for (i = 0; i < cnt; i++)
- new[i].f = params->next_value++;
-
- if (!datasheet_insert_columns (ds, new, cnt, pos))
- mc_error (mc, "datasheet_insert_columns failed");
-
- for (i = 0; i < row_cnt; i++)
- {
- insert_range (&data[i][0], column_cnt, sizeof data[i][0],
- pos, cnt);
- for (j = 0; j < cnt; j++)
- data[i][pos + j] = new[j].f;
- }
-
- check_datasheet (mc, ds, data, row_cnt, column_cnt + cnt);
- }
-
- /* Delete all possible numbers of columns from all possible
- positions. */
- for (pos = 0; pos < column_cnt; pos++)
- for (cnt = 0; cnt < column_cnt - pos; cnt++)
- if (mc_include_state (mc))
- {
- struct datasheet *ds;
- size_t i;
-
- mc_name_operation (mc, "delete %zu columns at %zu", cnt, pos);
- clone_model (ods, odata, &ds, data);
-
- datasheet_delete_columns (ds, pos, cnt);
-
- for (i = 0; i < row_cnt; i++)
- remove_range (&data[i], column_cnt, sizeof *data[i], pos, cnt);
-
- check_datasheet (mc, ds, data, row_cnt, column_cnt - cnt);
- }
-
- /* Move all possible numbers of columns from all possible
- existing positions to all possible new positions. */
- for (pos = 0; pos < column_cnt; pos++)
- for (cnt = 0; cnt < column_cnt - pos; cnt++)
- for (new_pos = 0; new_pos < column_cnt - cnt; new_pos++)
- if (mc_include_state (mc))
- {
- struct datasheet *ds;
- size_t i;
-
- clone_model (ods, odata, &ds, data);
- mc_name_operation (mc, "move %zu columns from %zu to %zu",
- cnt, pos, new_pos);
-
- datasheet_move_columns (ds, pos, new_pos, cnt);
-
- for (i = 0; i < row_cnt; i++)
- move_range (&data[i], column_cnt, sizeof data[i][0],
- pos, new_pos, cnt);
-
- check_datasheet (mc, ds, data, row_cnt, column_cnt);
- }
-
- /* Insert all possible numbers of rows in all possible
- positions. */
- for (pos = 0; pos <= row_cnt; pos++)
- for (cnt = 0; cnt <= params->max_rows - row_cnt; cnt++)
- if (mc_include_state (mc))
- {
- struct datasheet *ds;
- struct ccase c[MAX_ROWS];
- size_t i, j;
-
- clone_model (ods, odata, &ds, data);
- mc_name_operation (mc, "insert %zu rows at %zu", cnt, pos);
-
- for (i = 0; i < cnt; i++)
- {
- case_create (&c[i], column_cnt);
- for (j = 0; j < column_cnt; j++)
- case_data_rw_idx (&c[i], j)->f = params->next_value++;
- }
-
- insert_range (data, row_cnt, sizeof data[pos], pos, cnt);
- for (i = 0; i < cnt; i++)
- for (j = 0; j < column_cnt; j++)
- data[i + pos][j] = case_num_idx (&c[i], j);
-
- if (!datasheet_insert_rows (ds, pos, c, cnt))
- mc_error (mc, "datasheet_insert_rows failed");
-
- check_datasheet (mc, ds, data, row_cnt + cnt, column_cnt);
- }
-
- /* Delete all possible numbers of rows from all possible
- positions. */
- for (pos = 0; pos < row_cnt; pos++)
- for (cnt = 0; cnt < row_cnt - pos; cnt++)
- if (mc_include_state (mc))
- {
- struct datasheet *ds;
-
- clone_model (ods, odata, &ds, data);
- mc_name_operation (mc, "delete %zu rows at %zu", cnt, pos);
-
- datasheet_delete_rows (ds, pos, cnt);
-
- remove_range (&data[0], row_cnt, sizeof data[0], pos, cnt);
-
- check_datasheet (mc, ds, data, row_cnt - cnt, column_cnt);
- }
-
- /* Move all possible numbers of rows from all possible existing
- positions to all possible new positions. */
- for (pos = 0; pos < row_cnt; pos++)
- for (cnt = 0; cnt < row_cnt - pos; cnt++)
- for (new_pos = 0; new_pos < row_cnt - cnt; new_pos++)
- if (mc_include_state (mc))
- {
- struct datasheet *ds;
-
- clone_model (ods, odata, &ds, data);
- mc_name_operation (mc, "move %zu rows from %zu to %zu",
- cnt, pos, new_pos);
-
- datasheet_move_rows (ds, pos, new_pos, cnt);
-
- move_range (&data[0], row_cnt, sizeof data[0],
- pos, new_pos, cnt);
-
- check_datasheet (mc, ds, data, row_cnt, column_cnt);
- }
-}
-
-/* "destroy" function for struct mc_class. */
-static void
-datasheet_mc_destroy (const struct mc *mc UNUSED, void *ds_)
-{
- struct datasheet *ds = ds_;
- datasheet_destroy (ds);
-}
-
-/* Executes the model checker on the datasheet test driver with
- the given OPTIONS and passing in the given PARAMS, which must
- point to a modifiable "struct datasheet_test_params". If any
- value in PARAMS is out of range, it will be adjusted into the
- valid range before running the test.
-
- Returns the results of the model checking run. */
-struct mc_results *
-datasheet_test (struct mc_options *options, void *params_)
-{
- struct datasheet_test_params *params = params_;
- static const struct mc_class datasheet_mc_class =
- {
- datasheet_mc_init,
- datasheet_mc_mutate,
- datasheet_mc_destroy,
- };
-
- params->next_value = 1;
- params->max_rows = MIN (params->max_rows, MAX_ROWS);
- params->max_cols = MIN (params->max_cols, MAX_COLS);
- params->backing_rows = MIN (params->backing_rows, params->max_rows);
- params->backing_cols = MIN (params->backing_cols, params->max_cols);
-
- mc_options_set_aux (options, params);
- return mc_run (&datasheet_mc_class, options);