X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Flanguage%2Ftests%2Fmodel-checker.c;fp=src%2Flanguage%2Ftests%2Fmodel-checker.c;h=0000000000000000000000000000000000000000;hb=3db80dc65b18355b719e8d56032400c753aa4eb7;hp=a0407500688e2988c8cbffee2bbd93f646668cc8;hpb=02d26302aea9cb2c25c8cbb50bd120674de1f862;p=pspp

diff --git a/src/language/tests/model-checker.c b/src/language/tests/model-checker.c
deleted file mode 100644
index a040750068..0000000000
--- a/src/language/tests/model-checker.c
+++ /dev/null
@@ -1,1466 +0,0 @@
-/* PSPP - a program for statistical analysis.
-   Copyright (C) 2007 Free Software Foundation, Inc.
-
-   This program is free software: you can redistribute it and/or modify
-   it under the terms of the GNU General Public License as published by
-   the Free Software Foundation, either version 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.
-
-   You should have received a copy of the GNU General Public License
-   along with this program.  If not, see <http://www.gnu.org/licenses/>. */
-
-#include <config.h>
-
-#include "model-checker.h"
-
-#include <limits.h>
-#include <signal.h>
-#include <stdarg.h>
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <sys/time.h>
-
-#include <data/val-type.h>
-#include <libpspp/bit-vector.h>
-#include <libpspp/compiler.h>
-#include <libpspp/deque.h>
-#include <libpspp/str.h>
-#include <math/moments.h>
-
-#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. */
-    void (*saved_sigint) (int);         /* 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);
-}