[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Pspp-cvs] pspp/src data/datasheet.c language/tests/check-... [simpler-p
From: |
Ben Pfaff |
Subject: |
[Pspp-cvs] pspp/src data/datasheet.c language/tests/check-... [simpler-proc] |
Date: |
Sun, 15 Apr 2007 05:15:17 +0000 |
CVSROOT: /cvsroot/pspp
Module name: pspp
Branch: simpler-proc
Changes by: Ben Pfaff <blp> 07/04/15 05:15:17
Modified files:
src/data : datasheet.c
src/language/tests: check-model.q
src/libpspp : model-checker.c model-checker.h
Log message:
Start cleaning up model checker.
CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/pspp/src/data/datasheet.c?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.5&r2=1.1.2.6
http://cvs.savannah.gnu.org/viewcvs/pspp/src/language/tests/check-model.q?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.2&r2=1.1.2.3
http://cvs.savannah.gnu.org/viewcvs/pspp/src/libpspp/model-checker.c?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.2&r2=1.1.2.3
http://cvs.savannah.gnu.org/viewcvs/pspp/src/libpspp/model-checker.h?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.1&r2=1.1.2.2
Patches:
Index: data/datasheet.c
===================================================================
RCS file: /cvsroot/pspp/pspp/src/data/Attic/datasheet.c,v
retrieving revision 1.1.2.5
retrieving revision 1.1.2.6
diff -u -b -r1.1.2.5 -r1.1.2.6
--- data/datasheet.c 14 Apr 2007 23:01:54 -0000 1.1.2.5
+++ data/datasheet.c 15 Apr 2007 05:15:17 -0000 1.1.2.6
@@ -1070,8 +1070,6 @@
{
struct datasheet *ds;
struct range_map_node *r;
- size_t row_cnt, column_cnt;
- size_t row, column;
/* Clone ODS into DS. */
ds = *ds_ = xmalloc (sizeof *ds);
@@ -1090,11 +1088,7 @@
ds->column_min_alloc = ods->column_min_alloc;
/* Clone ODATA into DATA. */
- row_cnt = datasheet_get_row_cnt (ds);
- column_cnt = datasheet_get_column_cnt (ds);
- for (row = 0; row < row_cnt; row++)
- for (column = 0; column < column_cnt; column++)
- data[row][column] = odata[row][column];
+ memcpy (data, odata, MAX_ROWS * MAX_COLS * sizeof **data);
}
static void
@@ -1312,7 +1306,7 @@
datasheet_mc_destroy,
};
- params->next_value = 0;
+ 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);
Index: language/tests/check-model.q
===================================================================
RCS file: /cvsroot/pspp/pspp/src/language/tests/Attic/check-model.q,v
retrieving revision 1.1.2.2
retrieving revision 1.1.2.3
diff -u -b -r1.1.2.2 -r1.1.2.3
--- language/tests/check-model.q 14 Apr 2007 23:02:45 -0000 1.1.2.2
+++ language/tests/check-model.q 15 Apr 2007 05:15:17 -0000 1.1.2.3
@@ -39,6 +39,7 @@
search=strategy:broad/deep/random,
:mxd(n:max_depth),
:hash(n:hash_bits);
+ path=integer list;
queue=:limit(n:queue_limit,"%s>0"),
drop:newest/oldest/random;
seed=integer;
@@ -122,6 +123,30 @@
: cmd.strategy == CHM_DEEP ? MC_DEEP
: cmd.strategy == CHM_RANDOM ? MC_RANDOM
: -1);
+ if (cmd.sbc_path > 0)
+ {
+ if (cmd.sbc_search > 0)
+ msg (SW, _("PATH and SEARCH subcommands are mutually exclusive. "
+ "Ignoring PATH."));
+ else
+ {
+ struct subc_list_int *list = &cmd.il_path[0];
+ int count = subc_list_int_count (list);
+ if (count > 0)
+ {
+ struct mc_path path;
+ int i;
+
+ mc_path_init (&path);
+ for (i = 0; i < count; i++)
+ mc_path_push (&path, subc_list_int_at (list, i));
+ mc_options_set_follow_path (options, &path);
+ mc_path_destroy (&path);
+ }
+ else
+ msg (SW, _("At least one value must be specified on PATH."));
+ }
+ }
if (cmd.max_depth != NOT_LONG)
mc_options_set_max_depth (options, cmd.max_depth);
if (cmd.hash_bits != NOT_LONG)
@@ -196,6 +221,7 @@
reason == MC_SUCCESS ? "state space exhaustion"
: reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
: reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
+ : reason == MC_END_OF_PATH ? "reached end of specified path"
: reason == MC_TIMEOUT ? "reaching time limit"
: reason == MC_INTERRUPTED ? "user interruption"
: "unknown reason");
Index: libpspp/model-checker.c
===================================================================
RCS file: /cvsroot/pspp/pspp/src/libpspp/Attic/model-checker.c,v
retrieving revision 1.1.2.2
retrieving revision 1.1.2.3
diff -u -b -r1.1.2.2 -r1.1.2.3
--- libpspp/model-checker.c 14 Apr 2007 23:03:44 -0000 1.1.2.2
+++ libpspp/model-checker.c 15 Apr 2007 05:15:17 -0000 1.1.2.3
@@ -38,6 +38,76 @@
#include "minmax.h"
#include "xalloc.h"
+void
+mc_path_init (struct mc_path *path)
+{
+ path->states = NULL;
+ path->length = 0;
+ path->capacity = 0;
+}
+
+void
+mc_path_copy (struct mc_path *new, const struct mc_path *old)
+{
+ if (old->length > new->capacity)
+ {
+ new->capacity = old->length + 1;
+ free (new->states);
+ new->states = xnmalloc (new->capacity, sizeof *new->states);
+ }
+ new->length = old->length;
+ memcpy (new->states, old->states, old->length * sizeof *new->states);
+}
+
+void
+mc_path_push (struct mc_path *new, int new_state)
+{
+ if (new->length >= new->capacity)
+ new->states = xnrealloc (new->states,
+ ++new->capacity, sizeof *new->states);
+ new->states[new->length++] = new_state;
+}
+
+void
+mc_path_pop (struct mc_path *path)
+{
+ assert (path->length > 0);
+ path->length--;
+}
+
+void
+mc_path_destroy (struct mc_path *path)
+{
+ free (path->states);
+ path->states = NULL;
+}
+
+int
+mc_path_get_state (const struct mc_path *path, size_t index)
+{
+ assert (index < path->length);
+ return path->states[index];
+}
+
+size_t
+mc_path_get_length (const struct mc_path *path)
+{
+ return path->length;
+}
+
+static void
+mc_path_to_string (const struct mc_path *path, struct string *string)
+{
+ size_t i;
+
+ for (i = 0; i < mc_path_get_length (path); i++)
+ {
+ if (i > 0)
+ ds_put_char (string, ' ');
+ ds_put_format (string, "%d", mc_path_get_state (path, i));
+ }
+}
+
/* Search options. */
struct mc_options
{
@@ -45,6 +115,7 @@
int max_depth;
int hash_bits;
unsigned int seed;
+ struct mc_path follow_path;
int queue_limit;
enum mc_queue_limit_strategy queue_limit_strategy;
@@ -88,6 +159,7 @@
options->max_depth = INT_MAX;
options->hash_bits = 20;
options->seed = 0;
+ mc_path_init (&options->follow_path);
options->queue_limit = 10000;
options->queue_limit_strategy = MC_DROP_RANDOM;
@@ -116,6 +188,7 @@
void
mc_options_destroy (struct mc_options *options)
{
+ mc_path_destroy (&options->follow_path);
free (options);
}
@@ -171,6 +244,22 @@
options->hash_bits = MIN (hash_bits, 31);
}
+const struct mc_path *
+mc_options_get_follow_path (const struct mc_options *options)
+{
+ assert (options->strategy == MC_PATH);
+ return &options->follow_path;
+}
+
+void
+mc_options_set_follow_path (struct mc_options *options,
+ const struct mc_path *follow_path)
+{
+ assert (mc_path_get_length (follow_path) > 0);
+ options->strategy = MC_PATH;
+ mc_path_copy (&options->follow_path, follow_path);
+}
+
int
mc_options_get_queue_limit (const struct mc_options *options)
{
@@ -331,8 +420,7 @@
int max_depth_reached;
struct moments1 *depth_moments;
- int *error_path;
- size_t error_path_len;
+ struct mc_path error_path;
int duplicate_dropped_states;
int off_path_dropped_states;
@@ -360,7 +448,7 @@
if (results != NULL)
{
moments1_destroy (results->depth_moments);
- free (results->error_path);
+ mc_path_destroy (&results->error_path);
free (results);
}
}
@@ -397,22 +485,10 @@
return mean != SYSMIS ? mean : 0.0;
}
-bool
-mc_results_get_last_error_path (const struct mc_results *results,
- const int **path, size_t *path_len)
+const struct mc_path *
+mc_results_get_error_path (const struct mc_results *results)
{
- if (results->error_count > 0)
- {
- *path = results->error_path;
- *path_len = results->error_path_len;
- return true;
- }
- else
- {
- *path = NULL;
- *path_len = 0;
- return false;
- }
+ return results->error_count > 0 ? &results->error_path : NULL;
}
int
@@ -503,19 +579,20 @@
struct mc_options *options;
struct mc_results *results;
- unsigned char *seen_states;
+ unsigned char *hash;
struct deque state_deque;
struct mc_state **states;
+ size_t follow_path_idx;
struct mc_state *state;
+ struct mc_path substate_path;
+ struct string substate_path_string;
int substate;
bool named_state;
bool error_state;
- int include_substate;
-
unsigned int progress;
unsigned int next_progress;
unsigned int prev_progress;
@@ -528,17 +605,24 @@
struct mc_state
{
- int depth;
- int *sequence;
+ struct mc_path path;
void *data;
};
+static const char *
+substate_path_string (struct mc *mc)
+{
+ ds_clear (&mc->substate_path_string);
+ mc_path_to_string (&mc->substate_path, &mc->substate_path_string);
+ return ds_cstr (&mc->substate_path_string);
+}
+
static void
free_state (const struct mc_class *class, struct mc_state *state)
{
if (state->data != NULL)
class->destroy (state->data);
- free (state->sequence);
+ mc_path_destroy (&state->path);
free (state);
}
@@ -552,18 +636,10 @@
static struct mc_state *
make_child_state (const struct mc *mc, void *data)
{
- const struct mc_state *parent = mc->state;
struct mc_state *new = xmalloc (sizeof *new);
-
- new->depth = parent->depth + 1;
-
- new->sequence = xnmalloc (new->depth, sizeof *new->sequence);
- memcpy (new->sequence, parent->sequence,
- (new->depth - 1) * sizeof *parent->sequence);
- new->sequence[new->depth - 1] = mc->substate;
-
+ mc_path_init (&new->path);
+ mc_path_copy (&new->path, &mc->substate_path);
new->data = data;
-
return new;
}
@@ -580,9 +656,9 @@
{
size_t idx;
- if (new->depth > mc->results->max_depth_reached)
- mc->results->max_depth_reached = new->depth;
- moments1_add (mc->results->depth_moments, new->depth, 1.0);
+ if (new->path.length > mc->results->max_depth_reached)
+ mc->results->max_depth_reached = new->path.length;
+ moments1_add (mc->results->depth_moments, new->path.length, 1.0);
if (deque_count (&mc->state_deque) < mc->options->queue_limit)
{
@@ -608,6 +684,15 @@
else
idx = deque_push_front (&mc->state_deque);
break;
+ case MC_PATH:
+ assert (deque_is_empty (&mc->state_deque));
+ assert (mc->substate == mc_path_get_state (&mc->options->follow_path,
+ mc->state->path.length));
+ idx = deque_push_back (&mc->state_deque);
+ if (mc->state->path.length + 1
+ >= mc_path_get_length (&mc->options->follow_path))
+ stop (mc, MC_END_OF_PATH);
+ break;
default:
NOT_REACHED ();
}
@@ -618,6 +703,7 @@
{
/* Queue has reached limit, so replace an existing
state. */
+ assert (mc->options->strategy != MC_PATH);
assert (!deque_is_empty (&mc->state_deque));
mc->results->queue_dropped_states++;
switch (mc->options->queue_limit_strategy)
@@ -634,7 +720,8 @@
case MC_DEEP:
idx = deque_back (&mc->state_deque, 0);
break;
- case MC_DROP_RANDOM:
+ case MC_RANDOM:
+ case MC_PATH:
default:
NOT_REACHED ();
}
@@ -650,20 +737,6 @@
mc->states[idx] = new;
}
-static const char *
-state_path_string (const struct mc *mc)
-{
- static struct string s = DS_EMPTY_INITIALIZER;
- size_t i;
-
- ds_clear (&s);
- for (i = 0; i < mc->state->depth; i++)
- ds_put_format (&s, "%d ", mc->state->sequence[i]);
- ds_put_format (&s, "%d", mc->substate);
-
- return ds_cstr (&s);
-}
-
static void
do_error_state (struct mc *mc)
{
@@ -671,23 +744,21 @@
if (mc->results->error_count >= mc->options->max_errors)
stop (mc, MC_MAX_ERROR_COUNT);
+ mc_path_copy (&mc->results->error_path, &mc->substate_path);
+
if (mc->options->failure_verbosity > mc->options->verbosity)
{
struct mc_options *path_options;
- struct mc_state *state;
fprintf (mc->options->output_file, "[%s] retracing error path:\n",
- state_path_string (mc));
+ substate_path_string (mc));
path_options = mc_options_clone (mc->options);
mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
mc_options_set_failure_verbosity (path_options, 0);
+ mc_options_set_follow_path (path_options, &mc->substate_path);
- state = make_child_state (mc, NULL);
-
- mc_results_destroy (mc_follow_path (mc->class, path_options,
- state->sequence, state->depth));
+ mc_results_destroy (mc_run (mc->class, path_options));
- free_state (mc->class, state);
putc ('\n', mc->options->output_file);
}
}
@@ -698,16 +769,13 @@
if (mc->named_state)
fprintf (mc->options->output_file, " [%s] warning: duplicate call "
"to mc_name_state (missing call to mc_add_state?)\n",
- state_path_string (mc));
+ substate_path_string (mc));
mc->named_state = true;
if (mc->options->verbosity > 1)
{
-
- fprintf (mc->options->output_file, " [%s] ", state_path_string (mc));
-
+ fprintf (mc->options->output_file, " [%s] ", substate_path_string (mc));
vfprintf (mc->options->output_file, name, args);
-
putc ('\n', mc->options->output_file);
}
}
@@ -726,6 +794,9 @@
next_substate (struct mc *mc)
{
mc->substate++;
+ mc_path_pop (&mc->substate_path);
+ mc_path_push (&mc->substate_path, mc->substate);
+ mc->error_state = false;
mc->named_state = false;
if (++mc->progress >= mc->next_progress)
@@ -777,23 +848,35 @@
if (mc->options->hash_bits > 0)
{
hash &= (1u << mc->options->hash_bits) - 1;
- if (TEST_BIT (mc->seen_states, hash))
+ if (TEST_BIT (mc->hash, hash))
{
+ if (mc->options->verbosity > 2)
+ fprintf (mc->options->output_file,
+ " [%s] discard duplicate state\n",
+ substate_path_string (mc));
mc->results->duplicate_dropped_states++;
next_substate (mc);
return true;
}
- SET_BIT (mc->seen_states, hash);
+ SET_BIT (mc->hash, hash);
}
return false;
}
+static bool
+is_off_path (const struct mc *mc)
+{
+ return (mc->options->strategy == MC_PATH
+ && mc->substate != mc_path_get_state (&mc->options->follow_path,
+ mc->state->path.length));
+}
+
void
mc_add_state (struct mc *mc, void *data)
{
if (!mc->named_state)
fprintf (mc->options->output_file, " [%s] warning: unnamed state\n",
- state_path_string (mc));
+ substate_path_string (mc));
if (mc->results->stop_reason != MC_CONTINUING)
{
@@ -801,10 +884,9 @@
}
else if (mc->error_state)
do_error_state (mc);
- else if (mc->include_substate >= 0
- && mc->substate != mc->include_substate)
+ else if (is_off_path (mc))
mc->results->off_path_dropped_states++;
- else if (mc->state->depth + 1 > mc->options->max_depth)
+ else if (mc->state->path.length + 1 > mc->options->max_depth)
mc->results->depth_dropped_states++;
else
{
@@ -817,7 +899,6 @@
return;
}
- mc->error_state = false;
mc->class->destroy (data);
next_substate (mc);
}
@@ -834,13 +915,19 @@
init_mc (struct mc *mc, const struct mc_class *class,
struct mc_options *options)
{
- struct mc_state null_state = {0, NULL, NULL};
+ struct mc_state null_state = { { NULL, 0 }, NULL };
mc->class = class;
mc->options = options != NULL ? options : mc_options_create ();
check_options (mc->options);
+ if (mc->options->strategy == MC_PATH)
+ {
+ mc->options->max_depth = INT_MAX;
+ mc->options->hash_bits = 0;
+ }
+
if (mc->options->progress_usec == 0)
{
mc->options->progress_func = null_progress;
@@ -852,17 +939,18 @@
gettimeofday (&mc->results->start, NULL);
if (mc->options->hash_bits > 0)
- mc->seen_states = xcalloc (1, (1u << mc->options->hash_bits) / CHAR_BIT);
+ mc->hash = xcalloc (1, (1u << mc->options->hash_bits) / CHAR_BIT);
else
- mc->seen_states = NULL;
+ mc->hash = NULL;
mc->states = NULL;
deque_init_null (&mc->state_deque);
mc->substate = 0;
+ mc_path_init (&mc->substate_path);
+ mc_path_push (&mc->substate_path, mc->substate);
+ ds_init_empty (&mc->substate_path_string);
mc->state = &null_state;
- mc->include_substate = -1;
-
mc->named_state = false;
mc->error_state = false;
@@ -901,9 +989,11 @@
mc->options->progress_func (mc);
+ mc_path_destroy (&mc->substate_path);
+ ds_destroy (&mc->substate_path_string);
free (mc->options);
free (mc->states);
- free (mc->seen_states);
+ free (mc->hash);
}
static void
@@ -924,6 +1014,8 @@
{
mc.substate = 0;
mc.state = mc.states[deque_pop_front (&mc.state_deque)];
+ mc_path_copy (&mc.substate_path, &mc.state->path);
+ mc_path_push (&mc.substate_path, mc.substate);
class->mutate (&mc, mc.state->data);
free_state (class, mc.state);
periodic_mc (&mc);
@@ -933,39 +1025,6 @@
return mc.results;
}
-/* Should return "void *" reached by path? */
-struct mc_results *
-mc_follow_path (const struct mc_class *class, struct mc_options *options,
- int *path, size_t path_len)
-{
- struct mc mc;
- size_t i;
-
- init_mc (&mc, class, options);
- for (i = 1; i < path_len; i++)
- {
- if (deque_is_empty (&mc.state_deque))
- {
- fprintf (options->output_file,
- "No state found after %zu elements in path (out of %zu)\n",
- i, path_len);
- break;
- }
- assert (deque_count (&mc.state_deque) == 1);
-
- mc.substate = 0;
- mc.state = mc.states[deque_pop_front (&mc.state_deque)];
- mc.include_substate = path[i];
- class->mutate (&mc, mc.state->data);
- free_state (class, mc.state);
-
- periodic_mc (&mc);
- }
- finish_mc (&mc);
-
- return mc.results;
-}
-
void
mc_error (struct mc *mc, const char *message, ...)
{
@@ -976,7 +1035,8 @@
if (mc->options->verbosity > 1)
fputs (" ", mc->options->output_file);
- fprintf (mc->options->output_file, "[%s] error: ", state_path_string (mc));
+ fprintf (mc->options->output_file, "[%s] error: ",
+ substate_path_string (mc));
va_start (args, message);
vfprintf (mc->options->output_file, message, args);
va_end (args);
@@ -990,11 +1050,12 @@
{
if (mc->results->stop_reason != MC_CONTINUING)
return false;
- if (mc->include_substate >= 0 && mc->substate != mc->include_substate)
+ else if (is_off_path (mc))
{
- mc->substate++;
+ next_substate (mc);
return false;
}
+ else
return true;
}
Index: libpspp/model-checker.h
===================================================================
RCS file: /cvsroot/pspp/pspp/src/libpspp/Attic/model-checker.h,v
retrieving revision 1.1.2.1
retrieving revision 1.1.2.2
diff -u -b -r1.1.2.1 -r1.1.2.2
--- libpspp/model-checker.h 14 Apr 2007 05:04:23 -0000 1.1.2.1
+++ libpspp/model-checker.h 15 Apr 2007 05:15:17 -0000 1.1.2.2
@@ -36,6 +36,22 @@
void (*destroy) (void *);
};
+struct mc_path
+ {
+ int *states;
+ size_t length;
+ size_t capacity;
+ };
+
+void mc_path_init (struct mc_path *);
+void mc_path_copy (struct mc_path *, const struct mc_path *);
+void mc_path_push (struct mc_path *, int new_state);
+void mc_path_pop (struct mc_path *);
+void mc_path_destroy (struct mc_path *);
+
+int mc_path_get_state (const struct mc_path *, size_t index);
+size_t mc_path_get_length (const struct mc_path *);
+
struct mc_options *mc_options_create (void);
struct mc_options *mc_options_clone (const struct mc_options *);
void mc_options_destroy (struct mc_options *);
@@ -45,11 +61,13 @@
{
MC_BROAD, /* Breadth-first search. */
MC_DEEP, /* Depth-first search. */
- MC_RANDOM /* Randomly ordered search. */
+ MC_RANDOM, /* Randomly ordered search. */
+ MC_PATH /* Follow one explicit path. */
};
enum mc_strategy mc_options_get_strategy (const struct mc_options *);
void mc_options_set_strategy (struct mc_options *, enum mc_strategy);
+const struct mc_path *mc_options_get_follow_path (const struct mc_options *);
unsigned int mc_options_get_seed (const struct mc_options *);
void mc_options_set_seed (struct mc_options *, unsigned int seed);
int mc_options_get_max_depth (const struct mc_options *);
@@ -57,6 +75,8 @@
int mc_options_get_hash_bits (const struct mc_options *);
void mc_options_set_hash_bits (struct mc_options *, int hash_bits);
+void mc_options_set_follow_path (struct mc_options *, const struct mc_path *);
+
enum mc_queue_limit_strategy
{
MC_DROP_NEWEST,
@@ -102,6 +122,7 @@
MC_SUCCESS,
MC_MAX_UNIQUE_STATES,
MC_MAX_ERROR_COUNT,
+ MC_END_OF_PATH,
MC_TIMEOUT,
MC_INTERRUPTED
};
@@ -117,8 +138,7 @@
int mc_results_get_max_depth_reached (const struct mc_results *);
double mc_results_get_mean_depth_reached (const struct mc_results *);
-bool mc_results_get_last_error_path (const struct mc_results *,
- const int **path, size_t *path_len);
+const struct mc_path *mc_results_get_error_path (const struct mc_results *);
int mc_results_get_duplicate_dropped_states (const struct mc_results *);
int mc_results_get_off_path_dropped_states (const struct mc_results *);
@@ -132,9 +152,6 @@
double mc_results_get_duration (const struct mc_results *);
struct mc_results *mc_run (const struct mc_class *, struct mc_options *);
-struct mc_results *mc_follow_path (const struct mc_class *,
- struct mc_options *,
- int *path, size_t path_len);
bool mc_include_state (struct mc *);
bool mc_discard_dup_state (struct mc *, unsigned int hash);
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Pspp-cvs] pspp/src data/datasheet.c language/tests/check-... [simpler-proc],
Ben Pfaff <=