-/* 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 <string.h>
#include <sys/time.h>
+#include <libpspp/argv-parser.h>
#include <libpspp/bit-vector.h>
#include <libpspp/compiler.h>
#include <libpspp/deque.h>
+#include <libpspp/misc.h>
#include <libpspp/str.h>
-#include <math/moments.h>
#include "error.h"
#include "minmax.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)
+bool
+mc_progress_dots (struct mc *mc)
{
if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
putc ('.', stderr);
return true;
}
+/* Progress function that prints a one-line summary of the
+ current state on stderr. */
+bool
+mc_progress_fancy (struct mc *mc)
+{
+ const struct mc_results *results = mc_get_results (mc);
+ if (mc_results_get_stop_reason (results) == MC_CONTINUING)
+ fprintf (stderr, "Processed %d unique states, max depth %d, "
+ "dropped %d duplicates...\r",
+ mc_results_get_unique_state_count (results),
+ mc_results_get_max_depth_reached (results),
+ mc_results_get_duplicate_dropped_states (results));
+ else
+ putc ('\n', stderr);
+ return true;
+}
+
+/* Progress function that displays a detailed summary of the
+ current state on stderr. */
+bool
+mc_progress_verbose (struct mc *mc)
+{
+ const struct mc_results *results = mc_get_results (mc);
+
+ /* VT100 clear screen and home cursor. */
+ fprintf (stderr, "\033[H\033[2J");
+
+ if (mc_results_get_stop_reason (results) == MC_CONTINUING)
+ mc_results_print (results, stderr);
+
+ return true;
+}
+
/* 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;
options->failure_verbosity = 2;
options->output_file = stdout;
options->progress_usec = 250000;
- options->progress_func = default_progress;
+ options->progress_func = mc_progress_dots;
options->aux = NULL;
/* 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
+/* Options command-line parser. */
+
+enum
+ {
+ /* Search strategies. */
+ OPT_STRATEGY,
+ OPT_PATH,
+ OPT_MAX_DEPTH,
+ OPT_HASH_BITS,
+ OPT_SEED,
+
+ /* Queuing. */
+ OPT_QUEUE_LIMIT,
+ OPT_QUEUE_DROP,
+
+ /* Stop conditions. */
+ OPT_MAX_STATES,
+ OPT_MAX_ERRORS,
+ OPT_TIME_LIMIT,
+
+ /* User interface. */
+ OPT_PROGRESS,
+ OPT_VERBOSITY,
+ OPT_FAILURE_VERBOSITY,
+ };
+
+static const struct argv_option mc_argv_options[] =
+ {
+ {"strategy", 0, required_argument, OPT_STRATEGY},
+ {"max-depth", 0, required_argument, OPT_MAX_DEPTH},
+ {"hash-bits", 0, required_argument, OPT_HASH_BITS},
+ {"path", 0, required_argument, OPT_PATH},
+ {"queue-limit", 0, required_argument, OPT_QUEUE_LIMIT},
+ {"queue-drop", 0, required_argument, OPT_QUEUE_DROP},
+ {"seed", 0, required_argument, OPT_SEED},
+ {"max-states", 0, required_argument, OPT_MAX_STATES},
+ {"max-errors", 0, required_argument, OPT_MAX_ERRORS},
+ {"time-limit", 0, required_argument, OPT_TIME_LIMIT},
+ {"progress", 0, required_argument, OPT_PROGRESS},
+ {"verbosity", 0, required_argument, OPT_VERBOSITY},
+ {"failure-verbosity", 0, required_argument, OPT_FAILURE_VERBOSITY},
+ };
+enum { N_MC_ARGV_OPTIONS = sizeof mc_argv_options / sizeof *mc_argv_options };
+
+/* Called by argv_parser_run to indicate that option ID has been
+ parsed. */
+static void
+mc_parser_option_callback (int id, void *mc_options_)
+{
+ struct mc_options *options = mc_options_;
+ switch (id)
+ {
+ case OPT_STRATEGY:
+ if (mc_options_get_strategy (options) == MC_PATH)
+ error (1, 0, "--strategy and --path are mutually exclusive");
+
+ if (!strcmp (optarg, "broad"))
+ mc_options_set_strategy (options, MC_BROAD);
+ else if (!strcmp (optarg, "deep"))
+ mc_options_set_strategy (options, MC_DEEP);
+ else if (!strcmp (optarg, "random"))
+ mc_options_set_strategy (options, MC_RANDOM);
+ else
+ error (1, 0,
+ "strategy must be \"broad\", \"deep\", or \"random\"");
+ break;
+
+ case OPT_MAX_DEPTH:
+ mc_options_set_max_depth (options, atoi (optarg));
+ break;
+
+ case OPT_HASH_BITS:
+ {
+ int requested_hash_bits = atoi (optarg);
+ int hash_bits;
+ mc_options_set_hash_bits (options, requested_hash_bits);
+ hash_bits = mc_options_get_hash_bits (options);
+ if (hash_bits != requested_hash_bits)
+ error (0, 0, "hash bits adjusted to %d.", hash_bits);
+ }
+ break;
+
+ case OPT_PATH:
+ {
+ struct mc_path path;
+ char *op;
+
+ if (mc_options_get_strategy (options) != MC_BROAD)
+ error (1, 0, "--strategy and --path are mutually exclusive");
+
+ mc_path_init (&path);
+ for (op = strtok (optarg, ":, \t"); op != NULL;
+ op = strtok (NULL, ":, \t"))
+ mc_path_push (&path, atoi (op));
+ if (mc_path_get_length (&path) == 0)
+ error (1, 0, "at least one value must be specified on --path");
+ mc_options_set_follow_path (options, &path);
+ mc_path_destroy (&path);
+ }
+ break;
+
+ case OPT_QUEUE_LIMIT:
+ mc_options_set_queue_limit (options, atoi (optarg));
+ break;
+
+ case OPT_QUEUE_DROP:
+ if (!strcmp (optarg, "newest"))
+ mc_options_set_queue_limit_strategy (options, MC_DROP_NEWEST);
+ else if (!strcmp (optarg, "oldest"))
+ mc_options_set_queue_limit_strategy (options, MC_DROP_OLDEST);
+ else if (!strcmp (optarg, "random"))
+ mc_options_set_queue_limit_strategy (options, MC_DROP_RANDOM);
+ else
+ error (1, 0, "--queue-drop argument must be \"newest\", "
+ "\"oldest\", or \"random\"");
+ break;
+
+ case OPT_SEED:
+ mc_options_set_seed (options, atoi (optarg));
+ break;
+
+ case OPT_MAX_STATES:
+ mc_options_set_max_unique_states (options, atoi (optarg));
+ break;
+
+ case OPT_MAX_ERRORS:
+ mc_options_set_max_errors (options, atoi (optarg));
+ break;
+
+ case OPT_TIME_LIMIT:
+ mc_options_set_time_limit (options, atof (optarg));
+ break;
+
+ case OPT_PROGRESS:
+ if (!strcmp (optarg, "none"))
+ mc_options_set_progress_usec (options, 0);
+ else if (!strcmp (optarg, "dots"))
+ mc_options_set_progress_func (options, mc_progress_dots);
+ else if (!strcmp (optarg, "fancy"))
+ mc_options_set_progress_func (options, mc_progress_fancy);
+ else if (!strcmp (optarg, "verbose"))
+ mc_options_set_progress_func (options, mc_progress_verbose);
+ break;
+
+ case OPT_VERBOSITY:
+ mc_options_set_verbosity (options, atoi (optarg));
+ break;
+
+ case OPT_FAILURE_VERBOSITY:
+ mc_options_set_failure_verbosity (options, atoi (optarg));
+ break;
+
+ default:
+ NOT_REACHED ();
+ }
+}
+
+/* Adds the model checker command line options to the specified
+ command line PARSER. Model checker options parsed from the
+ command line will be applied to OPTIONS. */
+void
+mc_options_register_argv_parser (struct mc_options *options,
+ struct argv_parser *parser)
+{
+ argv_parser_add_options (parser, mc_argv_options, N_MC_ARGV_OPTIONS,
+ mc_parser_option_callback, options);
+}
+
+/* Prints a reference for the model checker command line options
+ to stdout. */
+void
+mc_options_usage (void)
+{
+ fputs (
+ "\nModel checker search algorithm options:\n"
+ " --strategy=STRATEGY Basic search strategy. One of:\n"
+ " broad: breadth-first search (default)\n"
+ " deep: depth-first search\n"
+ " random: randomly ordered search\n"
+ " --path=#[,#]... Fixes the exact search path to follow;\n"
+ " mutually exclusive with --strategy\n"
+ " --max-depth=MAX Limits search depth to MAX. The initial\n"
+ " states are at depth 1.\n"
+ " --hash-bits=BITS Use 2**BITS size hash table to avoid\n"
+ " duplicate states (0 will disable hashing)\n"
+ " --seed=SEED Sets the random number seed\n"
+ "\nModel checker queuing options:\n"
+ " --queue-limit=N Limit queue to N states (default: 10000)\n"
+ " --queue-drop=TYPE How to drop states when queue overflows:\n"
+ " newest: drop most recently added state\n"
+ " oldest: drop least recently added state\n"
+ " random (default): drop a random state\n"
+ "\nModel checker stop condition options:\n"
+ " --max-states=N Stop after visiting N unique states\n"
+ " --max-errors=N Stop after N errors (default: 1)\n"
+ " --time-limit=SECS Stop after SECS seconds\n"
+ "\nModel checker user interface options:\n"
+ " --progress=TYPE Show progress according to TYPE. One of:\n"
+ " none: Do not output progress message\n"
+ " dots (default): Output lines of dots\n"
+ " fancy: Show a few stats\n"
+ " verbose: Show all available stats\n"
+ " --verbosity=LEVEL Verbosity level before an error (default: 1)\n"
+ " --failure-verbosity=LEVEL Verbosity level for replaying failure\n"
+ " cases (default: 2)\n",
+ stdout);
+}
+\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. */
/* Depth statistics. */
int max_depth_reached; /* Max depth state examined. */
- struct moments1 *depth_moments; /* Enables reporting mean depth. */
+ unsigned long int depth_sum; /* Sum of depths. */
+ int n_depths; /* Number of depths in depth_sum. */
/* If error_count > 0, path to the last error reported. */
struct mc_path error_path;
/* 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;
- results->depth_moments = moments1_create (MOMENT_MEAN);
gettimeofday (&results->start, NULL);
return results;
}
/* 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);
free (results);
}
- 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);
- return mean != SYSMIS ? mean : 0.0;
+ return (results->n_depths == 0
+ ? 0
+ : (double) results->depth_sum / results->n_depths);
}
/* Returns the path traversed to obtain the last error
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);
}
+
+/* Prints a description of RESULTS to stream F. */
+void
+mc_results_print (const struct mc_results *results, FILE *f)
+{
+ enum mc_stop_reason reason = mc_results_get_stop_reason (results);
+
+ if (reason != MC_CONTINUING)
+ fprintf (f, "Stopped by: %s\n",
+ 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");
+ fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
+
+ fprintf (f, "Unique states checked: %d\n",
+ mc_results_get_unique_state_count (results));
+ fprintf (f, "Maximum depth reached: %d\n",
+ mc_results_get_max_depth_reached (results));
+ fprintf (f, "Mean depth reached: %.2f\n\n",
+ mc_results_get_mean_depth_reached (results));
+
+ fprintf (f, "Dropped duplicate states: %d\n",
+ mc_results_get_duplicate_dropped_states (results));
+ fprintf (f, "Dropped off-path states: %d\n",
+ mc_results_get_off_path_dropped_states (results));
+ fprintf (f, "Dropped too-deep states: %d\n",
+ mc_results_get_depth_dropped_states (results));
+ fprintf (f, "Dropped queue-overflow states: %d\n",
+ mc_results_get_queue_dropped_states (results));
+ fprintf (f, "Checked states still queued when stopped: %d\n",
+ mc_results_get_queued_unprocessed_states (results));
+ fprintf (f, "Maximum queue length reached: %d\n",
+ mc_results_get_max_queue_length (results));
+
+ if (reason != MC_CONTINUING)
+ fprintf (f, "\nRuntime: %.2f seconds\n",
+ mc_results_get_duration (results));
+}
\f
/* An active model checking run. */
struct mc
/* 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)
+ if (!mc->state_error && 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;
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);
+ mc->results->depth_sum += new->path.length;
+ mc->results->n_depths++;
- 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