-/* PSPP - computes sample statistics.
+/* PSPP - a program for statistical analysis.
Copyright (C) 2007 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 <string.h>
#include <sys/time.h>
+#include <data/val-type.h>
#include <libpspp/bit-vector.h>
#include <libpspp/compiler.h>
#include <libpspp/deque.h>
\f
/* Initializes PATH as an empty path. */
void
-mc_path_init (struct mc_path *path)
+mc_path_init (struct mc_path *path)
{
path->ops = NULL;
path->length = 0;
/* Copies the contents of OLD into NEW. */
void
-mc_path_copy (struct mc_path *new, const struct mc_path *old)
+mc_path_copy (struct mc_path *new, const struct mc_path *old)
{
- if (old->length > new->capacity)
+ if (old->length > new->capacity)
{
new->capacity = old->length;
free (new->ops);
/* Adds OP to the end of PATH. */
void
-mc_path_push (struct mc_path *path, int op)
+mc_path_push (struct mc_path *path, int op)
{
- if (path->length >= path->capacity)
+ if (path->length >= path->capacity)
path->ops = xnrealloc (path->ops, ++path->capacity, sizeof *path->ops);
path->ops[path->length++] = op;
}
/* Removes and returns the operation at the end of PATH. */
int
-mc_path_pop (struct mc_path *path)
+mc_path_pop (struct mc_path *path)
{
int back = mc_path_back (path);
path->length--;
/* Returns the operation at the end of PATH. */
int
-mc_path_back (const struct mc_path *path)
+mc_path_back (const struct mc_path *path)
{
assert (path->length > 0);
return path->ops[path->length - 1];
/* Destroys PATH. */
void
-mc_path_destroy (struct mc_path *path)
+mc_path_destroy (struct mc_path *path)
{
free (path->ops);
path->ops = NULL;
/* Returns the operation in position INDEX in PATH.
INDEX must be less than the length of PATH. */
int
-mc_path_get_operation (const struct mc_path *path, size_t index)
+mc_path_get_operation (const struct mc_path *path, size_t index)
{
assert (index < path->length);
return path->ops[index];
/* Returns the number of operations in PATH. */
size_t
-mc_path_get_length (const struct mc_path *path)
+mc_path_get_length (const struct mc_path *path)
{
return path->length;
}
/* Appends the operations in PATH to STRING, separating each one
with a single space. */
void
-mc_path_to_string (const struct mc_path *path, struct string *string)
+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++)
+ 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_operation (path, i));
+ ds_put_format (string, "%d", mc_path_get_operation (path, i));
}
}
\f
/* Search options. */
-struct mc_options
+struct mc_options
{
/* Search strategy. */
enum mc_strategy strategy; /* Type of strategy. */
/* Queue configuration. */
int queue_limit; /* Maximum length of queue. */
enum mc_queue_limit_strategy queue_limit_strategy;
- /* How to choose state to drop
+ /* How to choose state to drop
from queue. */
/* Stop conditions. */
/* Default progress function. */
static bool
-default_progress (struct mc *mc)
+default_progress (struct mc *mc)
{
if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
putc ('.', stderr);
/* Do-nothing progress function. */
static bool
-null_progress (struct mc *mc UNUSED)
+null_progress (struct mc *mc UNUSED)
{
return true;
}
/* Creates and returns a set of options initialized to the
defaults. */
struct mc_options *
-mc_options_create (void)
+mc_options_create (void)
{
struct mc_options *options = xmalloc (sizeof *options);
options->hash_bits = 20;
options->seed = 0;
mc_path_init (&options->follow_path);
-
+
options->queue_limit = 10000;
options->queue_limit_strategy = MC_DROP_RANDOM;
/* Returns a copy of the given OPTIONS. */
struct mc_options *
-mc_options_clone (const struct mc_options *options)
+mc_options_clone (const struct mc_options *options)
{
return xmemdup (options, sizeof *options);
}
/* Destroys OPTIONS. */
void
-mc_options_destroy (struct mc_options *options)
+mc_options_destroy (struct mc_options *options)
{
mc_path_destroy (&options->follow_path);
free (options);
- MC_PATH: Explicit path. Applies an explicitly specified
sequence of operations. */
enum mc_strategy
-mc_options_get_strategy (const struct mc_options *options)
+mc_options_get_strategy (const struct mc_options *options)
{
return options->strategy;
}
/* Returns OPTION's random seed used by MC_RANDOM and
MC_DROP_RANDOM. */
unsigned int
-mc_options_get_seed (const struct mc_options *options)
+mc_options_get_seed (const struct mc_options *options)
{
return options->seed;
}
/* Set OPTION's random seed used by MC_RANDOM and MC_DROP_RANDOM
to SEED. */
void
-mc_options_set_seed (struct mc_options *options, unsigned int seed)
+mc_options_set_seed (struct mc_options *options, unsigned int seed)
{
options->seed = seed;
}
descend. The initial states are at depth 1, states produced
as their mutations are at depth 2, and so on. */
int
-mc_options_get_max_depth (const struct mc_options *options)
+mc_options_get_max_depth (const struct mc_options *options)
{
return options->max_depth;
}
to MAX_DEPTH. The initial states are at depth 1, states
produced as their mutations are at depth 2, and so on. */
void
-mc_options_set_max_depth (struct mc_options *options, int max_depth)
+mc_options_set_max_depth (struct mc_options *options, int max_depth)
{
options->max_depth = max_depth;
}
table of 2**(N+1) bits to have a 50% chance of seeing a hash
collision, 2**(N+2) bits to have a 25% chance, and so on. */
int
-mc_options_get_hash_bits (const struct mc_options *options)
+mc_options_get_hash_bits (const struct mc_options *options)
{
return options->hash_bits;
}
hashes. (This causes the model checker to never terminate in
many cases.) */
void
-mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
+mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
{
assert (hash_bits >= 0);
options->hash_bits = MIN (hash_bits, CHAR_BIT * sizeof (unsigned int) - 1);
/* Returns the path set in OPTIONS by mc_options_set_follow_path.
May be used only if the search strategy is MC_PATH. */
const struct mc_path *
-mc_options_get_follow_path (const struct mc_options *options)
+mc_options_get_follow_path (const struct mc_options *options)
{
assert (options->strategy == MC_PATH);
return &options->follow_path;
to be the explicit path specified in FOLLOW_PATH. */
void
mc_options_set_follow_path (struct mc_options *options,
- const struct mc_path *follow_path)
+ const struct mc_path *follow_path)
{
assert (mc_path_get_length (follow_path) > 0);
options->strategy = MC_PATH;
the maximum queue length during the run by calling
mc_results_get_max_queue_length. */
int
-mc_options_get_queue_limit (const struct mc_options *options)
+mc_options_get_queue_limit (const struct mc_options *options)
{
return options->queue_limit;
}
/* Sets the maximum number of queued states in OPTIONS to
QUEUE_LIMIT. */
void
-mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
+mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
{
assert (queue_limit > 0);
options->queue_limit = queue_limit;
selects the state to drop; you can control the seed passed
to srand using mc_options_set_seed. */
enum mc_queue_limit_strategy
-mc_options_get_queue_limit_strategy (const struct mc_options *options)
+mc_options_get_queue_limit_strategy (const struct mc_options *options)
{
return options->queue_limit_strategy;
}
mc_options_get_queue_limit). */
void
mc_options_set_queue_limit_strategy (struct mc_options *options,
- enum mc_queue_limit_strategy strategy)
+ enum mc_queue_limit_strategy strategy)
{
assert (strategy == MC_DROP_NEWEST
|| strategy == MC_DROP_OLDEST
model checker will examine before terminating. The default is
INT_MAX. */
int
-mc_options_get_max_unique_states (const struct mc_options *options)
+mc_options_get_max_unique_states (const struct mc_options *options)
{
return options->max_unique_states;
}
MAX_UNIQUE_STATE. */
void
mc_options_set_max_unique_states (struct mc_options *options,
- int max_unique_states)
+ int max_unique_states)
{
options->max_unique_states = max_unique_states;
}
the model checker to encounter before terminating. The
default is 1. */
int
-mc_options_get_max_errors (const struct mc_options *options)
+mc_options_get_max_errors (const struct mc_options *options)
{
return options->max_errors;
}
model checker to encounter before terminating to
MAX_ERRORS. */
void
-mc_options_set_max_errors (struct mc_options *options, int max_errors)
+mc_options_set_max_errors (struct mc_options *options, int max_errors)
{
options->max_errors = max_errors;
}
model checker to consume before terminating. The
default of 0.0 means that time consumption is unlimited. */
double
-mc_options_get_time_limit (const struct mc_options *options)
+mc_options_get_time_limit (const struct mc_options *options)
{
return options->time_limit;
}
TIME_LIMIT. A value of 0.0 means that time consumption is
unlimited; otherwise, the return value will be positive. */
void
-mc_options_set_time_limit (struct mc_options *options, double time_limit)
+mc_options_set_time_limit (struct mc_options *options, double time_limit)
{
assert (time_limit >= 0.0);
options->time_limit = time_limit;
levels less than 0 or greater than 3 are allowed but currently
have no additional effect. */
int
-mc_options_get_verbosity (const struct mc_options *options)
+mc_options_get_verbosity (const struct mc_options *options)
{
return options->verbosity;
}
/* Sets the level of verbosity for output messages specified
by OPTIONS to VERBOSITY. */
void
-mc_options_set_verbosity (struct mc_options *options, int verbosity)
+mc_options_set_verbosity (struct mc_options *options, int verbosity)
{
options->verbosity = verbosity;
}
an explicit, human-readable description of the sequence of
operations that caused the error. */
int
-mc_options_get_failure_verbosity (const struct mc_options *options)
+mc_options_get_failure_verbosity (const struct mc_options *options)
{
return options->failure_verbosity;
}
to FAILURE_VERBOSITY. */
void
mc_options_set_failure_verbosity (struct mc_options *options,
- int failure_verbosity)
+ int failure_verbosity)
{
options->failure_verbosity = failure_verbosity;
}
/* Returns the output file used for messages printed by the model
checker specified by OPTIONS. The default is stdout. */
FILE *
-mc_options_get_output_file (const struct mc_options *options)
+mc_options_get_output_file (const struct mc_options *options)
{
return options->output_file;
}
must do so. */
void
mc_options_set_output_file (struct mc_options *options,
- FILE *output_file)
+ FILE *output_file)
{
options->output_file = output_file;
}
250,000 (1/4 second). A value of 0 disables progress
reporting. */
int
-mc_options_get_progress_usec (const struct mc_options *options)
+mc_options_get_progress_usec (const struct mc_options *options)
{
return options->progress_usec;
}
function specified by OPTIONS to PROGRESS_USEC. A value of 0
disables progress reporting. */
void
-mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
+mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
{
assert (progress_usec >= 0);
options->progress_usec = progress_usec;
mc_results_get_stop_reason will return a different value. */
void
mc_options_set_progress_func (struct mc_options *options,
- mc_progress_func *progress_func)
+ mc_progress_func *progress_func)
{
assert (options->progress_func != NULL);
options->progress_func = progress_func;
client-specified functions in struct mc_class during a model
checking run using mc_get_aux. */
void *
-mc_options_get_aux (const struct mc_options *options)
+mc_options_get_aux (const struct mc_options *options)
{
return options->aux;
}
/* Sets the auxiliary data in OPTIONS to AUX. */
void
-mc_options_set_aux (struct mc_options *options, void *aux)
+mc_options_set_aux (struct mc_options *options, void *aux)
{
options->aux = aux;
}
\f
/* Results of a model checking run. */
-struct mc_results
+struct mc_results
{
/* Overall results. */
enum mc_stop_reason stop_reason; /* Why the run ended. */
/* Creates, initializes, and returns a new set of results. */
static struct mc_results *
-mc_results_create (void)
+mc_results_create (void)
{
struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
results->stop_reason = MC_CONTINUING;
/* Destroys RESULTS. */
void
-mc_results_destroy (struct mc_results *results)
+mc_results_destroy (struct mc_results *results)
{
- if (results != NULL)
+ if (results != NULL)
{
moments1_destroy (results->depth_moments);
mc_path_destroy (&results->error_path);
- MC_INTERRUPTED: The run completed because SIGINT was caught
(typically, due to the user typing Ctrl+C). */
enum mc_stop_reason
-mc_results_get_stop_reason (const struct mc_results *results)
+mc_results_get_stop_reason (const struct mc_results *results)
{
return results->stop_reason;
}
/* Returns the number of unique states checked specified by
RESULTS. */
int
-mc_results_get_unique_state_count (const struct mc_results *results)
+mc_results_get_unique_state_count (const struct mc_results *results)
{
return results->unique_state_count;
}
/* Returns the number of errors found specified by RESULTS. */
int
-mc_results_get_error_count (const struct mc_results *results)
+mc_results_get_error_count (const struct mc_results *results)
{
return results->error_count;
}
represented by RESULTS. The initial states are at depth 1,
their child states at depth 2, and so on. */
int
-mc_results_get_max_depth_reached (const struct mc_results *results)
+mc_results_get_max_depth_reached (const struct mc_results *results)
{
return results->max_depth_reached;
}
/* Returns the mean depth reached during the model checker run
represented by RESULTS. */
double
-mc_results_get_mean_depth_reached (const struct mc_results *results)
+mc_results_get_mean_depth_reached (const struct mc_results *results)
{
double mean;
moments1_calculate (results->depth_moments, NULL, &mean, NULL, NULL, NULL);
RESULTS. Returns a null pointer if the run did not report any
errors. */
const struct mc_path *
-mc_results_get_error_path (const struct mc_results *results)
+mc_results_get_error_path (const struct mc_results *results)
{
return results->error_count > 0 ? &results->error_path : NULL;
}
hash value) during the model checker run represented by
RESULTS. */
int
-mc_results_get_duplicate_dropped_states (const struct mc_results *results)
+mc_results_get_duplicate_dropped_states (const struct mc_results *results)
{
return results->duplicate_dropped_states;
}
indicates a missing call to mc_include_state in the
client-supplied mutation function. */
int
-mc_results_get_off_path_dropped_states (const struct mc_results *results)
+mc_results_get_off_path_dropped_states (const struct mc_results *results)
{
return results->off_path_dropped_states;
}
exceeded the maximum specified with mc_options_set_max_depth
during the model checker run represented by RESULTS. */
int
-mc_results_get_depth_dropped_states (const struct mc_results *results)
+mc_results_get_depth_dropped_states (const struct mc_results *results)
{
return results->depth_dropped_states;
}
queue overflow during the model checker run represented by
RESULTS. */
int
-mc_results_get_queue_dropped_states (const struct mc_results *results)
+mc_results_get_queue_dropped_states (const struct mc_results *results)
{
return results->queue_dropped_states;
}
states in the queue at the time that the checking run
stopped. */
int
-mc_results_get_queued_unprocessed_states (const struct mc_results *results)
+mc_results_get_queued_unprocessed_states (const struct mc_results *results)
{
return results->queued_unprocessed_states;
}
maximum queue length, then the queue (probably) overflowed
during the run; otherwise, it did not overflow. */
int
-mc_results_get_max_queue_length (const struct mc_results *results)
+mc_results_get_max_queue_length (const struct mc_results *results)
{
return results->max_queue_length;
}
/* Returns the time at which the model checker run represented by
RESULTS started. */
struct timeval
-mc_results_get_start (const struct mc_results *results)
+mc_results_get_start (const struct mc_results *results)
{
return results->start;
}
RESULTS ended. (This function may not be called while the run
is still ongoing.) */
struct timeval
-mc_results_get_end (const struct mc_results *results)
+mc_results_get_end (const struct mc_results *results)
{
assert (results->stop_reason != MC_CONTINUING);
return results->end;
/* Returns the number of seconds obtained by subtracting time Y
from time X. */
static double
-timeval_subtract (struct timeval x, struct timeval y)
+timeval_subtract (struct timeval x, struct timeval y)
{
/* From libc.info. */
double difference;
-
+
/* Perform the carry for the later subtraction by updating Y. */
if (x.tv_usec < y.tv_usec) {
int nsec = (y.tv_usec - x.tv_usec) / 1000000 + 1;
represented by RESULTS. (This function may not be called
while the run is still ongoing.) */
double
-mc_results_get_duration (const struct mc_results *results)
+mc_results_get_duration (const struct mc_results *results)
{
assert (results->stop_reason != MC_CONTINUING);
return timeval_subtract (results->end, results->start);
/* Information for handling and restoring SIGINT. */
bool interrupted; /* SIGINT received? */
bool *saved_interrupted_ptr; /* Saved value of interrupted_ptr. */
- sighandler_t saved_sigint; /* Saved SIGINT handler. */
+ void (*saved_sigint) (int); /* Saved SIGINT handler. */
};
/* A state in the queue. */
mc_options_set_aux on OPTIONS, which may be retrieved from the
CLASS functions using mc_get_aux. */
struct mc_results *
-mc_run (const struct mc_class *class, struct mc_options *options)
+mc_run (const struct mc_class *class, struct mc_options *options)
{
struct mc mc;
"mutate" function, according to the pattern explained in the
big comment at the top of model-checker.h. */
bool
-mc_include_state (struct mc *mc)
+mc_include_state (struct mc *mc)
{
if (mc->results->stop_reason != MC_CONTINUING)
return false;
else if (is_off_path (mc))
{
next_operation (mc);
- return false;
+ return false;
}
else
return true;
"mutate" function, according to the pattern explained in the
big comment at the top of model-checker.h. */
bool
-mc_discard_dup_state (struct mc *mc, unsigned int hash)
+mc_discard_dup_state (struct mc *mc, unsigned int hash)
{
if (mc->options->hash_bits > 0)
{
hash &= (1u << mc->options->hash_bits) - 1;
- if (TEST_BIT (mc->hash, hash))
+ if (TEST_BIT (mc->hash, hash))
{
if (mc->options->verbosity > 2)
fprintf (mc->options->output_file,
}
SET_BIT (mc->hash, hash);
}
- return false;
+ return false;
}
/* Names the current state NAME, which may contain
"mutate" function, according to the pattern explained in the
big comment at the top of model-checker.h. */
void
-mc_name_operation (struct mc *mc, const char *name, ...)
+mc_name_operation (struct mc *mc, const char *name, ...)
{
va_list args;
-
+
va_start (args, name);
mc_vname_operation (mc, name, args);
va_end (args);
"mutate" function, according to the pattern explained in the
big comment at the top of model-checker.h. */
void
-mc_vname_operation (struct mc *mc, const char *name, va_list args)
+mc_vname_operation (struct mc *mc, const char *name, va_list args)
{
- if (mc->state_named && mc->options->verbosity > 0)
+ if (mc->state_named && mc->options->verbosity > 0)
fprintf (mc->options->output_file, " [%s] warning: duplicate call "
"to mc_name_operation (missing call to mc_add_state?)\n",
path_string (mc));
mc->state_named = true;
- if (mc->options->verbosity > 1)
+ if (mc->options->verbosity > 1)
{
fprintf (mc->options->output_file, " [%s] ", path_string (mc));
vfprintf (mc->options->output_file, name, args);
"mutate" function, according to the pattern explained in the
big comment at the top of model-checker.h. */
void
-mc_error (struct mc *mc, const char *message, ...)
+mc_error (struct mc *mc, const char *message, ...)
{
va_list args;
"mutate" function, according to the pattern explained in the
big comment at the top of model-checker.h. */
void
-mc_add_state (struct mc *mc, void *data)
+mc_add_state (struct mc *mc, void *data)
{
if (!mc->state_named && mc->options->verbosity > 0)
fprintf (mc->options->output_file, " [%s] warning: unnamed state\n",
{
/* Nothing to do. */
}
- else if (mc->state_error)
+ else if (mc->state_error)
do_error_state (mc);
else if (is_off_path (mc))
mc->results->off_path_dropped_states++;
else if (mc->path.length + 1 > mc->options->max_depth)
mc->results->depth_dropped_states++;
- else
+ else
{
/* This is the common case. */
mc->results->unique_state_count++;
/* Returns the options that were passed to mc_run for model
checker MC. */
const struct mc_options *
-mc_get_options (const struct mc *mc)
+mc_get_options (const struct mc *mc)
{
return mc->options;
}
Not all of the results are meaningful before model checking
completes. */
const struct mc_results *
-mc_get_results (const struct mc *mc)
+mc_get_results (const struct mc *mc)
{
return mc->results;
}
/* Returns the auxiliary data set on the options passed to mc_run
with mc_options_set_aux. */
void *
-mc_get_aux (const struct mc *mc)
+mc_get_aux (const struct mc *mc)
{
return mc_options_get_aux (mc_get_options (mc));
}
\f
/* Expresses MC->path as a string and returns the string. */
static const char *
-path_string (struct mc *mc)
+path_string (struct mc *mc)
{
ds_clear (&mc->path_string);
mc_path_to_string (&mc->path, &mc->path_string);
/* Frees STATE, including client data. */
static void
-free_state (const struct mc *mc, struct mc_state *state)
+free_state (const struct mc *mc, struct mc_state *state)
{
mc->class->destroy (mc, state->data);
mc_path_destroy (&state->path);
/* Sets STOP_REASON as the reason that MC's processing stopped,
unless MC is already stopped. */
static void
-stop (struct mc *mc, enum mc_stop_reason stop_reason)
+stop (struct mc *mc, enum mc_stop_reason stop_reason)
{
if (mc->results->stop_reason == MC_CONTINUING)
mc->results->stop_reason = stop_reason;
/* Creates and returns a new state whose path is copied from
MC->path and whose data is specified by DATA. */
static struct mc_state *
-make_state (const struct mc *mc, void *data)
+make_state (const struct mc *mc, void *data)
{
struct mc_state *new = xmalloc (sizeof *new);
mc_path_init (&new->path);
/* Returns the index in MC->queue of a random element in the
queue. */
static size_t
-random_queue_index (struct mc *mc)
+random_queue_index (struct mc *mc)
{
assert (!deque_is_empty (&mc->queue_deque));
return deque_front (&mc->queue_deque,
/* Adds NEW to MC's state queue, dropping a state if necessary
due to overflow. */
static void
-enqueue_state (struct mc *mc, struct mc_state *new)
+enqueue_state (struct mc *mc, struct mc_state *new)
{
size_t idx;
mc->results->max_depth_reached = new->path.length;
moments1_add (mc->results->depth_moments, new->path.length, 1.0);
- if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
+ if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
{
/* Add new state to queue. */
if (deque_is_full (&mc->queue_deque))
mc->queue = deque_expand (&mc->queue_deque,
mc->queue, sizeof *mc->queue);
- switch (mc->options->strategy)
+ switch (mc->options->strategy)
{
case MC_BROAD:
idx = deque_push_back (&mc->queue_deque);
if (deque_count (&mc->queue_deque) > mc->results->max_queue_length)
mc->results->max_queue_length = deque_count (&mc->queue_deque);
}
- else
+ else
{
/* Queue has reached limit, so replace an existing
state. */
assert (mc->options->strategy != MC_PATH);
assert (!deque_is_empty (&mc->queue_deque));
mc->results->queue_dropped_states++;
- switch (mc->options->queue_limit_strategy)
+ switch (mc->options->queue_limit_strategy)
{
case MC_DROP_NEWEST:
free_state (mc, new);
return;
case MC_DROP_OLDEST:
- switch (mc->options->strategy)
+ switch (mc->options->strategy)
{
case MC_BROAD:
idx = deque_front (&mc->queue_deque, 0);
stop (mc, MC_MAX_ERROR_COUNT);
mc_path_copy (&mc->results->error_path, &mc->path);
-
+
if (mc->options->failure_verbosity > mc->options->verbosity)
{
struct mc_options *path_options;
/* Advances MC to start processing the operation following the
current one. */
static void
-next_operation (struct mc *mc)
+next_operation (struct mc *mc)
{
mc_path_push (&mc->path, mc_path_pop (&mc->path) + 1);
mc->state_error = false;
mc->state_named = false;
- if (++mc->progress >= mc->next_progress)
+ if (++mc->progress >= mc->next_progress)
{
struct timeval now;
double elapsed, delta;
if (mc->results->stop_reason == MC_CONTINUING
&& !mc->options->progress_func (mc))
- stop (mc, MC_INTERRUPTED);
+ stop (mc, MC_INTERRUPTED);
gettimeofday (&now, NULL);
double progress_sec = mc->options->progress_usec / 1000000.0;
delta = progress / elapsed * progress_sec;
}
- else
+ else
{
/* No measurable time at all elapsed during that amount
of progress. Try doubling the amount of progress
required. */
- delta = (mc->progress - mc->prev_progress) * 2;
+ delta = (mc->progress - mc->prev_progress) * 2;
}
if (delta > 0.0 && delta + mc->progress + 1.0 < UINT_MAX)
/* Returns true if we're tracing an explicit path but the current
operation produces a state off that path, false otherwise. */
static bool
-is_off_path (const struct mc *mc)
+is_off_path (const struct mc *mc)
{
return (mc->options->strategy == MC_PATH
&& (mc_path_back (&mc->path)
/* Handler for SIGINT. */
static void
-sigint_handler (int signum UNUSED)
+sigint_handler (int signum UNUSED)
{
/* Just mark the model checker as interrupted. */
*interrupted_ptr = true;
OPTIONS. OPTIONS may be null to use the default options. */
static void
init_mc (struct mc *mc, const struct mc_class *class,
- struct mc_options *options)
+ struct mc_options *options)
{
/* Validate and adjust OPTIONS. */
if (options == NULL)
options = mc_options_create ();
assert (options->queue_limit_strategy != MC_DROP_OLDEST
|| options->strategy != MC_RANDOM);
- if (options->strategy == MC_PATH)
+ if (options->strategy == MC_PATH)
{
options->max_depth = INT_MAX;
options->hash_bits = 0;
}
- if (options->progress_usec == 0)
+ if (options->progress_usec == 0)
{
options->progress_func = null_progress;
- if (options->time_limit > 0.0)
+ if (options->time_limit > 0.0)
options->progress_usec = 250000;
}
/* Complete the model checker run for MC. */
static void
-finish_mc (struct mc *mc)
+finish_mc (struct mc *mc)
{
/* Restore signal handlers. */
signal (SIGINT, mc->saved_sigint);
projects / pspp-builds.git / blobdiff