-/* PSPP - computes sample statistics.
- Copyright (C) 2007 Free Software Foundation, Inc.
+/* PSPP - a program for statistical analysis.
+ Copyright (C) 2007, 2009 Free Software Foundation, Inc.
- This program is free software; you can redistribute it and/or
- modify it under the terms of the GNU General Public License as
- published by the Free Software Foundation; either version 2 of the
- License, or (at your option) any later version.
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or
+ (at your option) any later version.
- This program is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- General Public License for more details.
+ This program is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ GNU General Public License for more details.
You should have received a copy of the GNU General Public License
- along with this program; if not, write to the Free Software
- Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
- 02110-1301, USA. */
+ along with this program. If not, see <http://www.gnu.org/licenses/>. */
#include <config.h>
#include <data/casereader-provider.h>
#include <data/casereader.h>
#include <data/casewriter.h>
+#include <data/lazy-casereader.h>
#include <data/sparse-cases.h>
#include <libpspp/array.h>
#include <libpspp/assertion.h>
-#include <libpspp/model-checker.h>
#include <libpspp/range-map.h>
#include <libpspp/range-set.h>
#include <libpspp/taint.h>
unsigned long int *start,
unsigned long int *width);
static void axis_make_available (struct axis *,
- unsigned long int start,
- unsigned long int width);
+ unsigned long int start,
+ unsigned long int width);
static unsigned long int axis_extend (struct axis *, unsigned long int width);
static unsigned long int axis_map (const struct axis *, unsigned long log_pos);
/* A datasheet. */
struct datasheet
- {
- /* Mappings from logical to physical columns/rows. */
- struct axis *columns;
- struct axis *rows;
-
- /* Mapping from physical columns to "source_info"s. */
- struct range_map sources;
-
- /* Minimum number of columns to put in a new source when we
- need new columns and none are free. We double it whenever
- we add a new source to keep the number of file descriptors
- needed by the datasheet to a minimum, reducing the
- likelihood of running out. */
- unsigned column_min_alloc;
-
- /* Indicates corrupted data in the datasheet. */
- struct taint *taint;
- };
+{
+ /* Mappings from logical to physical columns/rows. */
+ struct axis *columns;
+ struct axis *rows;
+
+ /* Mapping from physical columns to "source_info"s. */
+ struct range_map sources;
+
+ /* Minimum number of columns to put in a new source when we
+ need new columns and none are free. We double it whenever
+ we add a new source to keep the number of file descriptors
+ needed by the datasheet to a minimum, reducing the
+ likelihood of running out. */
+ unsigned column_min_alloc;
+
+ /* Indicates corrupted data in the datasheet. */
+ struct taint *taint;
+};
/* Maps from a range of physical columns to a source. */
struct source_info
- {
- struct range_map_node column_range;
- struct source *source;
- };
+{
+ struct range_map_node column_range;
+ struct source *source;
+};
/* Is this operation a read or a write? */
enum rw_op
static void free_source_info (struct datasheet *, struct source_info *);
static struct source_info *source_info_from_range_map (
- struct range_map_node *);
+ struct range_map_node *);
static bool rw_case (struct datasheet *ds, enum rw_op op,
casenumber lrow, size_t start_column, size_t column_cnt,
union value data[]);
/* Creates and returns a new datasheet.
If READER is nonnull, then the datasheet initially contains
- the contents of READER. READER become owned by the datasheet
- and the caller must not directly reference it again. */
+ the contents of READER. */
struct datasheet *
datasheet_create (struct casereader *reader)
{
if ( column_cnt > 0 )
{
unsigned long int column_start;
- column_start = axis_extend (ds->columns, column_cnt);
- axis_insert (ds->columns, 0, column_start, column_cnt);
- range_map_insert (&ds->sources, column_start, column_cnt,
- &si->column_range);
+ column_start = axis_extend (ds->columns, column_cnt);
+ axis_insert (ds->columns, 0, column_start, column_cnt);
+ range_map_insert (&ds->sources, column_start, column_cnt,
+ &si->column_range);
}
if ( row_cnt > 0 )
{
unsigned long int row_start;
- row_start = axis_extend (ds->rows, row_cnt);
- axis_insert (ds->rows, 0, row_start, row_cnt);
+ row_start = axis_extend (ds->rows, row_cnt);
+ axis_insert (ds->rows, 0, row_start, row_cnt);
}
}
{
size_t lcol;
+ assert ( start + cnt <= axis_get_size (ds->columns) );
+
/* Free up columns for reuse. */
for (lcol = start; lcol < start + cnt; lcol++)
{
axis_move (ds->columns, old_start, new_start, cnt);
}
-/* Retrieves the contents of the given ROW in datasheet DS into
- newly created case C. Returns true if successful, false on
- I/O error. */
-bool
-datasheet_get_row (const struct datasheet *ds, casenumber row, struct ccase *c)
+/* Retrieves and returns the contents of the given ROW in
+ datasheet DS. The caller owns the returned case and must
+ unref it when it is no longer needed. Returns a null pointer
+ on I/O error. */
+struct ccase *
+datasheet_get_row (const struct datasheet *ds, casenumber row)
{
size_t column_cnt = datasheet_get_column_cnt (ds);
- case_create (c, column_cnt);
+ struct ccase *c = case_create (column_cnt);
if (rw_case ((struct datasheet *) ds, OP_READ,
row, 0, column_cnt, case_data_all_rw (c)))
- return true;
+ return c;
else
{
- case_destroy (c);
- return false;
+ case_unref (c);
+ return NULL;
}
}
size_t column_cnt = datasheet_get_column_cnt (ds);
bool ok = rw_case (ds, OP_WRITE, row, 0, column_cnt,
(union value *) case_data_all (c));
- case_destroy (c);
+ case_unref (c);
return ok;
}
datasheet_get_value (const struct datasheet *ds, casenumber row, size_t column,
union value *value, int width)
{
+ assert ( row >= 0 );
return rw_case ((struct datasheet *) ds,
OP_READ, row, column, value_cnt_from_width (width), value);
}
(union value *) value);
}
-/* Inserts the CNT cases at C, which are destroyed, into
- datasheet DS just before row BEFORE. Returns true if
- successful, false on I/O error. On failure, datasheet DS is
- not modified. */
+/* Inserts the CNT cases at C into datasheet DS just before row
+ BEFORE. Returns true if successful, false on I/O error. On
+ failure, datasheet DS is not modified.
+
+ Regardless of success, this function unrefs all of the cases
+ in C. */
bool
datasheet_insert_rows (struct datasheet *ds,
- casenumber before, struct ccase c[],
+ casenumber before, struct ccase *c[],
casenumber cnt)
{
casenumber added = 0;
/* Initialize the new rows. */
for (i = 0; i < phy_cnt; i++)
- if (!datasheet_put_row (ds, before + i, &c[i]))
+ if (!datasheet_put_row (ds, before + i, c[i]))
{
while (++i < cnt)
- case_destroy (&c[i]);
+ case_unref (c[i]);
datasheet_delete_rows (ds, before - added, phy_cnt + added);
return false;
}
}
/* "read" function for the datasheet random casereader. */
-static bool
+static struct ccase *
datasheet_reader_read (struct casereader *reader UNUSED, void *ds_,
- casenumber case_idx, struct ccase *c)
+ casenumber case_idx)
{
struct datasheet *ds = ds_;
- if (case_idx >= datasheet_get_row_cnt (ds))
- return false;
- else if (datasheet_get_row (ds, case_idx, c))
- return true;
- else
+ if (case_idx < datasheet_get_row_cnt (ds))
{
- taint_set_taint (ds->taint);
- return false;
+ struct ccase *c = datasheet_get_row (ds, case_idx);
+ if (c == NULL)
+ taint_set_taint (ds->taint);
+ return c;
}
+ else
+ return NULL;
}
/* "destroy" function for the datasheet random casereader. */
axis_make_available, and axis_extend functions affect the set
of available ordinates. */
struct axis
- {
- struct tower log_to_phy; /* Map from logical to physical ordinates;
- contains "struct axis_group"s. */
- struct range_set *available; /* Set of unused, available ordinates. */
- unsigned long int phy_size; /* Current physical length of axis. */
- };
+{
+ struct tower log_to_phy; /* Map from logical to physical ordinates;
+ contains "struct axis_group"s. */
+ struct range_set *available; /* Set of unused, available ordinates. */
+ unsigned long int phy_size; /* Current physical length of axis. */
+};
/* A mapping from logical to physical ordinates. */
struct axis_group
- {
- struct tower_node logical; /* Range of logical ordinates. */
- unsigned long phy_start; /* First corresponding physical ordinate. */
- };
+{
+ struct tower_node logical; /* Range of logical ordinates. */
+ unsigned long phy_start; /* First corresponding physical ordinate. */
+};
static struct axis_group *axis_group_from_tower_node (struct tower_node *);
static struct tower_node *make_axis_group (unsigned long int phy_start);
for (node = tower_first (&old->log_to_phy); node != NULL;
node = tower_next (&old->log_to_phy, node))
{
- unsigned long int size = tower_node_get_height (node);
+ unsigned long int size = tower_node_get_size (node);
struct axis_group *group = tower_data (node, struct axis_group, logical);
tower_insert (&new->log_to_phy, size, make_axis_group (group->phy_start),
NULL);
{
struct axis_group *group = tower_data (tn, struct axis_group, logical);
unsigned long int phy_start = group->phy_start;
- unsigned long int size = tower_node_get_height (tn);
+ unsigned long int size = tower_node_get_size (tn);
md4_process_bytes (&phy_start, sizeof phy_start, ctx);
md4_process_bytes (&size, sizeof size, ctx);
if (where > group_start)
{
unsigned long int size_1 = where - group_start;
- unsigned long int size_2 = tower_node_get_height (group_node) - size_1;
+ unsigned long int size_2 = tower_node_get_size (group_node) - size_1;
struct tower_node *next = tower_next (&axis->log_to_phy, group_node);
struct tower_node *new = make_axis_group (group->phy_start + size_1);
tower_resize (&axis->log_to_phy, group_node, size_1);
if (next != NULL)
{
struct axis_group *next_group = axis_group_from_tower_node (next);
- unsigned long this_height = tower_node_get_height (node);
+ unsigned long this_height = tower_node_get_size (node);
if (group->phy_start + this_height == next_group->phy_start)
{
- unsigned long next_height = tower_node_get_height (next);
+ unsigned long next_height = tower_node_get_size (next);
tower_resize (t, node, this_height + next_height);
if (other_node != NULL && *other_node == next)
*other_node = tower_next (t, *other_node);
if (prev != NULL)
{
struct axis_group *prev_group = axis_group_from_tower_node (prev);
- unsigned long prev_height = tower_node_get_height (prev);
+ unsigned long prev_height = tower_node_get_size (prev);
if (prev_group->phy_start + prev_height == group->phy_start)
{
- unsigned long this_height = tower_node_get_height (node);
+ unsigned long this_height = tower_node_get_size (node);
group->phy_start = prev_group->phy_start;
tower_resize (t, node, this_height + prev_height);
if (other_node != NULL && *other_node == prev)
if (prev != NULL)
{
struct axis_group *prev_group = axis_group_from_tower_node (prev);
- unsigned long prev_height = tower_node_get_height (prev);
+ unsigned long prev_height = tower_node_get_size (prev);
struct axis_group *node_group = axis_group_from_tower_node (node);
assert (prev_group->phy_start + prev_height != node_group->phy_start);
}
\f
/* A source. */
struct source
- {
- size_t columns_used; /* Number of columns in use by client. */
- struct sparse_cases *data; /* Data at top level, atop the backing. */
- struct casereader *backing; /* Backing casereader (or null). */
- casenumber backing_rows; /* Number of rows in backing (if nonnull). */
- };
+{
+ size_t columns_used; /* Number of columns in use by client. */
+ struct sparse_cases *data; /* Data at top level, atop the backing. */
+ struct casereader *backing; /* Backing casereader (or null). */
+ casenumber backing_rows; /* Number of rows in backing (if nonnull). */
+};
/* Creates and returns an empty, unbacked source with COLUMN_CNT
columns and an initial "columns_used" of 0. */
return sparse_cases_read (source->data, row, column, values, value_cnt);
else
{
- struct ccase c;
- bool ok;
-
- assert (source->backing != NULL);
- ok = casereader_peek (source->backing, row, &c);
+ struct ccase *c = casereader_peek (source->backing, row);
+ bool ok = c != NULL;
if (ok)
{
- case_copy_out (&c, column, values, value_cnt);
- case_destroy (&c);
+ case_copy_out (c, column, values, value_cnt);
+ case_unref (c);
}
return ok;
}
ok = sparse_cases_write (source->data, row, column, values, value_cnt);
else
{
- struct ccase c;
+ struct ccase *c;
+
if (row < source->backing_rows)
- ok = casereader_peek (source->backing, row, &c);
+ c = case_unshare (casereader_peek (source->backing, row));
else
{
/* It's not one of the backed rows. Ideally, this
levels, so that we in fact usually write the full
contents of new, unbacked rows in multiple calls to
this function. Make this work. */
- case_create (&c, column_cnt);
- ok = true;
+ c = case_create (column_cnt);
}
+ ok = c != NULL;
+
if (ok)
{
- case_copy_in (&c, column, values, value_cnt);
+ case_copy_in (c, column, values, value_cnt);
ok = sparse_cases_write (source->data, row, 0,
- case_data_all (&c), column_cnt);
- case_destroy (&c);
+ case_data_all (c), column_cnt);
+ case_unref (c);
}
}
return ok;
#define MAX_ROWS 5
#define MAX_COLS 5
-/* Hashes the structure of datasheet DS and returns the hash.
- We use MD4 because it is much faster than MD5 or SHA-1 but its
- collision resistance is just as good. */
-static unsigned int
-hash_datasheet (const struct datasheet *ds)
-{
- unsigned int hash[DIV_RND_UP (20, sizeof (unsigned int))];
- struct md4_ctx ctx;
- struct range_map_node *r;
-
- md4_init_ctx (&ctx);
- axis_hash (ds->columns, &ctx);
- axis_hash (ds->rows, &ctx);
- for (r = range_map_first (&ds->sources); r != NULL;
- r = range_map_next (&ds->sources, r))
- {
- unsigned long int start = range_map_node_get_start (r);
- unsigned long int end = range_map_node_get_end (r);
- md4_process_bytes (&start, sizeof start, &ctx);
- md4_process_bytes (&end, sizeof end, &ctx);
- }
- md4_process_bytes (&ds->column_min_alloc, sizeof ds->column_min_alloc,
- &ctx);
- md4_finish_ctx (&ctx, hash);
- return hash[0];
-}
-
-/* Checks that datasheet DS contains has ROW_CNT rows, COLUMN_CNT
- columns, and the same contents as ARRAY, reporting any
- mismatches via mc_error. Then, adds DS to MC as a new state. */
-static void
-check_datasheet (struct mc *mc, struct datasheet *ds,
- double array[MAX_ROWS][MAX_COLS],
- size_t row_cnt, size_t column_cnt)
-{
- assert (row_cnt < MAX_ROWS);
- assert (column_cnt < MAX_COLS);
-
- /* If it is a duplicate hash, discard the state before checking
- its consistency, to save time. */
- if (mc_discard_dup_state (mc, hash_datasheet (ds)))
- {
- datasheet_destroy (ds);
- return;
- }
- if (row_cnt != datasheet_get_row_cnt (ds))
- mc_error (mc, "row count (%lu) does not match expected (%zu)",
- (unsigned long int) datasheet_get_row_cnt (ds), row_cnt);
- else if (column_cnt != datasheet_get_column_cnt (ds))
- mc_error (mc, "column count (%lu) does not match expected (%zu)",
- (unsigned long int) datasheet_get_column_cnt (ds), column_cnt);
- else
- {
- size_t row, col;
-
- for (row = 0; row < row_cnt; row++)
- for (col = 0; col < column_cnt; col++)
- {
- union value v;
- if (!datasheet_get_value (ds, row, col, &v, 1))
- NOT_REACHED ();
- if (v.f != array[row][col])
- mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: %g != %g",
- row, col, row_cnt, column_cnt, v.f, array[row][col]);
- }
- }
-
- mc_add_state (mc, ds);
-}
-
-/* Extracts the contents of DS into DATA. */
-static void
-extract_data (const struct datasheet *ds, double data[MAX_ROWS][MAX_COLS])
-{
- size_t column_cnt = datasheet_get_column_cnt (ds);
- size_t row_cnt = datasheet_get_row_cnt (ds);
- size_t row, col;
-
- assert (row_cnt < MAX_ROWS);
- assert (column_cnt < MAX_COLS);
- for (row = 0; row < row_cnt; row++)
- for (col = 0; col < column_cnt; col++)
- {
- union value v;
- if (!datasheet_get_value (ds, row, col, &v, 1))
- NOT_REACHED ();
- data[row][col] = v.f;
- }
-}
-
-/* Clones the structure and contents of ODS into *DS,
- and the contents of ODATA into DATA. */
-static void
-clone_model (const struct datasheet *ods, double odata[MAX_ROWS][MAX_COLS],
- struct datasheet **ds_, double data[MAX_ROWS][MAX_COLS])
+/* Clones the structure and contents of ODS into a new datasheet,
+ and returns the new datasheet. */
+struct datasheet *
+clone_datasheet (const struct datasheet *ods)
{
struct datasheet *ds;
struct range_map_node *r;
- /* Clone ODS into DS. */
- ds = *ds_ = xmalloc (sizeof *ds);
+ ds = xmalloc (sizeof *ds);
ds->columns = axis_clone (ods->columns);
ds->rows = axis_clone (ods->rows);
range_map_init (&ds->sources);
ds->column_min_alloc = ods->column_min_alloc;
ds->taint = taint_create ();
- /* Clone ODATA into DATA. */
- memcpy (data, odata, MAX_ROWS * MAX_COLS * sizeof **data);
+ return ds;
}
-/* "init" function for struct mc_class. */
-static void
-datasheet_mc_init (struct mc *mc)
+
+/* Hashes the structure of datasheet DS and returns the hash.
+ We use MD4 because it is much faster than MD5 or SHA-1 but its
+ collision resistance is just as good. */
+unsigned int
+hash_datasheet (const struct datasheet *ds)
{
- struct datasheet_test_params *params = mc_get_aux (mc);
- struct datasheet *ds;
+ unsigned int hash[DIV_RND_UP (20, sizeof (unsigned int))];
+ struct md4_ctx ctx;
+ struct range_map_node *r;
- if (params->backing_rows == 0 && params->backing_cols == 0)
- {
- /* Create unbacked datasheet. */
- ds = datasheet_create (NULL);
- mc_name_operation (mc, "empty datasheet");
- check_datasheet (mc, ds, NULL, 0, 0);
- }
- else
+ md4_init_ctx (&ctx);
+ axis_hash (ds->columns, &ctx);
+ axis_hash (ds->rows, &ctx);
+ for (r = range_map_first (&ds->sources); r != NULL;
+ r = range_map_next (&ds->sources, r))
{
- /* Create datasheet with backing. */
- struct casewriter *writer;
- struct casereader *reader;
- double data[MAX_ROWS][MAX_COLS];
- int row;
-
- assert (params->backing_rows > 0 && params->backing_rows <= MAX_ROWS);
- assert (params->backing_cols > 0 && params->backing_cols <= MAX_COLS);
-
- writer = mem_writer_create (params->backing_cols);
- for (row = 0; row < params->backing_rows; row++)
- {
- struct ccase c;
- int col;
-
- case_create (&c, params->backing_cols);
- for (col = 0; col < params->backing_cols; col++)
- {
- double value = params->next_value++;
- data[row][col] = value;
- case_data_rw_idx (&c, col)->f = value;
- }
- casewriter_write (writer, &c);
- }
- reader = casewriter_make_reader (writer);
- assert (reader != NULL);
-
- ds = datasheet_create (reader);
- mc_name_operation (mc, "datasheet with (%d,%d) backing",
- params->backing_rows, params->backing_cols);
- check_datasheet (mc, ds, data,
- params->backing_rows, params->backing_cols);
+ unsigned long int start = range_map_node_get_start (r);
+ unsigned long int end = range_map_node_get_end (r);
+ md4_process_bytes (&start, sizeof start, &ctx);
+ md4_process_bytes (&end, sizeof end, &ctx);
}
+ md4_process_bytes (&ds->column_min_alloc, sizeof ds->column_min_alloc,
+ &ctx);
+ md4_finish_ctx (&ctx, hash);
+ return hash[0];
}
-/* "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);
-}