From 5060fdedfe17e843301ac0c738e12488af467378 Mon Sep 17 00:00:00 2001 From: Ben Pfaff Date: Mon, 23 Apr 2007 01:26:31 +0000 Subject: [PATCH] Implement model checker for testing purposes. Patch #5873. * automake.mk (src_libpspp_libpspp_a_SOURCES): Add model-checker.[ch]. Alphabetize. * model-checker.c: New file. * model-checker.h: New file. * automake.mk: Add check-model.[ch]. * check-model.h: New file. * check-model.q: New file. * Smake (GNULIB_MODULES): Add crypto/md4, fwriteerror, gettimeofday. --- ChangeLog | 9 + Smake | 3 + src/language/tests/ChangeLog | 12 + src/language/tests/automake.mk | 11 +- src/language/tests/check-model.h | 39 + src/language/tests/check-model.q | 271 ++++++ src/libpspp/ChangeLog | 13 + src/libpspp/automake.mk | 26 +- src/libpspp/model-checker.c | 1467 ++++++++++++++++++++++++++++++ src/libpspp/model-checker.h | 465 ++++++++++ 10 files changed, 2303 insertions(+), 13 deletions(-) create mode 100644 src/language/tests/check-model.h create mode 100644 src/language/tests/check-model.q create mode 100644 src/libpspp/model-checker.c create mode 100644 src/libpspp/model-checker.h diff --git a/ChangeLog b/ChangeLog index f3a9910f..da5339d5 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2007-04-22 Ben Pfaff + + Implement model checker for testing purposes. + + Patch #5873. + + * Smake (GNULIB_MODULES): Add crypto/md4, fwriteerror, + gettimeofday. + 2007-04-03 Ben Pfaff * configure.ac: Increment version to 0.4.3 due to snapshot posted diff --git a/Smake b/Smake index c716bae0..21583c6d 100644 --- a/Smake +++ b/Smake @@ -11,16 +11,19 @@ GNULIB_MODULES = \ byteswap \ c-ctype \ c-strtod \ + crypto/md4 \ dirname \ exit \ fpieee \ full-read \ full-write \ + fwriteerror \ gethostname \ getline \ getlogin_r \ getopt \ gettext-h \ + gettimeofday \ intprops \ inttostr \ linebreak \ diff --git a/src/language/tests/ChangeLog b/src/language/tests/ChangeLog index ba09d323..45f8a5ba 100644 --- a/src/language/tests/ChangeLog +++ b/src/language/tests/ChangeLog @@ -1,3 +1,15 @@ +2007-04-22 Ben Pfaff + + Implement model checker for testing purposes. + + Patch #5873. + + * automake.mk: Add check-model.[ch]. + + * check-model.h: New file. + + * check-model.q: New file. + Thu Oct 26 20:19:19 2006 Ben Pfaff * automake.mk: Add float-format.c. diff --git a/src/language/tests/automake.mk b/src/language/tests/automake.mk index 9b3f67a2..05d18a5a 100644 --- a/src/language/tests/automake.mk +++ b/src/language/tests/automake.mk @@ -1,7 +1,16 @@ ## Process this file with automake to produce Makefile.in -*- makefile -*- +language_tests_built_sources = \ + src/language/tests/check-model.c + language_tests_sources = \ src/language/tests/casefile-test.c \ + src/language/tests/check-model.h \ src/language/tests/moments-test.c \ src/language/tests/pool-test.c \ - src/language/tests/float-format.c + src/language/tests/float-format.c \ + $(language_tests_built_sources) + +all_q_sources += $(language_tests_built_sources:.c=.q) +EXTRA_DIST += $(language_tests_built_sources:.c=.q) +CLEANFILES += $(language_tests_built_sources) diff --git a/src/language/tests/check-model.h b/src/language/tests/check-model.h new file mode 100644 index 00000000..8cdddbe1 --- /dev/null +++ b/src/language/tests/check-model.h @@ -0,0 +1,39 @@ +/* PSPP - computes sample statistics. + 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 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. */ + +/* PSPP syntax interface to model checker. + + A model checker is a software testing tool. PSPP includes a + generic model checker in libpspp/model-checker.[ch]. This + module layers a PSPP syntax interface on top of the model + checker's options. */ + +#ifndef LANGUAGE_TESTS_CHECK_MODEL +#define LANGUAGE_TESTS_CHECK_MODEL 1 + +#include + +struct lexer; +struct mc_options; +struct mc_results; + +bool check_model (struct lexer *lexer, + struct mc_results *(*checker) (struct mc_options *, void *), + void *aux); + +#endif /* check-model.h */ diff --git a/src/language/tests/check-model.q b/src/language/tests/check-model.q new file mode 100644 index 00000000..77fba355 --- /dev/null +++ b/src/language/tests/check-model.q @@ -0,0 +1,271 @@ +/* PSPP - computes sample statistics. + 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 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. */ + +#include + +#include + +#include + +#include +#include + +#include "error.h" +#include "fwriteerror.h" + +#include "gettext.h" +#define _(msgid) gettext (msgid) +#define N_(msgid) msgid + +/* (headers) */ + +/* (specification) + "CHECK MODEL" (chm_): + 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; + stop=:states(n:max_unique_states,"%s>0"), + :errors(n:max_errors), + :timeout(d:time_limit,"%s>0"); + progress=progress:none/dots/fancy; + output=:verbosity(n:verbosity), + :errverbosity(n:err_verbosity), + :file(s:output_file). +*/ +/* (declarations) */ +/* (functions) */ + +static struct mc_options *parse_options (struct lexer *); +static void print_results (const struct mc_results *, FILE *); + +/* Parses a syntax description of model checker options from + LEXER and passes them, along with AUX, to the CHECKER + function, which must wrap a call to mc_run and return the + mc_results that it returned. This function then prints a + description of the mc_results to the output file. Returns + true if the model checker run found no errors, false + otherwise. */ +bool +check_model (struct lexer *lexer, + struct mc_results *(*checker) (struct mc_options *, void *aux), + void *aux) +{ + struct mc_options *options; + struct mc_results *results; + FILE *output_file; + bool ok; + + options = parse_options (lexer); + if (options == NULL) + return false; + output_file = mc_options_get_output_file (options); + + results = checker (options, aux); + + print_results (results, output_file); + + if (output_file != stdout && output_file != stderr) + { + if (fwriteerror (output_file) < 0) + { + /* We've already discarded the name of the output file. + Oh well. */ + error (0, errno, "error closing output file"); + } + } + + ok = mc_results_get_error_count (results) == 0; + mc_results_destroy (results); + + return ok; +} + +/* Fancy progress function for mc_options_set_progress_func. */ +static bool +fancy_progress (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; +} + +/* Parses options from LEXER and returns a corresponding + mc_options, or a null pointer if parsing fails. */ +static struct mc_options * +parse_options (struct lexer *lexer) +{ + struct cmd_check_model cmd; + struct mc_options *options; + + if (!parse_check_model (lexer, NULL, &cmd, NULL)) + return NULL; + + options = mc_options_create (); + if (cmd.strategy != -1) + mc_options_set_strategy (options, + cmd.strategy == CHM_BROAD ? MC_BROAD + : 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) + { + int hash_bits; + mc_options_set_hash_bits (options, cmd.hash_bits); + hash_bits = mc_options_get_hash_bits (options); + if (hash_bits != cmd.hash_bits) + msg (SW, _("Hash bits adjusted to %d."), hash_bits); + } + if (cmd.queue_limit != NOT_LONG) + mc_options_set_queue_limit (options, cmd.queue_limit); + if (cmd.drop != -1) + { + enum mc_queue_limit_strategy drop + = (cmd.drop == CHM_NEWEST ? MC_DROP_NEWEST + : cmd.drop == CHM_OLDEST ? MC_DROP_OLDEST + : cmd.drop == CHM_RANDOM ? MC_DROP_RANDOM + : -1); + mc_options_set_queue_limit_strategy (options, drop); + } + if (cmd.sbc_search > 0) + mc_options_set_seed (options, cmd.n_seed[0]); + if (cmd.max_unique_states != NOT_LONG) + mc_options_set_max_unique_states (options, cmd.max_unique_states); + if (cmd.max_errors != NOT_LONG) + mc_options_set_max_errors (options, cmd.max_errors); + if (cmd.time_limit != SYSMIS) + mc_options_set_time_limit (options, cmd.time_limit); + if (cmd.verbosity != NOT_LONG) + mc_options_set_verbosity (options, cmd.verbosity); + if (cmd.err_verbosity != NOT_LONG) + mc_options_set_failure_verbosity (options, cmd.err_verbosity); + if (cmd.progress != -1) + { + if (cmd.progress == CHM_NONE) + mc_options_set_progress_usec (options, 0); + else if (cmd.progress == CHM_DOTS) + { + /* Nothing to do: that's the default anyway. */ + } + else if (cmd.progress == CHM_FANCY) + mc_options_set_progress_func (options, fancy_progress); + } + if (cmd.output_file != NULL) + { + FILE *output_file = fopen (cmd.output_file, "w"); + if (output_file == NULL) + { + error (0, errno, _("error opening \"%s\" for writing"), + cmd.output_file); + free_check_model (&cmd); + mc_options_destroy (options); + return NULL; + } + mc_options_set_output_file (options, output_file); + } + + return options; +} + +/* Prints a description of RESULTS to stream F. */ +static void +print_results (const struct mc_results *results, FILE *f) +{ + enum mc_stop_reason reason = mc_results_get_stop_reason (results); + + fputs ("\n" + "MODEL CHECKING SUMMARY\n" + "----------------------\n\n", f); + + 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\n", + mc_results_get_max_queue_length (results)); + + fprintf (f, "Runtime: %.2f seconds\n", + mc_results_get_duration (results)); + + putc ('\n', f); +} + +/* + Local Variables: + mode: c + End: +*/ diff --git a/src/libpspp/ChangeLog b/src/libpspp/ChangeLog index ca06aea9..9c3692be 100644 --- a/src/libpspp/ChangeLog +++ b/src/libpspp/ChangeLog @@ -1,3 +1,16 @@ +2007-04-22 Ben Pfaff + + Implement model checker for testing purposes. + + Patch #5873. + + * automake.mk (src_libpspp_libpspp_a_SOURCES): Add + model-checker.[ch]. Alphabetize. + + * model-checker.c: New file. + + * model-checker.h: New file. + 2007-04-03 Ben Pfaff Apply patches #5828, #5837, #5841, #5843. diff --git a/src/libpspp/automake.mk b/src/libpspp/automake.mk index 265178d4..c626d61a 100644 --- a/src/libpspp/automake.mk +++ b/src/libpspp/automake.mk @@ -6,27 +6,25 @@ noinst_LIBRARIES += src/libpspp/libpspp.a src_libpspp_libpspp_a_SOURCES = \ src/libpspp/abt.c \ src/libpspp/abt.h \ + src/libpspp/alloc.c \ + src/libpspp/alloc.h \ src/libpspp/array.c \ src/libpspp/array.h \ src/libpspp/assertion.h \ - src/libpspp/alloc.c \ - src/libpspp/alloc.h \ src/libpspp/bit-vector.h \ src/libpspp/bt.c \ src/libpspp/bt.h \ - src/libpspp/legacy-encoding.c \ - src/libpspp/legacy-encoding.h \ + src/libpspp/compiler.h \ src/libpspp/copyleft.c \ src/libpspp/copyleft.h \ - src/libpspp/compiler.h \ src/libpspp/deque.c \ src/libpspp/deque.h \ src/libpspp/float-format.c \ src/libpspp/float-format.h \ src/libpspp/freaderror.c \ src/libpspp/freaderror.h \ - src/libpspp/getl.h \ src/libpspp/getl.c \ + src/libpspp/getl.h \ src/libpspp/hash.c \ src/libpspp/hash.h \ src/libpspp/heap.c \ @@ -35,16 +33,22 @@ src_libpspp_libpspp_a_SOURCES = \ src/libpspp/i18n.h \ src/libpspp/integer-format.c \ src/libpspp/integer-format.h \ - src/libpspp/msg-locator.c \ - src/libpspp/msg-locator.h \ + src/libpspp/legacy-encoding.c \ + src/libpspp/legacy-encoding.h \ src/libpspp/ll.c \ src/libpspp/ll.h \ src/libpspp/llx.c \ src/libpspp/llx.h \ src/libpspp/magic.c \ src/libpspp/magic.h \ + src/libpspp/message.c \ + src/libpspp/message.h \ src/libpspp/misc.c \ src/libpspp/misc.h \ + src/libpspp/model-checker.c \ + src/libpspp/model-checker.h \ + src/libpspp/msg-locator.c \ + src/libpspp/msg-locator.h \ src/libpspp/pool.c \ src/libpspp/pool.h \ src/libpspp/range-map.c \ @@ -53,14 +57,12 @@ src_libpspp_libpspp_a_SOURCES = \ src/libpspp/range-set.h \ src/libpspp/sparse-array.c \ src/libpspp/sparse-array.h \ - src/libpspp/syntax-gen.c \ - src/libpspp/syntax-gen.h \ - src/libpspp/message.c \ - src/libpspp/message.h \ src/libpspp/start-date.c \ src/libpspp/start-date.h \ src/libpspp/str.c \ src/libpspp/str.h \ + src/libpspp/syntax-gen.c \ + src/libpspp/syntax-gen.h \ src/libpspp/tower.c \ src/libpspp/tower.h \ src/libpspp/verbose-msg.c \ diff --git a/src/libpspp/model-checker.c b/src/libpspp/model-checker.c new file mode 100644 index 00000000..cd83b399 --- /dev/null +++ b/src/libpspp/model-checker.c @@ -0,0 +1,1467 @@ +/* PSPP - computes sample statistics. + 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 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. */ + +#include + +#include + +#include +#include +#include +#include +#include +#include +#include + +#include +#include +#include +#include +#include + +#include "error.h" +#include "minmax.h" +#include "xalloc.h" + +/* Initializes PATH as an empty path. */ +void +mc_path_init (struct mc_path *path) +{ + path->ops = NULL; + path->length = 0; + path->capacity = 0; +} + +/* Copies the contents of OLD into NEW. */ +void +mc_path_copy (struct mc_path *new, const struct mc_path *old) +{ + if (old->length > new->capacity) + { + new->capacity = old->length; + free (new->ops); + new->ops = xnmalloc (new->capacity, sizeof *new->ops); + } + new->length = old->length; + memcpy (new->ops, old->ops, old->length * sizeof *new->ops); +} + +/* Adds OP to the end of PATH. */ +void +mc_path_push (struct mc_path *path, int op) +{ + 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) +{ + int back = mc_path_back (path); + path->length--; + return back; +} + +/* Returns the operation at the end of PATH. */ +int +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) +{ + 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) +{ + 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) +{ + 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) +{ + 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_operation (path, i)); + } +} + +/* Search options. */ +struct mc_options + { + /* Search strategy. */ + enum mc_strategy strategy; /* Type of strategy. */ + int max_depth; /* Limit on depth (or INT_MAX). */ + int hash_bits; /* Number of bits to hash (or 0). */ + unsigned int seed; /* Random seed for MC_RANDOM + or MC_DROP_RANDOM. */ + struct mc_path follow_path; /* Path for MC_PATH. */ + + /* Queue configuration. */ + int queue_limit; /* Maximum length of queue. */ + enum mc_queue_limit_strategy queue_limit_strategy; + /* How to choose state to drop + from queue. */ + + /* Stop conditions. */ + int max_unique_states; /* Maximum unique states to process. */ + int max_errors; /* Maximum errors to detect. */ + double time_limit; /* Maximum time in seconds. */ + + /* Output configuration. */ + int verbosity; /* 0=low, 1=normal, 2+=high. */ + int failure_verbosity; /* If greater than verbosity, + verbosity of error replays. */ + FILE *output_file; /* File to receive output. */ + + /* How to report intermediate progress. */ + int progress_usec; /* Microseconds between reports. */ + mc_progress_func *progress_func; /* Function to call on each report. */ + + /* Client data. */ + void *aux; + }; + +/* Default progress function. */ +static bool +default_progress (struct mc *mc) +{ + if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING) + putc ('.', stderr); + else + putc ('\n', stderr); + return true; +} + +/* Do-nothing progress function. */ +static bool +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) +{ + struct mc_options *options = xmalloc (sizeof *options); + + options->strategy = MC_BROAD; + 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; + + options->max_unique_states = INT_MAX; + options->max_errors = 1; + options->time_limit = 0.0; + + options->verbosity = 1; + options->failure_verbosity = 2; + options->output_file = stdout; + options->progress_usec = 250000; + options->progress_func = default_progress; + + options->aux = NULL; + + return options; +} + +/* Returns a copy of the given OPTIONS. */ +struct mc_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_path_destroy (&options->follow_path); + free (options); +} + +/* Returns the search strategy used for OPTIONS. The choices + are: + + - MC_BROAD (the default): Breadth-first search. First tries + all the operations with depth 1, then those with depth 2, + then those with depth 3, and so on. + + This search algorithm finds the least number of operations + needed to trigger a given bug. + + - MC_DEEP: Depth-first search. Searches downward in the tree + of states as fast as possible. Good for finding bugs that + require long sequences of operations to trigger. + + - MC_RANDOM: Random-first search. Searches through the tree + of states in random order. The standard C library's rand + function selects the search path; you can control the seed + passed to srand using mc_options_set_seed. + + - MC_PATH: Explicit path. Applies an explicitly specified + sequence of operations. */ +enum mc_strategy +mc_options_get_strategy (const struct mc_options *options) +{ + return options->strategy; +} + +/* Sets the search strategy used for OPTIONS to STRATEGY. + + This function cannot be used to set MC_PATH as the search + strategy. Use mc_options_set_follow_path instead. */ +void +mc_options_set_strategy (struct mc_options *options, enum mc_strategy strategy) +{ + assert (strategy == MC_BROAD + || strategy == MC_DEEP + || strategy == MC_RANDOM); + options->strategy = 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) +{ + 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) +{ + options->seed = seed; +} + +/* Returns the maximum depth to which OPTIONS's search will + 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) +{ + return options->max_depth; +} + +/* Sets the maximum depth to which OPTIONS's search will descend + 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) +{ + options->max_depth = max_depth; +} + +/* Returns the base-2 log of the number of bits in OPTIONS's hash + table. The hash table is used for dropping states that are + probably duplicates: any state with a given hash value, as + will only be processed once. A return value of 0 indicates + that the model checker will not discard duplicate states based + on their hashes. + + The hash table is a power of 2 bits long, by default 2**20 + bits (128 kB). Depending on how many states you expect the + model checker to check, how much memory you're willing to let + the hash table take up, and how worried you are about missing + states due to hash collisions, you could make it larger or + smaller. + + The "birthday paradox" points to a reasonable way to size your + hash table. If you expect the model checker to check about + 2**N states, then, assuming a perfect hash, you need a hash + 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) +{ + return options->hash_bits; +} + +/* Sets the base-2 log of the number of bits in OPTIONS's hash + table to HASH_BITS. A HASH_BITS value of 0 requests that the + model checker not discard duplicate states based on their + 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) +{ + 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) +{ + assert (options->strategy == MC_PATH); + return &options->follow_path; +} + +/* Sets, in OPTIONS, the search algorithm to MC_PATH and the 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) +{ + assert (mc_path_get_length (follow_path) > 0); + options->strategy = MC_PATH; + mc_path_copy (&options->follow_path, follow_path); +} + +/* Returns the maximum number of queued states in OPTIONS. The + default value is 10,000. The primary reason to limit the + number of queued states is to conserve memory, so if you can + afford the memory and your model needs more room in the queue, + you can raise the limit. Conversely, if your models are large + or memory is constrained, you can reduce the limit. + + Following the execution of the model checker, you can find out + 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) +{ + 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) +{ + assert (queue_limit > 0); + options->queue_limit = queue_limit; +} + +/* Returns the queue limit strategy used by OPTIONS, that is, + when a new state must be inserted into a full state queue is + full, how the state to be dropped is chosen. The choices are: + + - MC_DROP_NEWEST: Drop the newest state; that is, do not + insert the new state into the queue at all. + + - MC_DROP_OLDEST: Drop the state that has been enqueued for + the longest. + + - MC_DROP_RANDOM (the default): Drop a randomly selected state + from the queue. The standard C library's rand function + 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) +{ + return options->queue_limit_strategy; +} + +/* Sets the queue limit strategy used by OPTIONS to STRATEGY. + + This setting has no effect unless the model being checked + causes the state queue to overflow (see + mc_options_get_queue_limit). */ +void +mc_options_set_queue_limit_strategy (struct mc_options *options, + enum mc_queue_limit_strategy strategy) +{ + assert (strategy == MC_DROP_NEWEST + || strategy == MC_DROP_OLDEST + || strategy == MC_DROP_RANDOM); + options->queue_limit_strategy = strategy; +} + +/* Returns OPTIONS's maximum number of unique states that the + model checker will examine before terminating. The default is + INT_MAX. */ +int +mc_options_get_max_unique_states (const struct mc_options *options) +{ + return options->max_unique_states; +} + +/* Sets OPTIONS's maximum number of unique states that the model + checker will examine before terminating to + MAX_UNIQUE_STATE. */ +void +mc_options_set_max_unique_states (struct mc_options *options, + int max_unique_states) +{ + options->max_unique_states = max_unique_states; +} + +/* Returns the maximum number of errors that OPTIONS will allow + the model checker to encounter before terminating. The + default is 1. */ +int +mc_options_get_max_errors (const struct mc_options *options) +{ + return options->max_errors; +} + +/* Sets the maximum number of errors that OPTIONS will allow the + model checker to encounter before terminating to + MAX_ERRORS. */ +void +mc_options_set_max_errors (struct mc_options *options, int max_errors) +{ + options->max_errors = max_errors; +} + +/* Returns the maximum amount of time, in seconds, that OPTIONS will allow the + 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) +{ + return options->time_limit; +} + +/* Sets the maximum amount of time, in seconds, that OPTIONS will + allow the model checker to consume before terminating to + 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) +{ + assert (time_limit >= 0.0); + options->time_limit = time_limit; +} + +/* Returns the level of verbosity for output messages specified + by OPTIONS. The default verbosity level is 1. + + A verbosity level of 0 inhibits all messages except for + errors; a verbosity level of 1 also allows warnings; a + verbosity level of 2 also causes a description of each state + added to be output; a verbosity level of 3 also causes a + description of each duplicate state to be output. Verbosity + 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) +{ + 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) +{ + options->verbosity = verbosity; +} + +/* Returns the level of verbosity for failures specified by + OPTIONS. The default failure verbosity level is 2. + + The failure verbosity level has an effect only when an error + is reported, and only when the failure verbosity level is + higher than the regular verbosity level. When this is the + case, the model checker replays the error path at the higher + verbosity level specified. This has the effect of outputting + 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) +{ + return options->failure_verbosity; +} + +/* Sets the level of verbosity for failures specified by OPTIONS + to FAILURE_VERBOSITY. */ +void +mc_options_set_failure_verbosity (struct mc_options *options, + 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) +{ + return options->output_file; +} + +/* Sets the output file used for messages printed by the model + checker specified by OPTIONS to OUTPUT_FILE. + + The model checker does not automatically close the specified + output file. If this is desired, the model checker's client + must do so. */ +void +mc_options_set_output_file (struct mc_options *options, + FILE *output_file) +{ + options->output_file = output_file; +} + +/* Returns the number of microseconds between calls to the + progress function specified by OPTIONS. The default is + 250,000 (1/4 second). A value of 0 disables progress + reporting. */ +int +mc_options_get_progress_usec (const struct mc_options *options) +{ + return options->progress_usec; +} + +/* Sets the number of microseconds between calls to the progress + 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) +{ + assert (progress_usec >= 0); + options->progress_usec = progress_usec; +} + +/* Returns the function called to report progress specified by + OPTIONS. The function used by default prints '.' to + stderr. */ +mc_progress_func * +mc_options_get_progress_func (const struct mc_options *options) +{ + return options->progress_func; +} + +/* Sets the function called to report progress specified by + OPTIONS to PROGRESS_FUNC. A non-null function must be + specified; to disable progress reporting, set the progress + reporting interval to 0. + + PROGRESS_FUNC will be called zero or more times while the + model checker's run is ongoing. For these calls to the + progress function, mc_results_get_stop_reason will return + MC_CONTINUING. It will also be called exactly once soon + before mc_run returns, in which case + 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) +{ + assert (options->progress_func != NULL); + options->progress_func = progress_func; +} + +/* Returns the auxiliary data set in OPTIONS by the client. The + default is a null pointer. + + This auxiliary data value can be retrieved by the + 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) +{ + return options->aux; +} + +/* Sets the auxiliary data in OPTIONS to AUX. */ +void +mc_options_set_aux (struct mc_options *options, void *aux) +{ + options->aux = aux; +} + +/* Results of a model checking run. */ +struct mc_results + { + /* Overall results. */ + enum mc_stop_reason stop_reason; /* Why the run ended. */ + int unique_state_count; /* Number of unique states checked. */ + int error_count; /* Number of errors found. */ + + /* Depth statistics. */ + int max_depth_reached; /* Max depth state examined. */ + struct moments1 *depth_moments; /* Enables reporting mean depth. */ + + /* If error_count > 0, path to the last error reported. */ + struct mc_path error_path; + + /* States dropped... */ + int duplicate_dropped_states; /* ...as duplicates. */ + int off_path_dropped_states; /* ...as off-path (MC_PATH only). */ + int depth_dropped_states; /* ...due to excessive depth. */ + int queue_dropped_states; /* ...due to queue overflow. */ + + /* Queue statistics. */ + int queued_unprocessed_states; /* Enqueued but never dequeued. */ + int max_queue_length; /* Maximum queue length observed. */ + + /* Timing. */ + struct timeval start; /* Start of model checking run. */ + struct timeval end; /* End of model checking run. */ + }; + +/* Creates, initializes, and returns a new set of results. */ +static struct mc_results * +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) +{ + if (results != NULL) + { + moments1_destroy (results->depth_moments); + mc_path_destroy (&results->error_path); + free (results); + } +} + +/* Returns RESULTS's reason that the model checking run + terminated. The possible reasons are: + + - MC_CONTINUING: The run is not actually yet complete. This + can only be returned before mc_run has returned, e.g. when + the progress function set by mc_options_set_progress_func + examines the run's results. + + - MC_SUCCESS: The run completed because the queue emptied. + The entire state space might not have been explored due to a + requested limit on maximum depth, hash collisions, etc. + + - MC_MAX_UNIQUE_STATES: The run completed because as many + unique states have been checked as were requested (using + mc_options_set_max_unique_states). + + - MC_MAX_ERROR_COUNT: The run completed because the maximum + requested number of errors (by default, 1 error) was + reached. + + - MC_END_OF_PATH: The run completed because the path specified + with mc_options_set_follow_path was fully traversed. + + - MC_TIMEOUT: The run completed because the time limit set + with mc_options_set_time_limit was exceeded. + + - 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) +{ + 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) +{ + 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) +{ + return results->error_count; +} + +/* Returns the maximum depth reached during the model checker run + 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) +{ + 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) +{ + double mean; + moments1_calculate (results->depth_moments, NULL, &mean, NULL, NULL, NULL); + return mean != SYSMIS ? mean : 0.0; +} + +/* Returns the path traversed to obtain the last error + encountered during the model checker run represented by + 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) +{ + return results->error_count > 0 ? &results->error_path : NULL; +} + +/* Returns the number of states dropped as duplicates (based on + hash value) during the model checker run represented by + RESULTS. */ +int +mc_results_get_duplicate_dropped_states (const struct mc_results *results) +{ + return results->duplicate_dropped_states; +} + +/* Returns the number of states dropped because they were off the + path specified by mc_options_set_follow_path during the model + checker run represented by RESULTS. A nonzero value here + 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) +{ + return results->off_path_dropped_states; +} + +/* Returns the number of states dropped because their depth + 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) +{ + return results->depth_dropped_states; +} + +/* Returns the number of states dropped from the queue due to + queue overflow during the model checker run represented by + RESULTS. */ +int +mc_results_get_queue_dropped_states (const struct mc_results *results) +{ + return results->queue_dropped_states; +} + +/* Returns the number of states that were checked and enqueued + but never dequeued and processed during the model checker run + represented by RESULTS. This is zero if the stop reason is + MC_CONTINUING or MC_SUCCESS; otherwise, it is the number of + states in the queue at the time that the checking run + stopped. */ +int +mc_results_get_queued_unprocessed_states (const struct mc_results *results) +{ + return results->queued_unprocessed_states; +} + +/* Returns the maximum length of the queue during the model + checker run represented by RESULTS. If this is equal to the + 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) +{ + 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) +{ + return results->start; +} + +/* Returns the time at which the model checker run represented by + 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) +{ + 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) +{ + /* 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; + y.tv_usec -= 1000000 * nsec; + y.tv_sec += nsec; + } + if (x.tv_usec - y.tv_usec > 1000000) { + int nsec = (x.tv_usec - y.tv_usec) / 1000000; + y.tv_usec += 1000000 * nsec; + y.tv_sec -= nsec; + } + + /* Compute the time remaining to wait. + `tv_usec' is certainly positive. */ + difference = (x.tv_sec - y.tv_sec) + (x.tv_usec - y.tv_usec) / 1000000.0; + if (x.tv_sec < y.tv_sec) + difference = -difference; + return difference; +} + + +/* Returns the duration, in seconds, of the model checker run + 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) +{ + assert (results->stop_reason != MC_CONTINUING); + return timeval_subtract (results->end, results->start); +} + +/* An active model checking run. */ +struct mc + { + /* Related data structures. */ + const struct mc_class *class; + struct mc_options *options; + struct mc_results *results; + + /* Array of 2**(options->hash_bits) bits representing states + already visited. */ + unsigned char *hash; + + /* State queue. */ + struct mc_state **queue; /* Array of pointers to states. */ + struct deque queue_deque; /* Deque. */ + + /* State currently being built by "init" or "mutate". */ + struct mc_path path; /* Path to current state. */ + struct string path_string; /* Buffer for path_string function. */ + bool state_named; /* mc_name_operation called? */ + bool state_error; /* mc_error called? */ + + /* Statistics for calling the progress function. */ + unsigned int progress; /* Current progress value. */ + unsigned int next_progress; /* Next value to call progress func. */ + unsigned int prev_progress; /* Last value progress func called. */ + struct timeval prev_progress_time; /* Last time progress func called. */ + + /* 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. */ + }; + +/* A state in the queue. */ +struct mc_state + { + struct mc_path path; /* Path to this state. */ + void *data; /* Client-supplied data. */ + }; + +/* Points to the current struct mc's "interrupted" member. */ +static bool *interrupted_ptr = NULL; + +static const char *path_string (struct mc *); +static void free_state (const struct mc *, struct mc_state *); +static void stop (struct mc *, enum mc_stop_reason); +static struct mc_state *make_state (const struct mc *, void *); +static size_t random_queue_index (struct mc *); +static void enqueue_state (struct mc *, struct mc_state *); +static void do_error_state (struct mc *); +static void next_operation (struct mc *); +static bool is_off_path (const struct mc *); +static void sigint_handler (int signum); +static void init_mc (struct mc *, + const struct mc_class *, struct mc_options *); +static void finish_mc (struct mc *); + +/* Runs the model checker on the client-specified CLASS with the + client-specified OPTIONS. OPTIONS may be a null pointer if + the defaults are acceptable. Destroys OPTIONS; use + mc_options_clone if a copy is needed. + + Returns the results of the model checking run, which must be + destroyed by the client with mc_results_destroy. + + To pass auxiliary data to the functions in CLASS, use + 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) +{ + struct mc mc; + + init_mc (&mc, class, options); + while (!deque_is_empty (&mc.queue_deque) + && mc.results->stop_reason == MC_CONTINUING) + { + struct mc_state *state = mc.queue[deque_pop_front (&mc.queue_deque)]; + mc_path_copy (&mc.path, &state->path); + mc_path_push (&mc.path, 0); + class->mutate (&mc, state->data); + free_state (&mc, state); + if (mc.interrupted) + stop (&mc, MC_INTERRUPTED); + } + finish_mc (&mc); + + return mc.results; +} + +/* Tests whether the current operation is one that should be + performed, checked, and enqueued. If so, returns true. + Otherwise, returns false and, unless checking is stopped, + advances to the next state. The caller should then advance + to the next operation. + + This function should be called from the client-provided + "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) +{ + if (mc->results->stop_reason != MC_CONTINUING) + return false; + else if (is_off_path (mc)) + { + next_operation (mc); + return false; + } + else + return true; +} + +/* Tests whether HASH represents a state that has (probably) + already been enqueued. If not, returns false and marks HASH + so that it will be treated as a duplicate in the future. If + so, returns true and advances to the next state. The + caller should then advance to the next operation. + + This function should be called from the client-provided + "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) +{ + if (mc->options->hash_bits > 0) + { + hash &= (1u << mc->options->hash_bits) - 1; + if (TEST_BIT (mc->hash, hash)) + { + if (mc->options->verbosity > 2) + fprintf (mc->options->output_file, + " [%s] discard duplicate state\n", path_string (mc)); + mc->results->duplicate_dropped_states++; + next_operation (mc); + return true; + } + SET_BIT (mc->hash, hash); + } + return false; +} + +/* Names the current state NAME, which may contain + printf-style format specifications. NAME should be a + human-readable name for the current operation. + + This function should be called from the client-provided + "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, ...) +{ + va_list args; + + va_start (args, name); + mc_vname_operation (mc, name, args); + va_end (args); +} + +/* Names the current state NAME, which may contain + printf-style format specifications, for which the + corresponding arguments must be given in ARGS. NAME should be + a human-readable name for the current operation. + + This function should be called from the client-provided + "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) +{ + 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) + { + fprintf (mc->options->output_file, " [%s] ", path_string (mc)); + vfprintf (mc->options->output_file, name, args); + putc ('\n', mc->options->output_file); + } +} + +/* Reports the given error MESSAGE for the current operation. + The resulting state should still be passed to mc_add_state + when all relevant error messages have been issued. The state + will not, however, be enqueued for later mutation of its own. + + By default, model checking stops after the first error + encountered. + + This function should be called from the client-provided + "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, ...) +{ + va_list args; + + if (mc->results->stop_reason != MC_CONTINUING) + return; + + if (mc->options->verbosity > 1) + fputs (" ", mc->options->output_file); + fprintf (mc->options->output_file, "[%s] error: ", + path_string (mc)); + va_start (args, message); + vfprintf (mc->options->output_file, message, args); + va_end (args); + putc ('\n', mc->options->output_file); + + mc->state_error = true; +} + +/* Enqueues DATA as the state corresponding to the current + operation. The operation should have been named with a call + to mc_name_operation, and it should have been checked by the + caller (who should have reported any errors with mc_error). + + This function should be called from the client-provided + "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) +{ + if (!mc->state_named && mc->options->verbosity > 0) + fprintf (mc->options->output_file, " [%s] warning: unnamed state\n", + path_string (mc)); + + if (mc->results->stop_reason != MC_CONTINUING) + { + /* Nothing to do. */ + } + 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 + { + /* This is the common case. */ + mc->results->unique_state_count++; + if (mc->results->unique_state_count >= mc->options->max_unique_states) + stop (mc, MC_MAX_UNIQUE_STATES); + enqueue_state (mc, make_state (mc, data)); + next_operation (mc); + return; + } + + mc->class->destroy (mc, data); + next_operation (mc); +} + +/* Returns the options that were passed to mc_run for model + checker MC. */ +const struct mc_options * +mc_get_options (const struct mc *mc) +{ + return mc->options; +} + +/* Returns the current state of the results for model checker + MC. This function is appropriate for use from the progress + function set by mc_options_set_progress_func. + + Not all of the results are meaningful before model checking + completes. */ +const struct mc_results * +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) +{ + return mc_options_get_aux (mc_get_options (mc)); +} + +/* Expresses MC->path as a string and returns the string. */ +static const char * +path_string (struct mc *mc) +{ + ds_clear (&mc->path_string); + mc_path_to_string (&mc->path, &mc->path_string); + return ds_cstr (&mc->path_string); +} + +/* Frees STATE, including client data. */ +static void +free_state (const struct mc *mc, struct mc_state *state) +{ + mc->class->destroy (mc, state->data); + mc_path_destroy (&state->path); + free (state); +} + +/* 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) +{ + 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) +{ + struct mc_state *new = xmalloc (sizeof *new); + mc_path_init (&new->path); + mc_path_copy (&new->path, &mc->path); + new->data = data; + return new; +} + +/* Returns the index in MC->queue of a random element in the + queue. */ +static size_t +random_queue_index (struct mc *mc) +{ + assert (!deque_is_empty (&mc->queue_deque)); + return deque_front (&mc->queue_deque, + rand () % deque_count (&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) +{ + 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); + + 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) + { + case MC_BROAD: + idx = deque_push_back (&mc->queue_deque); + break; + case MC_DEEP: + idx = deque_push_front (&mc->queue_deque); + break; + case MC_RANDOM: + if (!deque_is_empty (&mc->queue_deque)) + { + idx = random_queue_index (mc); + mc->queue[deque_push_front (&mc->queue_deque)] + = mc->queue[idx]; + } + else + idx = deque_push_front (&mc->queue_deque); + break; + case MC_PATH: + assert (deque_is_empty (&mc->queue_deque)); + assert (!is_off_path (mc)); + idx = deque_push_back (&mc->queue_deque); + if (mc->path.length + >= mc_path_get_length (&mc->options->follow_path)) + stop (mc, MC_END_OF_PATH); + break; + default: + NOT_REACHED (); + } + if (deque_count (&mc->queue_deque) > mc->results->max_queue_length) + mc->results->max_queue_length = deque_count (&mc->queue_deque); + } + 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) + { + case MC_DROP_NEWEST: + free_state (mc, new); + return; + case MC_DROP_OLDEST: + switch (mc->options->strategy) + { + case MC_BROAD: + idx = deque_front (&mc->queue_deque, 0); + break; + case MC_DEEP: + idx = deque_back (&mc->queue_deque, 0); + break; + case MC_RANDOM: + case MC_PATH: + default: + NOT_REACHED (); + } + break; + case MC_DROP_RANDOM: + idx = random_queue_index (mc); + break; + default: + NOT_REACHED (); + } + free_state (mc, mc->queue[idx]); + } + mc->queue[idx] = new; +} + +/* Process an error state being added to MC. */ +static void +do_error_state (struct mc *mc) +{ + mc->results->error_count++; + if (mc->results->error_count >= mc->options->max_errors) + 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; + + fprintf (mc->options->output_file, "[%s] retracing error path:\n", + 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->path); + + mc_results_destroy (mc_run (mc->class, path_options)); + + putc ('\n', mc->options->output_file); + } +} + +/* Advances MC to start processing the operation following the + current one. */ +static void +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) + { + struct timeval now; + double elapsed, delta; + + if (mc->results->stop_reason == MC_CONTINUING + && !mc->options->progress_func (mc)) + stop (mc, MC_INTERRUPTED); + + gettimeofday (&now, NULL); + + if (mc->options->time_limit > 0.0 + && (timeval_subtract (now, mc->results->start) + > mc->options->time_limit)) + stop (mc, MC_TIMEOUT); + + elapsed = timeval_subtract (now, mc->prev_progress_time); + if (elapsed > 0.0) + { + /* Re-estimate the amount of progress to take + progress_usec microseconds. */ + unsigned int progress = mc->progress - mc->prev_progress; + double progress_sec = mc->options->progress_usec / 1000000.0; + delta = progress / elapsed * progress_sec; + } + 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; + } + + if (delta > 0.0 && delta + mc->progress + 1.0 < UINT_MAX) + mc->next_progress = mc->progress + delta + 1.0; + else + mc->next_progress = mc->progress + (mc->progress - mc->prev_progress); + + mc->prev_progress = mc->progress; + mc->prev_progress_time = now; + } +} + +/* 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) +{ + return (mc->options->strategy == MC_PATH + && (mc_path_back (&mc->path) + != mc_path_get_operation (&mc->options->follow_path, + mc->path.length - 1))); +} + +/* Handler for SIGINT. */ +static void +sigint_handler (int signum UNUSED) +{ + /* Just mark the model checker as interrupted. */ + *interrupted_ptr = true; +} + +/* Initializes MC as a model checker with the given CLASS and + 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) +{ + /* 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) + { + options->max_depth = INT_MAX; + options->hash_bits = 0; + } + if (options->progress_usec == 0) + { + options->progress_func = null_progress; + if (options->time_limit > 0.0) + options->progress_usec = 250000; + } + + /* Initialize MC. */ + mc->class = class; + mc->options = options; + mc->results = mc_results_create (); + + mc->hash = (mc->options->hash_bits > 0 + ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT)) + : NULL); + + mc->queue = NULL; + deque_init_null (&mc->queue_deque); + + mc_path_init (&mc->path); + mc_path_push (&mc->path, 0); + ds_init_empty (&mc->path_string); + mc->state_named = false; + mc->state_error = false; + + mc->progress = 0; + mc->next_progress = mc->options->progress_usec != 0 ? 100 : UINT_MAX; + mc->prev_progress = 0; + mc->prev_progress_time = mc->results->start; + + if (mc->options->strategy == MC_RANDOM + || options->queue_limit_strategy == MC_DROP_RANDOM) + srand (mc->options->seed); + + mc->interrupted = false; + mc->saved_interrupted_ptr = interrupted_ptr; + interrupted_ptr = &mc->interrupted; + mc->saved_sigint = signal (SIGINT, sigint_handler); + + class->init (mc); +} + +/* Complete the model checker run for MC. */ +static void +finish_mc (struct mc *mc) +{ + /* Restore signal handlers. */ + signal (SIGINT, mc->saved_sigint); + interrupted_ptr = mc->saved_interrupted_ptr; + + /* Mark the run complete. */ + stop (mc, MC_SUCCESS); + gettimeofday (&mc->results->end, NULL); + + /* Empty the queue. */ + mc->results->queued_unprocessed_states = deque_count (&mc->queue_deque); + while (!deque_is_empty (&mc->queue_deque)) + { + struct mc_state *state = mc->queue[deque_pop_front (&mc->queue_deque)]; + free_state (mc, state); + } + + /* Notify the progress function of completion. */ + mc->options->progress_func (mc); + + /* Free memory. */ + mc_path_destroy (&mc->path); + ds_destroy (&mc->path_string); + free (mc->options); + free (mc->queue); + free (mc->hash); +} diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h new file mode 100644 index 00000000..dd42e2fd --- /dev/null +++ b/src/libpspp/model-checker.h @@ -0,0 +1,465 @@ +/* PSPP - computes sample statistics. + 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 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. */ + +/* Implementation-level model checker. + + A model checker is a tool for software testing and + verification that works by exploring all the possible states + in a system and verifying their internal consistency. A + conventional model checker requires that the code in a system + be translated into a specification language. The model + checker then verifies the specification, rather than the code. + + This is instead an implementation-level model checker, which + does not require a separate specification. Instead, the model + checker requires writing a second implementation of the system + being checked. The second implementation can usually be made + almost trivial in comparison to the one being checked, because + it's usually acceptable for its performance to be + comparatively poor, e.g. O(N^2) instead of O(lg N), and thus + to use much simpler algorithms. + + For introduction to the implementation-level model checking + approach used here, please refer to the following papers: + + Musuvathi, Park, Chou, Engler, Dill, "CMC: A Pragmatic + Approach to Model Checking Real Code", Proceedings of the + Fifth Symposium on Operating Systems Design and + Implementation (OSDI), Dec 2002. + http://sprout.stanford.edu/PAPERS/CMC-OSDI-2002/CMC-OSDI-2002.pdf + + Yang, Twohey, Engler, Musuvathi, "Using Model Checking to + Find Serious File System Errors", Proceedings of the Sixth + Symposium on Operating System Design and Implementation + (OSDI), Dec 2004. + http://www.stanford.edu/~engler/osdi04-fisc.pdf + + Yang, Twohey, Pfaff, Sar, Engler, "EXPLODE: A Lightweight, + General Approach to Finding Serious Errors in Storage + Systems", First Workshop on the Evaluation of Software + Defect Detection Tools (BUGS), June 2005. + http://benpfaff.org/papers/explode.pdf + + Use of a model checker is appropriate when the system being + checked is difficult to test using handwritten tests. This + can be the case, for example, when the system has a + complicated internal state that is difficult to reason about + over a long series of operations. + + The implementation model checker works by putting a set of one + of more initial states in a queue (and checking them for + consistency). Then the model checker removes a state from the + queue and applies all possible operations of interest to it + ("mutates" it), obtaining a set of zero or more child states + (and checking each of them for consistency). Each of these + states is itself added to the queue. The model checker + continues dequeuing states and mutating and checking them + until the queue is empty. + + In pseudo-code, the process looks like this: + + Q = { initial states } + while Q is not empty: + S = dequeue(Q) + for each operation applicable to S do: + T = operation(S) + check(T) + enqueue(Q, T) + + In many cases this process will never terminate, because every + state has one or more child states. For some systems this is + unavoidable, but in others we can make the process finite by + pursuing a few stratagems: + + 1. Limit the maximum size of the system; for example, limit + the number of rows and columns in the implementation of a + table being checked. The client of the model checker is + responsible for implementing such limits. + + 2. Avoid checking a single state more than one time. This + model checker provides assistance for this function by + allowing the client to provide a hash of the system state. + States with identical hashes will only be checked once + during a single run. + + When a system cannot be made finite, or when a finite system + is too large to check in a practical amount of time, the model + checker provides multiple ways to limit the checking run: + based on maximum depth, maximum unique states checked, maximum + errors found (by default, 1), or maximum time used for + checking. + + The client of the model checker must provide three functions + via function pointers embedded into a "struct mc_class": + + 1. void init (struct mc *mc); + + This function is called once at the beginning of a + checking run. It checks one or more initial states and + adds them to the model checker's queue. (If it does not + add any states to the queue, then there is nothing to + check.) + + Here's an outline for writing the init function: + + void + init_foo (struct mc *mc) + { + struct foo *foo; + + mc_name_operation (mc, "initial state"); + foo = generate_initial_foo (); + if (!state_is_consistent (foo)) + mc_error (mc, "inconsistent state"); + mc_add_state (mc, foo); + } + + 2. void mutate (struct mc *mc, const void *data); + + This function is called when a dequeued state is ready to + be mutated. For each operation that can be applied to + the client-specified DATA, it applies that operation to a + clone of the DATA, checks that the clone is consistent, + and adds the clone to the model checker's queue. + + Here's an outline for writing the mutate function: + + void + mutate_foo (struct mc *mc, void *state_) + { + struct foo *state = state_; + + for (...each operation...) + if (mc_include_state (mc)) + { + struct foo *clone; + + mc_name_operation (mc, "do operation %s", ...); + clone = clone_foo (state); + do_operation (clone); + if (!mc_discard_dup_state (mc, hash_foo (clone))) + { + if (!state_is_consistent (clone)) + mc_error (mc, "inconsistent state"); + mc_add_state (mc, clone); + } + else + destroy_foo (clone); + } + } + + Notes on the above outline: + + - The call to mc_include_state allows currently + uninteresting operations to be skipped. It is not + essential. + + - The call to mc_name_operation should give the current + operation a human-readable name. The name may + include printf-style format specifications. + + When an error occurs, the model checker (by default) + replays the sequence of operations performed to reach + the error, printing the name of the operation at each + step, which is often sufficient information in itself + to debug the error. + + At higher levels of verbosity, the name is printed + for each operation. + + - Operations should be performed on a copy of the data + provided. The data provided should not be destroyed + or modified. + + - The call to mc_discard_dup_state is needed to discard + (probably) duplicate states. It is otherwise + optional. + + To reduce the probability of collisions, use a + high-quality hash function. MD4 is a reasonable + choice: it is fast but high-quality. In one test, + switching to MD4 from MD5 increased overall speed of + model checking by 8% and actually reduced (!) the + number of collisions. + + The hash value needs to include enough of the state + to ensure that interesting states are not excluded, + but it need not include the entire state. For + example, in many cases, the structure of complex data + (metadata) is often much more important than the + contents (data), so it may be reasonable to hash only + the metadata. + + mc_discard_dup_state may be called before or after + checking for consistency, but calling it first avoids + wasting time checking duplicate states for + consistency, which again can be a significant + performance boost. + + - The mc_error function reports errors. It may be + called as many times as desired to report each kind + of inconsistency in a state. + + - The mc_add_state function adds the new state to the + queue. It should be called regardless of whether an + error was reported, to indicate to the model checker + that state processing has finished. + + - The mutation function should be deterministic, to + make it possible to reliably reproduce errors. + + 3. void destroy (struct mc *mc, void *data); + + This function is called to discard the client-specified + DATA associated with a state. + + Numerous options are available for configuring the model + checker. The most important of these are: + + - Search algorithm: + + * Breadth-first search (the default): First try all the + operations with depth 1, then those with depth 2, then + those with depth 3, and so on. + + This search algorithm finds the least number of + operations needed to trigger a given bug. + + * Depth-first search: Searches downward in the tree of + states as fast as possible. Good for finding bugs that + require long sequences of operations to trigger. + + * Random-first search: Searches through the tree of + states in random order. + + * Explicit path: Applies an explicitly specified sequence + of operations. + + - Verbosity: By default, messages are printed only when an + error is encountered, but you can cause the checker to + print a message on every state transition. This is most + useful when the errors in your code cause segfaults or + some other kind of sudden termination. + + - Treatment of errors: By default, when an error is + encountered, the model checker recursively invokes itself + with an increased verbosity level and configured to follow + only the error path. As long as the mutation function is + deterministic, this quickly and concisely replays the + error and describes the path followed to reach it in an + easily human-readable manner. + + - Limits: + + * Maximum depth: You can limit the depth of the operations + performed. Most often useful with depth-first search. + By default, depth is unlimited. + + * Maximum queue length: You can limit the number of states + kept in the queue at any given time. The main reason to + do so is to limit memory consumption. The default + limit is 10,000 states. Several strategies are + available for choosing which state to drop when the + queue overflows. + + - Stop conditions: based on maximum unique states checked, + maximum errors found (by default, 1), or maximum time used + for checking. + + - Progress: by default, the checker prints a '.' on stderr + every .25 seconds, but you can substitute another progress + function or disable progress printing. + + This model checker does not (yet) include two features + described in the papers cited above: utility scoring + heuristics to guide the search strategy and "choice points" to + explore alternative cases. The former feature is less + interesting for this model checker, because the data + structures we are thus far using it to model are much smaller + than those discussed in the paper. The latter feature we + should implement at some point. */ + +#ifndef LIBPSPP_MODEL_CHECKER_H +#define LIBPSPP_MODEL_CHECKER_H 1 + +#include +#include +#include +#include + +#include + +/* An active model checking run. */ +struct mc; + +/* Provided by each client of the model checker. */ +struct mc_class + { + void (*init) (struct mc *); + void (*mutate) (struct mc *, const void *); + void (*destroy) (const struct mc *, void *); + }; + +/* Results of a model checking run. */ +struct mc_results; + +/* Configuration for running the model checker. */ +struct mc_options; + +/* Primary external interface to model checker. */ +struct mc_results *mc_run (const struct mc_class *, struct mc_options *); + +/* Functions for use from client-supplied "init" and "mutate" + functions. */ +bool mc_include_state (struct mc *); +bool mc_discard_dup_state (struct mc *, unsigned int hash); +void mc_name_operation (struct mc *, const char *, ...) PRINTF_FORMAT (2, 3); +void mc_vname_operation (struct mc *, const char *, va_list) + PRINTF_FORMAT (2, 0); +void mc_error (struct mc *, const char *, ...) PRINTF_FORMAT (2, 3); +void mc_add_state (struct mc *, void *data); + +/* Functions for use from client-supplied "init", "mutate", and + "destroy" functions. */ +const struct mc_options *mc_get_options (const struct mc *); +const struct mc_results *mc_get_results (const struct mc *); +void *mc_get_aux (const struct mc *); + +/* A path of operations through a model to arrive at some + particular state. */ +struct mc_path + { + int *ops; /* Sequence of operations. */ + size_t length; /* Number of operations. */ + size_t capacity; /* Number of operations for which room is allocated. */ + }; + +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); +int mc_path_pop (struct mc_path *); +int mc_path_back (const struct mc_path *); +void mc_path_destroy (struct mc_path *); + +int mc_path_get_operation (const struct mc_path *, size_t index); +size_t mc_path_get_length (const struct mc_path *); + +struct string; +void mc_path_to_string (const struct mc_path *, struct string *); + +struct mc_options *mc_options_create (void); +struct mc_options *mc_options_clone (const struct mc_options *); +void mc_options_destroy (struct mc_options *); + +/* Search strategy. */ +enum mc_strategy + { + MC_BROAD, /* Breadth-first search. */ + MC_DEEP, /* Depth-first 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); +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 *); +void mc_options_set_max_depth (struct mc_options *, int max_depth); +int mc_options_get_hash_bits (const struct mc_options *); +void mc_options_set_hash_bits (struct mc_options *, int hash_bits); + +const struct mc_path *mc_options_get_follow_path (const struct mc_options *); +void mc_options_set_follow_path (struct mc_options *, const struct mc_path *); + +/* Strategy for dropped states from the queue when it + overflows. */ +enum mc_queue_limit_strategy + { + MC_DROP_NEWEST, /* Don't enqueue the new state at all. */ + MC_DROP_OLDEST, /* Drop the oldest state in the queue. */ + MC_DROP_RANDOM /* Drop a random state from the queue. */ + }; + +int mc_options_get_queue_limit (const struct mc_options *); +void mc_options_set_queue_limit (struct mc_options *, int queue_limit); +enum mc_queue_limit_strategy mc_options_get_queue_limit_strategy ( + const struct mc_options *); +void mc_options_set_queue_limit_strategy (struct mc_options *, + enum mc_queue_limit_strategy); + +int mc_options_get_max_unique_states (const struct mc_options *); +void mc_options_set_max_unique_states (struct mc_options *, + int max_unique_states); +int mc_options_get_max_errors (const struct mc_options *); +void mc_options_set_max_errors (struct mc_options *, int max_errors); +double mc_options_get_time_limit (const struct mc_options *); +void mc_options_set_time_limit (struct mc_options *, double time_limit); + +int mc_options_get_verbosity (const struct mc_options *); +void mc_options_set_verbosity (struct mc_options *, int verbosity); +int mc_options_get_failure_verbosity (const struct mc_options *); +void mc_options_set_failure_verbosity (struct mc_options *, + int failure_verbosity); +FILE *mc_options_get_output_file (const struct mc_options *); +void mc_options_set_output_file (struct mc_options *, FILE *); + +typedef bool mc_progress_func (struct mc *); +int mc_options_get_progress_usec (const struct mc_options *); +void mc_options_set_progress_usec (struct mc_options *, int progress_usec); +mc_progress_func *mc_options_get_progress_func (const struct mc_options *); +void mc_options_set_progress_func (struct mc_options *, mc_progress_func *); + +void *mc_options_get_aux (const struct mc_options *); +void mc_options_set_aux (struct mc_options *, void *aux); + +/* Reason that a model checking run terminated. */ +enum mc_stop_reason + { + MC_CONTINUING, /* Run has not yet terminated. */ + MC_SUCCESS, /* Queue emptied (ran out of states). */ + MC_MAX_UNIQUE_STATES, /* Did requested number of unique states. */ + MC_MAX_ERROR_COUNT, /* Too many errors. */ + MC_END_OF_PATH, /* Processed requested path (MC_PATH only). */ + MC_TIMEOUT, /* Timeout. */ + MC_INTERRUPTED /* Received SIGINT (Ctrl+C). */ + }; + +void mc_results_destroy (struct mc_results *); + +enum mc_stop_reason mc_results_get_stop_reason (const struct mc_results *); +int mc_results_get_unique_state_count (const struct mc_results *); +int mc_results_get_error_count (const struct mc_results *); + +int mc_results_get_max_depth_reached (const struct mc_results *); +double mc_results_get_mean_depth_reached (const struct mc_results *); + +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 *); +int mc_results_get_depth_dropped_states (const struct mc_results *); +int mc_results_get_queue_dropped_states (const struct mc_results *); +int mc_results_get_queued_unprocessed_states (const struct mc_results *); +int mc_results_get_max_queue_length (const struct mc_results *); + +struct timeval mc_results_get_start (const struct mc_results *); +struct timeval mc_results_get_end (const struct mc_results *); +double mc_results_get_duration (const struct mc_results *); + +#endif /* libpspp/model-checker.h */ -- 2.30.2