src/libpspp/model-checker.c

   1 /* PSPP - a program for statistical analysis.
   2    Copyright (C) 2007 Free Software Foundation, Inc.
   3
   4    This program is free software: you can redistribute it and/or modify
   5    it under the terms of the GNU General Public License as published by
   6    the Free Software Foundation, either version 3 of the License, or
   7    (at your option) any later version.
   8
   9    This program is distributed in the hope that it will be useful,
  10    but WITHOUT ANY WARRANTY; without even the implied warranty of
  11    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  12    GNU General Public License for more details.
  13
  14    You should have received a copy of the GNU General Public License
  15    along with this program.  If not, see <http://www.gnu.org/licenses/>. */
  16
  17 #include <config.h>
  18
  19 #include <libpspp/model-checker.h>
  20
  21 #include <limits.h>
  22 #include <signal.h>
  23 #include <stdarg.h>
  24 #include <stdio.h>
  25 #include <stdlib.h>
  26 #include <string.h>
  27 #include <sys/time.h>
  28
  29 #include <data/val-type.h>
  30 #include <libpspp/bit-vector.h>
  31 #include <libpspp/compiler.h>
  32 #include <libpspp/deque.h>
  33 #include <libpspp/str.h>
  34 #include <math/moments.h>
  35
  36 #include "error.h"
  37 #include "minmax.h"
  38 #include "xalloc.h"
  39 \f
  40 /* Initializes PATH as an empty path. */
  41 void
  42 mc_path_init (struct mc_path *path)
  43 {
  44   path->ops = NULL;
  45   path->length = 0;
  46   path->capacity = 0;
  47 }
  48
  49 /* Copies the contents of OLD into NEW. */
  50 void
  51 mc_path_copy (struct mc_path *new, const struct mc_path *old)
  52 {
  53   if (old->length > new->capacity)
  54     {
  55       new->capacity = old->length;
  56       free (new->ops);
  57       new->ops = xnmalloc (new->capacity, sizeof *new->ops);
  58     }
  59   new->length = old->length;
  60   memcpy (new->ops, old->ops, old->length * sizeof *new->ops);
  61 }
  62
  63 /* Adds OP to the end of PATH. */
  64 void
  65 mc_path_push (struct mc_path *path, int op)
  66 {
  67   if (path->length >= path->capacity)
  68     path->ops = xnrealloc (path->ops, ++path->capacity, sizeof *path->ops);
  69   path->ops[path->length++] = op;
  70 }
  71
  72 /* Removes and returns the operation at the end of PATH. */
  73 int
  74 mc_path_pop (struct mc_path *path)
  75 {
  76   int back = mc_path_back (path);
  77   path->length--;
  78   return back;
  79 }
  80
  81 /* Returns the operation at the end of PATH. */
  82 int
  83 mc_path_back (const struct mc_path *path)
  84 {
  85   assert (path->length > 0);
  86   return path->ops[path->length - 1];
  87 }
  88
  89 /* Destroys PATH. */
  90 void
  91 mc_path_destroy (struct mc_path *path)
  92 {
  93   free (path->ops);
  94   path->ops = NULL;
  95 }
  96
  97 /* Returns the operation in position INDEX in PATH.
  98    INDEX must be less than the length of PATH. */
  99 int
 100 mc_path_get_operation (const struct mc_path *path, size_t index)
 101 {
 102   assert (index < path->length);
 103   return path->ops[index];
 104 }
 105
 106 /* Returns the number of operations in PATH. */
 107 size_t
 108 mc_path_get_length (const struct mc_path *path)
 109 {
 110   return path->length;
 111 }
 112
 113 /* Appends the operations in PATH to STRING, separating each one
 114    with a single space. */
 115 void
 116 mc_path_to_string (const struct mc_path *path, struct string *string)
 117 {
 118   size_t i;
 119
 120   for (i = 0; i < mc_path_get_length (path); i++)
 121     {
 122       if (i > 0)
 123         ds_put_char (string, ' ');
 124       ds_put_format (string, "%d", mc_path_get_operation (path, i));
 125     }
 126 }
 127 \f
 128 /* Search options. */
 129 struct mc_options
 130   {
 131     /* Search strategy. */
 132     enum mc_strategy strategy;          /* Type of strategy. */
 133     int max_depth;                      /* Limit on depth (or INT_MAX). */
 134     int hash_bits;                      /* Number of bits to hash (or 0). */
 135     unsigned int seed;                  /* Random seed for MC_RANDOM
 136                                            or MC_DROP_RANDOM. */
 137     struct mc_path follow_path;         /* Path for MC_PATH. */
 138
 139     /* Queue configuration. */
 140     int queue_limit;                    /* Maximum length of queue. */
 141     enum mc_queue_limit_strategy queue_limit_strategy;
 142                                         /* How to choose state to drop
 143                                            from queue. */
 144
 145     /* Stop conditions. */
 146     int max_unique_states;              /* Maximum unique states to process. */
 147     int max_errors;                     /* Maximum errors to detect. */
 148     double time_limit;                  /* Maximum time in seconds. */
 149
 150     /* Output configuration. */
 151     int verbosity;                      /* 0=low, 1=normal, 2+=high. */
 152     int failure_verbosity;              /* If greater than verbosity,
 153                                            verbosity of error replays. */
 154     FILE *output_file;                  /* File to receive output. */
 155
 156     /* How to report intermediate progress. */
 157     int progress_usec;                  /* Microseconds between reports. */
 158     mc_progress_func *progress_func;    /* Function to call on each report. */
 159
 160     /* Client data. */
 161     void *aux;
 162   };
 163
 164 /* Default progress function. */
 165 static bool
 166 default_progress (struct mc *mc)
 167 {
 168   if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
 169     putc ('.', stderr);
 170   else
 171     putc ('\n', stderr);
 172   return true;
 173 }
 174
 175 /* Do-nothing progress function. */
 176 static bool
 177 null_progress (struct mc *mc UNUSED)
 178 {
 179   return true;
 180 }
 181
 182 /* Creates and returns a set of options initialized to the
 183    defaults. */
 184 struct mc_options *
 185 mc_options_create (void)
 186 {
 187   struct mc_options *options = xmalloc (sizeof *options);
 188
 189   options->strategy = MC_BROAD;
 190   options->max_depth = INT_MAX;
 191   options->hash_bits = 20;
 192   options->seed = 0;
 193   mc_path_init (&options->follow_path);
 194
 195   options->queue_limit = 10000;
 196   options->queue_limit_strategy = MC_DROP_RANDOM;
 197
 198   options->max_unique_states = INT_MAX;
 199   options->max_errors = 1;
 200   options->time_limit = 0.0;
 201
 202   options->verbosity = 1;
 203   options->failure_verbosity = 2;
 204   options->output_file = stdout;
 205   options->progress_usec = 250000;
 206   options->progress_func = default_progress;
 207
 208   options->aux = NULL;
 209
 210   return options;
 211 }
 212
 213 /* Returns a copy of the given OPTIONS. */
 214 struct mc_options *
 215 mc_options_clone (const struct mc_options *options)
 216 {
 217   return xmemdup (options, sizeof *options);
 218 }
 219
 220 /* Destroys OPTIONS. */
 221 void
 222 mc_options_destroy (struct mc_options *options)
 223 {
 224   mc_path_destroy (&options->follow_path);
 225   free (options);
 226 }
 227
 228 /* Returns the search strategy used for OPTIONS.  The choices
 229    are:
 230
 231    - MC_BROAD (the default): Breadth-first search.  First tries
 232      all the operations with depth 1, then those with depth 2,
 233      then those with depth 3, and so on.
 234
 235      This search algorithm finds the least number of operations
 236      needed to trigger a given bug.
 237
 238    - MC_DEEP: Depth-first search.  Searches downward in the tree
 239      of states as fast as possible.  Good for finding bugs that
 240      require long sequences of operations to trigger.
 241
 242    - MC_RANDOM: Random-first search.  Searches through the tree
 243      of states in random order.  The standard C library's rand
 244      function selects the search path; you can control the seed
 245      passed to srand using mc_options_set_seed.
 246
 247    - MC_PATH: Explicit path.  Applies an explicitly specified
 248      sequence of operations. */
 249 enum mc_strategy
 250 mc_options_get_strategy (const struct mc_options *options)
 251 {
 252   return options->strategy;
 253 }
 254
 255 /* Sets the search strategy used for OPTIONS to STRATEGY.
 256
 257    This function cannot be used to set MC_PATH as the search
 258    strategy.  Use mc_options_set_follow_path instead. */
 259 void
 260 mc_options_set_strategy (struct mc_options *options, enum mc_strategy strategy)
 261 {
 262   assert (strategy == MC_BROAD
 263           || strategy == MC_DEEP
 264           || strategy == MC_RANDOM);
 265   options->strategy = strategy;
 266 }
 267
 268 /* Returns OPTION's random seed used by MC_RANDOM and
 269    MC_DROP_RANDOM. */
 270 unsigned int
 271 mc_options_get_seed (const struct mc_options *options)
 272 {
 273   return options->seed;
 274 }
 275
 276 /* Set OPTION's random seed used by MC_RANDOM and MC_DROP_RANDOM
 277    to SEED. */
 278 void
 279 mc_options_set_seed (struct mc_options *options, unsigned int seed)
 280 {
 281   options->seed = seed;
 282 }
 283
 284 /* Returns the maximum depth to which OPTIONS's search will
 285    descend.  The initial states are at depth 1, states produced
 286    as their mutations are at depth 2, and so on. */
 287 int
 288 mc_options_get_max_depth (const struct mc_options *options)
 289 {
 290   return options->max_depth;
 291 }
 292
 293 /* Sets the maximum depth to which OPTIONS's search will descend
 294    to MAX_DEPTH.  The initial states are at depth 1, states
 295    produced as their mutations are at depth 2, and so on. */
 296 void
 297 mc_options_set_max_depth (struct mc_options *options, int max_depth)
 298 {
 299   options->max_depth = max_depth;
 300 }
 301
 302 /* Returns the base-2 log of the number of bits in OPTIONS's hash
 303    table.  The hash table is used for dropping states that are
 304    probably duplicates: any state with a given hash value, as
 305    will only be processed once.  A return value of 0 indicates
 306    that the model checker will not discard duplicate states based
 307    on their hashes.
 308
 309    The hash table is a power of 2 bits long, by default 2**20
 310    bits (128 kB).  Depending on how many states you expect the
 311    model checker to check, how much memory you're willing to let
 312    the hash table take up, and how worried you are about missing
 313    states due to hash collisions, you could make it larger or
 314    smaller.
 315
 316    The "birthday paradox" points to a reasonable way to size your
 317    hash table.  If you expect the model checker to check about
 318    2**N states, then, assuming a perfect hash, you need a hash
 319    table of 2**(N+1) bits to have a 50% chance of seeing a hash
 320    collision, 2**(N+2) bits to have a 25% chance, and so on. */
 321 int
 322 mc_options_get_hash_bits (const struct mc_options *options)
 323 {
 324   return options->hash_bits;
 325 }
 326
 327 /* Sets the base-2 log of the number of bits in OPTIONS's hash
 328    table to HASH_BITS.  A HASH_BITS value of 0 requests that the
 329    model checker not discard duplicate states based on their
 330    hashes.  (This causes the model checker to never terminate in
 331    many cases.) */
 332 void
 333 mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
 334 {
 335   assert (hash_bits >= 0);
 336   options->hash_bits = MIN (hash_bits, CHAR_BIT * sizeof (unsigned int) - 1);
 337 }
 338
 339 /* Returns the path set in OPTIONS by mc_options_set_follow_path.
 340    May be used only if the search strategy is MC_PATH. */
 341 const struct mc_path *
 342 mc_options_get_follow_path (const struct mc_options *options)
 343 {
 344   assert (options->strategy == MC_PATH);
 345   return &options->follow_path;
 346 }
 347
 348 /* Sets, in OPTIONS, the search algorithm to MC_PATH and the path
 349    to be the explicit path specified in FOLLOW_PATH. */
 350 void
 351 mc_options_set_follow_path (struct mc_options *options,
 352                             const struct mc_path *follow_path)
 353 {
 354   assert (mc_path_get_length (follow_path) > 0);
 355   options->strategy = MC_PATH;
 356   mc_path_copy (&options->follow_path, follow_path);
 357 }
 358
 359 /* Returns the maximum number of queued states in OPTIONS.  The
 360    default value is 10,000.  The primary reason to limit the
 361    number of queued states is to conserve memory, so if you can
 362    afford the memory and your model needs more room in the queue,
 363    you can raise the limit.  Conversely, if your models are large
 364    or memory is constrained, you can reduce the limit.
 365
 366    Following the execution of the model checker, you can find out
 367    the maximum queue length during the run by calling
 368    mc_results_get_max_queue_length. */
 369 int
 370 mc_options_get_queue_limit (const struct mc_options *options)
 371 {
 372   return options->queue_limit;
 373 }
 374
 375 /* Sets the maximum number of queued states in OPTIONS to
 376    QUEUE_LIMIT.  */
 377 void
 378 mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
 379 {
 380   assert (queue_limit > 0);
 381   options->queue_limit = queue_limit;
 382 }
 383
 384 /* Returns the queue limit strategy used by OPTIONS, that is,
 385    when a new state must be inserted into a full state queue is
 386    full, how the state to be dropped is chosen.  The choices are:
 387
 388    - MC_DROP_NEWEST: Drop the newest state; that is, do not
 389      insert the new state into the queue at all.
 390
 391    - MC_DROP_OLDEST: Drop the state that has been enqueued for
 392      the longest.
 393
 394    - MC_DROP_RANDOM (the default): Drop a randomly selected state
 395      from the queue.  The standard C library's rand function
 396      selects the state to drop; you can control the seed passed
 397      to srand using mc_options_set_seed. */
 398 enum mc_queue_limit_strategy
 399 mc_options_get_queue_limit_strategy (const struct mc_options *options)
 400 {
 401   return options->queue_limit_strategy;
 402 }
 403
 404 /* Sets the queue limit strategy used by OPTIONS to STRATEGY.
 405
 406    This setting has no effect unless the model being checked
 407    causes the state queue to overflow (see
 408    mc_options_get_queue_limit). */
 409 void
 410 mc_options_set_queue_limit_strategy (struct mc_options *options,
 411                                      enum mc_queue_limit_strategy strategy)
 412 {
 413   assert (strategy == MC_DROP_NEWEST
 414           || strategy == MC_DROP_OLDEST
 415           || strategy == MC_DROP_RANDOM);
 416   options->queue_limit_strategy = strategy;
 417 }
 418
 419 /* Returns OPTIONS's maximum number of unique states that the
 420    model checker will examine before terminating.  The default is
 421    INT_MAX. */
 422 int
 423 mc_options_get_max_unique_states (const struct mc_options *options)
 424 {
 425   return options->max_unique_states;
 426 }
 427
 428 /* Sets OPTIONS's maximum number of unique states that the model
 429    checker will examine before terminating to
 430    MAX_UNIQUE_STATE. */
 431 void
 432 mc_options_set_max_unique_states (struct mc_options *options,
 433                                   int max_unique_states)
 434 {
 435   options->max_unique_states = max_unique_states;
 436 }
 437
 438 /* Returns the maximum number of errors that OPTIONS will allow
 439    the model checker to encounter before terminating.  The
 440    default is 1. */
 441 int
 442 mc_options_get_max_errors (const struct mc_options *options)
 443 {
 444   return options->max_errors;
 445 }
 446
 447 /* Sets the maximum number of errors that OPTIONS will allow the
 448    model checker to encounter before terminating to
 449    MAX_ERRORS. */
 450 void
 451 mc_options_set_max_errors (struct mc_options *options, int max_errors)
 452 {
 453   options->max_errors = max_errors;
 454 }
 455
 456 /* Returns the maximum amount of time, in seconds, that OPTIONS will allow the
 457    model checker to consume before terminating.  The
 458    default of 0.0 means that time consumption is unlimited. */
 459 double
 460 mc_options_get_time_limit (const struct mc_options *options)
 461 {
 462   return options->time_limit;
 463 }
 464
 465 /* Sets the maximum amount of time, in seconds, that OPTIONS will
 466    allow the model checker to consume before terminating to
 467    TIME_LIMIT.  A value of 0.0 means that time consumption is
 468    unlimited; otherwise, the return value will be positive. */
 469 void
 470 mc_options_set_time_limit (struct mc_options *options, double time_limit)
 471 {
 472   assert (time_limit >= 0.0);
 473   options->time_limit = time_limit;
 474 }
 475
 476 /* Returns the level of verbosity for output messages specified
 477    by OPTIONS.  The default verbosity level is 1.
 478
 479    A verbosity level of 0 inhibits all messages except for
 480    errors; a verbosity level of 1 also allows warnings; a
 481    verbosity level of 2 also causes a description of each state
 482    added to be output; a verbosity level of 3 also causes a
 483    description of each duplicate state to be output.  Verbosity
 484    levels less than 0 or greater than 3 are allowed but currently
 485    have no additional effect. */
 486 int
 487 mc_options_get_verbosity (const struct mc_options *options)
 488 {
 489   return options->verbosity;
 490 }
 491
 492 /* Sets the level of verbosity for output messages specified
 493    by OPTIONS to VERBOSITY. */
 494 void
 495 mc_options_set_verbosity (struct mc_options *options, int verbosity)
 496 {
 497   options->verbosity = verbosity;
 498 }
 499
 500 /* Returns the level of verbosity for failures specified by
 501    OPTIONS.  The default failure verbosity level is 2.
 502
 503    The failure verbosity level has an effect only when an error
 504    is reported, and only when the failure verbosity level is
 505    higher than the regular verbosity level.  When this is the
 506    case, the model checker replays the error path at the higher
 507    verbosity level specified.  This has the effect of outputting
 508    an explicit, human-readable description of the sequence of
 509    operations that caused the error. */
 510 int
 511 mc_options_get_failure_verbosity (const struct mc_options *options)
 512 {
 513   return options->failure_verbosity;
 514 }
 515
 516 /* Sets the level of verbosity for failures specified by OPTIONS
 517    to FAILURE_VERBOSITY. */
 518 void
 519 mc_options_set_failure_verbosity (struct mc_options *options,
 520                                   int failure_verbosity)
 521 {
 522   options->failure_verbosity = failure_verbosity;
 523 }
 524
 525 /* Returns the output file used for messages printed by the model
 526    checker specified by OPTIONS.  The default is stdout. */
 527 FILE *
 528 mc_options_get_output_file (const struct mc_options *options)
 529 {
 530   return options->output_file;
 531 }
 532
 533 /* Sets the output file used for messages printed by the model
 534    checker specified by OPTIONS to OUTPUT_FILE.
 535
 536    The model checker does not automatically close the specified
 537    output file.  If this is desired, the model checker's client
 538    must do so. */
 539 void
 540 mc_options_set_output_file (struct mc_options *options,
 541                             FILE *output_file)
 542 {
 543   options->output_file = output_file;
 544 }
 545
 546 /* Returns the number of microseconds between calls to the
 547    progress function specified by OPTIONS.   The default is
 548    250,000 (1/4 second).  A value of 0 disables progress
 549    reporting. */
 550 int
 551 mc_options_get_progress_usec (const struct mc_options *options)
 552 {
 553   return options->progress_usec;
 554 }
 555
 556 /* Sets the number of microseconds between calls to the progress
 557    function specified by OPTIONS to PROGRESS_USEC.  A value of 0
 558    disables progress reporting. */
 559 void
 560 mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
 561 {
 562   assert (progress_usec >= 0);
 563   options->progress_usec = progress_usec;
 564 }
 565
 566 /* Returns the function called to report progress specified by
 567    OPTIONS.  The function used by default prints '.' to
 568    stderr. */
 569 mc_progress_func *
 570 mc_options_get_progress_func (const struct mc_options *options)
 571 {
 572   return options->progress_func;
 573 }
 574
 575 /* Sets the function called to report progress specified by
 576    OPTIONS to PROGRESS_FUNC.  A non-null function must be
 577    specified; to disable progress reporting, set the progress
 578    reporting interval to 0.
 579
 580    PROGRESS_FUNC will be called zero or more times while the
 581    model checker's run is ongoing.  For these calls to the
 582    progress function, mc_results_get_stop_reason will return
 583    MC_CONTINUING.  It will also be called exactly once soon
 584    before mc_run returns, in which case
 585    mc_results_get_stop_reason will return a different value. */
 586 void
 587 mc_options_set_progress_func (struct mc_options *options,
 588                               mc_progress_func *progress_func)
 589 {
 590   assert (options->progress_func != NULL);
 591   options->progress_func = progress_func;
 592 }
 593
 594 /* Returns the auxiliary data set in OPTIONS by the client.  The
 595    default is a null pointer.
 596
 597    This auxiliary data value can be retrieved by the
 598    client-specified functions in struct mc_class during a model
 599    checking run using mc_get_aux. */
 600 void *
 601 mc_options_get_aux (const struct mc_options *options)
 602 {
 603   return options->aux;
 604 }
 605
 606 /* Sets the auxiliary data in OPTIONS to AUX. */
 607 void
 608 mc_options_set_aux (struct mc_options *options, void *aux)
 609 {
 610   options->aux = aux;
 611 }
 612 \f
 613 /* Results of a model checking run. */
 614 struct mc_results
 615   {
 616     /* Overall results. */
 617     enum mc_stop_reason stop_reason;    /* Why the run ended. */
 618     int unique_state_count;             /* Number of unique states checked. */
 619     int error_count;                    /* Number of errors found. */
 620
 621     /* Depth statistics. */
 622     int max_depth_reached;              /* Max depth state examined. */
 623     struct moments1 *depth_moments;     /* Enables reporting mean depth. */
 624
 625     /* If error_count > 0, path to the last error reported. */
 626     struct mc_path error_path;
 627
 628     /* States dropped... */
 629     int duplicate_dropped_states;       /* ...as duplicates. */
 630     int off_path_dropped_states;        /* ...as off-path (MC_PATH only). */
 631     int depth_dropped_states;           /* ...due to excessive depth. */
 632     int queue_dropped_states;           /* ...due to queue overflow. */
 633
 634     /* Queue statistics. */
 635     int queued_unprocessed_states;      /* Enqueued but never dequeued. */
 636     int max_queue_length;               /* Maximum queue length observed. */
 637
 638     /* Timing. */
 639     struct timeval start;               /* Start of model checking run. */
 640     struct timeval end;                 /* End of model checking run. */
 641   };
 642
 643 /* Creates, initializes, and returns a new set of results. */
 644 static struct mc_results *
 645 mc_results_create (void)
 646 {
 647   struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
 648   results->stop_reason = MC_CONTINUING;
 649   results->depth_moments = moments1_create (MOMENT_MEAN);
 650   gettimeofday (&results->start, NULL);
 651   return results;
 652 }
 653
 654 /* Destroys RESULTS. */
 655 void
 656 mc_results_destroy (struct mc_results *results)
 657 {
 658   if (results != NULL)
 659     {
 660       moments1_destroy (results->depth_moments);
 661       mc_path_destroy (&results->error_path);
 662       free (results);
 663     }
 664 }
 665
 666 /* Returns RESULTS's reason that the model checking run
 667    terminated.  The possible reasons are:
 668
 669    - MC_CONTINUING: The run is not actually yet complete.  This
 670      can only be returned before mc_run has returned, e.g. when
 671      the progress function set by mc_options_set_progress_func
 672      examines the run's results.
 673
 674    - MC_SUCCESS: The run completed because the queue emptied.
 675      The entire state space might not have been explored due to a
 676      requested limit on maximum depth, hash collisions, etc.
 677
 678    - MC_MAX_UNIQUE_STATES: The run completed because as many
 679      unique states have been checked as were requested (using
 680      mc_options_set_max_unique_states).
 681
 682    - MC_MAX_ERROR_COUNT: The run completed because the maximum
 683      requested number of errors (by default, 1 error) was
 684      reached.
 685
 686    - MC_END_OF_PATH: The run completed because the path specified
 687      with mc_options_set_follow_path was fully traversed.
 688
 689    - MC_TIMEOUT: The run completed because the time limit set
 690      with mc_options_set_time_limit was exceeded.
 691
 692    - MC_INTERRUPTED: The run completed because SIGINT was caught
 693      (typically, due to the user typing Ctrl+C). */
 694 enum mc_stop_reason
 695 mc_results_get_stop_reason (const struct mc_results *results)
 696 {
 697   return results->stop_reason;
 698 }
 699
 700 /* Returns the number of unique states checked specified by
 701    RESULTS. */
 702 int
 703 mc_results_get_unique_state_count (const struct mc_results *results)
 704 {
 705   return results->unique_state_count;
 706 }
 707
 708 /* Returns the number of errors found specified by RESULTS. */
 709 int
 710 mc_results_get_error_count (const struct mc_results *results)
 711 {
 712   return results->error_count;
 713 }
 714
 715 /* Returns the maximum depth reached during the model checker run
 716    represented by RESULTS.  The initial states are at depth 1,
 717    their child states at depth 2, and so on. */
 718 int
 719 mc_results_get_max_depth_reached (const struct mc_results *results)
 720 {
 721   return results->max_depth_reached;
 722 }
 723
 724 /* Returns the mean depth reached during the model checker run
 725    represented by RESULTS. */
 726 double
 727 mc_results_get_mean_depth_reached (const struct mc_results *results)
 728 {
 729   double mean;
 730   moments1_calculate (results->depth_moments, NULL, &mean, NULL, NULL, NULL);
 731   return mean != SYSMIS ? mean : 0.0;
 732 }
 733
 734 /* Returns the path traversed to obtain the last error
 735    encountered during the model checker run represented by
 736    RESULTS.  Returns a null pointer if the run did not report any
 737    errors. */
 738 const struct mc_path *
 739 mc_results_get_error_path (const struct mc_results *results)
 740 {
 741   return results->error_count > 0 ? &results->error_path : NULL;
 742 }
 743
 744 /* Returns the number of states dropped as duplicates (based on
 745    hash value) during the model checker run represented by
 746    RESULTS. */
 747 int
 748 mc_results_get_duplicate_dropped_states (const struct mc_results *results)
 749 {
 750   return results->duplicate_dropped_states;
 751 }
 752
 753 /* Returns the number of states dropped because they were off the
 754    path specified by mc_options_set_follow_path during the model
 755    checker run represented by RESULTS.  A nonzero value here
 756    indicates a missing call to mc_include_state in the
 757    client-supplied mutation function. */
 758 int
 759 mc_results_get_off_path_dropped_states (const struct mc_results *results)
 760 {
 761   return results->off_path_dropped_states;
 762 }
 763
 764 /* Returns the number of states dropped because their depth
 765    exceeded the maximum specified with mc_options_set_max_depth
 766    during the model checker run represented by RESULTS. */
 767 int
 768 mc_results_get_depth_dropped_states (const struct mc_results *results)
 769 {
 770   return results->depth_dropped_states;
 771 }
 772
 773 /* Returns the number of states dropped from the queue due to
 774    queue overflow during the model checker run represented by
 775    RESULTS. */
 776 int
 777 mc_results_get_queue_dropped_states (const struct mc_results *results)
 778 {
 779   return results->queue_dropped_states;
 780 }
 781
 782 /* Returns the number of states that were checked and enqueued
 783    but never dequeued and processed during the model checker run
 784    represented by RESULTS.  This is zero if the stop reason is
 785    MC_CONTINUING or MC_SUCCESS; otherwise, it is the number of
 786    states in the queue at the time that the checking run
 787    stopped. */
 788 int
 789 mc_results_get_queued_unprocessed_states (const struct mc_results *results)
 790 {
 791   return results->queued_unprocessed_states;
 792 }
 793
 794 /* Returns the maximum length of the queue during the model
 795    checker run represented by RESULTS.  If this is equal to the
 796    maximum queue length, then the queue (probably) overflowed
 797    during the run; otherwise, it did not overflow. */
 798 int
 799 mc_results_get_max_queue_length (const struct mc_results *results)
 800 {
 801   return results->max_queue_length;
 802 }
 803
 804 /* Returns the time at which the model checker run represented by
 805    RESULTS started. */
 806 struct timeval
 807 mc_results_get_start (const struct mc_results *results)
 808 {
 809   return results->start;
 810 }
 811
 812 /* Returns the time at which the model checker run represented by
 813    RESULTS ended.  (This function may not be called while the run
 814    is still ongoing.) */
 815 struct timeval
 816 mc_results_get_end (const struct mc_results *results)
 817 {
 818   assert (results->stop_reason != MC_CONTINUING);
 819   return results->end;
 820 }
 821
 822 /* Returns the number of seconds obtained by subtracting time Y
 823    from time X. */
 824 static double
 825 timeval_subtract (struct timeval x, struct timeval y)
 826 {
 827   /* From libc.info. */
 828   double difference;
 829
 830   /* Perform the carry for the later subtraction by updating Y. */
 831   if (x.tv_usec < y.tv_usec) {
 832     int nsec = (y.tv_usec - x.tv_usec) / 1000000 + 1;
 833     y.tv_usec -= 1000000 * nsec;
 834     y.tv_sec += nsec;
 835   }
 836   if (x.tv_usec - y.tv_usec > 1000000) {
 837     int nsec = (x.tv_usec - y.tv_usec) / 1000000;
 838     y.tv_usec += 1000000 * nsec;
 839     y.tv_sec -= nsec;
 840   }
 841
 842   /* Compute the time remaining to wait.
 843      `tv_usec' is certainly positive. */
 844   difference = (x.tv_sec - y.tv_sec) + (x.tv_usec - y.tv_usec) / 1000000.0;
 845   if (x.tv_sec < y.tv_sec)
 846     difference = -difference;
 847   return difference;
 848 }
 849
 850
 851 /* Returns the duration, in seconds, of the model checker run
 852    represented by RESULTS.  (This function may not be called
 853    while the run is still ongoing.) */
 854 double
 855 mc_results_get_duration (const struct mc_results *results)
 856 {
 857   assert (results->stop_reason != MC_CONTINUING);
 858   return timeval_subtract (results->end, results->start);
 859 }
 860 \f
 861 /* An active model checking run. */
 862 struct mc
 863   {
 864     /* Related data structures. */
 865     const struct mc_class *class;
 866     struct mc_options *options;
 867     struct mc_results *results;
 868
 869     /* Array of 2**(options->hash_bits) bits representing states
 870        already visited. */
 871     unsigned char *hash;
 872
 873     /* State queue. */
 874     struct mc_state **queue;            /* Array of pointers to states. */
 875     struct deque queue_deque;           /* Deque. */
 876
 877     /* State currently being built by "init" or "mutate". */
 878     struct mc_path path;                /* Path to current state. */
 879     struct string path_string;          /* Buffer for path_string function. */
 880     bool state_named;                   /* mc_name_operation called? */
 881     bool state_error;                   /* mc_error called? */
 882
 883     /* Statistics for calling the progress function. */
 884     unsigned int progress;              /* Current progress value. */
 885     unsigned int next_progress;         /* Next value to call progress func. */
 886     unsigned int prev_progress;         /* Last value progress func called. */
 887     struct timeval prev_progress_time;  /* Last time progress func called. */
 888
 889     /* Information for handling and restoring SIGINT. */
 890     bool interrupted;                   /* SIGINT received? */
 891     bool *saved_interrupted_ptr;        /* Saved value of interrupted_ptr. */
 892     void (*saved_sigint) (int);         /* Saved SIGINT handler. */
 893   };
 894
 895 /* A state in the queue. */
 896 struct mc_state
 897   {
 898     struct mc_path path;                /* Path to this state. */
 899     void *data;                         /* Client-supplied data. */
 900   };
 901
 902 /* Points to the current struct mc's "interrupted" member. */
 903 static bool *interrupted_ptr = NULL;
 904
 905 static const char *path_string (struct mc *);
 906 static void free_state (const struct mc *, struct mc_state *);
 907 static void stop (struct mc *, enum mc_stop_reason);
 908 static struct mc_state *make_state (const struct mc *, void *);
 909 static size_t random_queue_index (struct mc *);
 910 static void enqueue_state (struct mc *, struct mc_state *);
 911 static void do_error_state (struct mc *);
 912 static void next_operation (struct mc *);
 913 static bool is_off_path (const struct mc *);
 914 static void sigint_handler (int signum);
 915 static void init_mc (struct mc *,
 916                      const struct mc_class *, struct mc_options *);
 917 static void finish_mc (struct mc *);
 918
 919 /* Runs the model checker on the client-specified CLASS with the
 920    client-specified OPTIONS.  OPTIONS may be a null pointer if
 921    the defaults are acceptable.  Destroys OPTIONS; use
 922    mc_options_clone if a copy is needed.
 923
 924    Returns the results of the model checking run, which must be
 925    destroyed by the client with mc_results_destroy.
 926
 927    To pass auxiliary data to the functions in CLASS, use
 928    mc_options_set_aux on OPTIONS, which may be retrieved from the
 929    CLASS functions using mc_get_aux. */
 930 struct mc_results *
 931 mc_run (const struct mc_class *class, struct mc_options *options)
 932 {
 933   struct mc mc;
 934
 935   init_mc (&mc, class, options);
 936   while (!deque_is_empty (&mc.queue_deque)
 937          && mc.results->stop_reason == MC_CONTINUING)
 938     {
 939       struct mc_state *state = mc.queue[deque_pop_front (&mc.queue_deque)];
 940       mc_path_copy (&mc.path, &state->path);
 941       mc_path_push (&mc.path, 0);
 942       class->mutate (&mc, state->data);
 943       free_state (&mc, state);
 944       if (mc.interrupted)
 945         stop (&mc, MC_INTERRUPTED);
 946     }
 947   finish_mc (&mc);
 948
 949   return mc.results;
 950 }
 951
 952 /* Tests whether the current operation is one that should be
 953    performed, checked, and enqueued.  If so, returns true.
 954    Otherwise, returns false and, unless checking is stopped,
 955    advances to the next state.  The caller should then advance
 956    to the next operation.
 957
 958    This function should be called from the client-provided
 959    "mutate" function, according to the pattern explained in the
 960    big comment at the top of model-checker.h. */
 961 bool
 962 mc_include_state (struct mc *mc)
 963 {
 964   if (mc->results->stop_reason != MC_CONTINUING)
 965     return false;
 966   else if (is_off_path (mc))
 967     {
 968       next_operation (mc);
 969       return false;
 970     }
 971   else
 972     return true;
 973 }
 974
 975 /* Tests whether HASH represents a state that has (probably)
 976    already been enqueued.  If not, returns false and marks HASH
 977    so that it will be treated as a duplicate in the future.  If
 978    so, returns true and advances to the next state.  The
 979    caller should then advance to the next operation.
 980
 981    This function should be called from the client-provided
 982    "mutate" function, according to the pattern explained in the
 983    big comment at the top of model-checker.h. */
 984 bool
 985 mc_discard_dup_state (struct mc *mc, unsigned int hash)
 986 {
 987   if (mc->options->hash_bits > 0)
 988     {
 989       hash &= (1u << mc->options->hash_bits) - 1;
 990       if (TEST_BIT (mc->hash, hash))
 991         {
 992           if (mc->options->verbosity > 2)
 993             fprintf (mc->options->output_file,
 994                      "    [%s] discard duplicate state\n", path_string (mc));
 995           mc->results->duplicate_dropped_states++;
 996           next_operation (mc);
 997           return true;
 998         }
 999       SET_BIT (mc->hash, hash);
1000     }
1001   return false;
1002 }
1003
1004 /* Names the current state NAME, which may contain
1005    printf-style format specifications.  NAME should be a
1006    human-readable name for the current operation.
1007
1008    This function should be called from the client-provided
1009    "mutate" function, according to the pattern explained in the
1010    big comment at the top of model-checker.h. */
1011 void
1012 mc_name_operation (struct mc *mc, const char *name, ...)
1013 {
1014   va_list args;
1015
1016   va_start (args, name);
1017   mc_vname_operation (mc, name, args);
1018   va_end (args);
1019 }
1020
1021 /* Names the current state NAME, which may contain
1022    printf-style format specifications, for which the
1023    corresponding arguments must be given in ARGS.  NAME should be
1024    a human-readable name for the current operation.
1025
1026    This function should be called from the client-provided
1027    "mutate" function, according to the pattern explained in the
1028    big comment at the top of model-checker.h. */
1029 void
1030 mc_vname_operation (struct mc *mc, const char *name, va_list args)
1031 {
1032   if (mc->state_named && mc->options->verbosity > 0)
1033     fprintf (mc->options->output_file, "  [%s] warning: duplicate call "
1034              "to mc_name_operation (missing call to mc_add_state?)\n",
1035              path_string (mc));
1036   mc->state_named = true;
1037
1038   if (mc->options->verbosity > 1)
1039     {
1040       fprintf (mc->options->output_file, "  [%s] ", path_string (mc));
1041       vfprintf (mc->options->output_file, name, args);
1042       putc ('\n', mc->options->output_file);
1043     }
1044 }
1045
1046 /* Reports the given error MESSAGE for the current operation.
1047    The resulting state should still be passed to mc_add_state
1048    when all relevant error messages have been issued.  The state
1049    will not, however, be enqueued for later mutation of its own.
1050
1051    By default, model checking stops after the first error
1052    encountered.
1053
1054    This function should be called from the client-provided
1055    "mutate" function, according to the pattern explained in the
1056    big comment at the top of model-checker.h. */
1057 void
1058 mc_error (struct mc *mc, const char *message, ...)
1059 {
1060   va_list args;
1061
1062   if (mc->results->stop_reason != MC_CONTINUING)
1063     return;
1064
1065   if (mc->options->verbosity > 1)
1066     fputs ("    ", mc->options->output_file);
1067   fprintf (mc->options->output_file, "[%s] error: ",
1068            path_string (mc));
1069   va_start (args, message);
1070   vfprintf (mc->options->output_file, message, args);
1071   va_end (args);
1072   putc ('\n', mc->options->output_file);
1073
1074   mc->state_error = true;
1075 }
1076
1077 /* Enqueues DATA as the state corresponding to the current
1078    operation.  The operation should have been named with a call
1079    to mc_name_operation, and it should have been checked by the
1080    caller (who should have reported any errors with mc_error).
1081
1082    This function should be called from the client-provided
1083    "mutate" function, according to the pattern explained in the
1084    big comment at the top of model-checker.h. */
1085 void
1086 mc_add_state (struct mc *mc, void *data)
1087 {
1088   if (!mc->state_named && mc->options->verbosity > 0)
1089     fprintf (mc->options->output_file, "  [%s] warning: unnamed state\n",
1090              path_string (mc));
1091
1092   if (mc->results->stop_reason != MC_CONTINUING)
1093     {
1094       /* Nothing to do. */
1095     }
1096   else if (mc->state_error)
1097     do_error_state (mc);
1098   else if (is_off_path (mc))
1099     mc->results->off_path_dropped_states++;
1100   else if (mc->path.length + 1 > mc->options->max_depth)
1101     mc->results->depth_dropped_states++;
1102   else
1103     {
1104       /* This is the common case. */
1105       mc->results->unique_state_count++;
1106       if (mc->results->unique_state_count >= mc->options->max_unique_states)
1107         stop (mc, MC_MAX_UNIQUE_STATES);
1108       enqueue_state (mc, make_state (mc, data));
1109       next_operation (mc);
1110       return;
1111     }
1112
1113   mc->class->destroy (mc, data);
1114   next_operation (mc);
1115 }
1116
1117 /* Returns the options that were passed to mc_run for model
1118    checker MC. */
1119 const struct mc_options *
1120 mc_get_options (const struct mc *mc)
1121 {
1122   return mc->options;
1123 }
1124
1125 /* Returns the current state of the results for model checker
1126    MC.  This function is appropriate for use from the progress
1127    function set by mc_options_set_progress_func.
1128
1129    Not all of the results are meaningful before model checking
1130    completes. */
1131 const struct mc_results *
1132 mc_get_results (const struct mc *mc)
1133 {
1134   return mc->results;
1135 }
1136
1137 /* Returns the auxiliary data set on the options passed to mc_run
1138    with mc_options_set_aux. */
1139 void *
1140 mc_get_aux (const struct mc *mc)
1141 {
1142   return mc_options_get_aux (mc_get_options (mc));
1143 }
1144 \f
1145 /* Expresses MC->path as a string and returns the string. */
1146 static const char *
1147 path_string (struct mc *mc)
1148 {
1149   ds_clear (&mc->path_string);
1150   mc_path_to_string (&mc->path, &mc->path_string);
1151   return ds_cstr (&mc->path_string);
1152 }
1153
1154 /* Frees STATE, including client data. */
1155 static void
1156 free_state (const struct mc *mc, struct mc_state *state)
1157 {
1158   mc->class->destroy (mc, state->data);
1159   mc_path_destroy (&state->path);
1160   free (state);
1161 }
1162
1163 /* Sets STOP_REASON as the reason that MC's processing stopped,
1164    unless MC is already stopped. */
1165 static void
1166 stop (struct mc *mc, enum mc_stop_reason stop_reason)
1167 {
1168   if (mc->results->stop_reason == MC_CONTINUING)
1169     mc->results->stop_reason = stop_reason;
1170 }
1171
1172 /* Creates and returns a new state whose path is copied from
1173    MC->path and whose data is specified by DATA. */
1174 static struct mc_state *
1175 make_state (const struct mc *mc, void *data)
1176 {
1177   struct mc_state *new = xmalloc (sizeof *new);
1178   mc_path_init (&new->path);
1179   mc_path_copy (&new->path, &mc->path);
1180   new->data = data;
1181   return new;
1182 }
1183
1184 /* Returns the index in MC->queue of a random element in the
1185    queue. */
1186 static size_t
1187 random_queue_index (struct mc *mc)
1188 {
1189   assert (!deque_is_empty (&mc->queue_deque));
1190   return deque_front (&mc->queue_deque,
1191                       rand () % deque_count (&mc->queue_deque));
1192 }
1193
1194 /* Adds NEW to MC's state queue, dropping a state if necessary
1195    due to overflow. */
1196 static void
1197 enqueue_state (struct mc *mc, struct mc_state *new)
1198 {
1199   size_t idx;
1200
1201   if (new->path.length > mc->results->max_depth_reached)
1202     mc->results->max_depth_reached = new->path.length;
1203   moments1_add (mc->results->depth_moments, new->path.length, 1.0);
1204
1205   if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
1206     {
1207       /* Add new state to queue. */
1208       if (deque_is_full (&mc->queue_deque))
1209         mc->queue = deque_expand (&mc->queue_deque,
1210                                    mc->queue, sizeof *mc->queue);
1211       switch (mc->options->strategy)
1212         {
1213         case MC_BROAD:
1214           idx = deque_push_back (&mc->queue_deque);
1215           break;
1216         case MC_DEEP:
1217           idx = deque_push_front (&mc->queue_deque);
1218           break;
1219         case MC_RANDOM:
1220           if (!deque_is_empty (&mc->queue_deque))
1221             {
1222               idx = random_queue_index (mc);
1223               mc->queue[deque_push_front (&mc->queue_deque)]
1224                 = mc->queue[idx];
1225             }
1226           else
1227             idx = deque_push_front (&mc->queue_deque);
1228           break;
1229         case MC_PATH:
1230           assert (deque_is_empty (&mc->queue_deque));
1231           assert (!is_off_path (mc));
1232           idx = deque_push_back (&mc->queue_deque);
1233           if (mc->path.length
1234               >= mc_path_get_length (&mc->options->follow_path))
1235             stop (mc, MC_END_OF_PATH);
1236           break;
1237         default:
1238           NOT_REACHED ();
1239         }
1240       if (deque_count (&mc->queue_deque) > mc->results->max_queue_length)
1241         mc->results->max_queue_length = deque_count (&mc->queue_deque);
1242     }
1243   else
1244     {
1245       /* Queue has reached limit, so replace an existing
1246          state. */
1247       assert (mc->options->strategy != MC_PATH);
1248       assert (!deque_is_empty (&mc->queue_deque));
1249       mc->results->queue_dropped_states++;
1250       switch (mc->options->queue_limit_strategy)
1251         {
1252         case MC_DROP_NEWEST:
1253           free_state (mc, new);
1254           return;
1255         case MC_DROP_OLDEST:
1256           switch (mc->options->strategy)
1257             {
1258             case MC_BROAD:
1259               idx = deque_front (&mc->queue_deque, 0);
1260               break;
1261             case MC_DEEP:
1262               idx = deque_back (&mc->queue_deque, 0);
1263               break;
1264             case MC_RANDOM:
1265             case MC_PATH:
1266             default:
1267               NOT_REACHED ();
1268             }
1269           break;
1270         case MC_DROP_RANDOM:
1271           idx = random_queue_index (mc);
1272           break;
1273         default:
1274           NOT_REACHED ();
1275         }
1276       free_state (mc, mc->queue[idx]);
1277     }
1278   mc->queue[idx] = new;
1279 }
1280
1281 /* Process an error state being added to MC. */
1282 static void
1283 do_error_state (struct mc *mc)
1284 {
1285   mc->results->error_count++;
1286   if (mc->results->error_count >= mc->options->max_errors)
1287     stop (mc, MC_MAX_ERROR_COUNT);
1288
1289   mc_path_copy (&mc->results->error_path, &mc->path);
1290
1291   if (mc->options->failure_verbosity > mc->options->verbosity)
1292     {
1293       struct mc_options *path_options;
1294
1295       fprintf (mc->options->output_file, "[%s] retracing error path:\n",
1296                path_string (mc));
1297       path_options = mc_options_clone (mc->options);
1298       mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
1299       mc_options_set_failure_verbosity (path_options, 0);
1300       mc_options_set_follow_path (path_options, &mc->path);
1301
1302       mc_results_destroy (mc_run (mc->class, path_options));
1303
1304       putc ('\n', mc->options->output_file);
1305     }
1306 }
1307
1308 /* Advances MC to start processing the operation following the
1309    current one. */
1310 static void
1311 next_operation (struct mc *mc)
1312 {
1313   mc_path_push (&mc->path, mc_path_pop (&mc->path) + 1);
1314   mc->state_error = false;
1315   mc->state_named = false;
1316
1317   if (++mc->progress >= mc->next_progress)
1318     {
1319       struct timeval now;
1320       double elapsed, delta;
1321
1322       if (mc->results->stop_reason == MC_CONTINUING
1323           && !mc->options->progress_func (mc))
1324         stop (mc, MC_INTERRUPTED);
1325
1326       gettimeofday (&now, NULL);
1327
1328       if (mc->options->time_limit > 0.0
1329           && (timeval_subtract (now, mc->results->start)
1330               > mc->options->time_limit))
1331         stop (mc, MC_TIMEOUT);
1332
1333       elapsed = timeval_subtract (now, mc->prev_progress_time);
1334       if (elapsed > 0.0)
1335         {
1336           /* Re-estimate the amount of progress to take
1337              progress_usec microseconds. */
1338           unsigned int progress = mc->progress - mc->prev_progress;
1339           double progress_sec = mc->options->progress_usec / 1000000.0;
1340           delta = progress / elapsed * progress_sec;
1341         }
1342       else
1343         {
1344           /* No measurable time at all elapsed during that amount
1345              of progress.  Try doubling the amount of progress
1346              required. */
1347           delta = (mc->progress - mc->prev_progress) * 2;
1348         }
1349
1350       if (delta > 0.0 && delta + mc->progress + 1.0 < UINT_MAX)
1351         mc->next_progress = mc->progress + delta + 1.0;
1352       else
1353         mc->next_progress = mc->progress + (mc->progress - mc->prev_progress);
1354
1355       mc->prev_progress = mc->progress;
1356       mc->prev_progress_time = now;
1357     }
1358 }
1359
1360 /* Returns true if we're tracing an explicit path but the current
1361    operation produces a state off that path, false otherwise. */
1362 static bool
1363 is_off_path (const struct mc *mc)
1364 {
1365   return (mc->options->strategy == MC_PATH
1366           && (mc_path_back (&mc->path)
1367               != mc_path_get_operation (&mc->options->follow_path,
1368                                         mc->path.length - 1)));
1369 }
1370
1371 /* Handler for SIGINT. */
1372 static void
1373 sigint_handler (int signum UNUSED)
1374 {
1375   /* Just mark the model checker as interrupted. */
1376   *interrupted_ptr = true;
1377 }
1378
1379 /* Initializes MC as a model checker with the given CLASS and
1380    OPTIONS.  OPTIONS may be null to use the default options. */
1381 static void
1382 init_mc (struct mc *mc, const struct mc_class *class,
1383          struct mc_options *options)
1384 {
1385   /* Validate and adjust OPTIONS. */
1386   if (options == NULL)
1387     options = mc_options_create ();
1388   assert (options->queue_limit_strategy != MC_DROP_OLDEST
1389           || options->strategy != MC_RANDOM);
1390   if (options->strategy == MC_PATH)
1391     {
1392       options->max_depth = INT_MAX;
1393       options->hash_bits = 0;
1394     }
1395   if (options->progress_usec == 0)
1396     {
1397       options->progress_func = null_progress;
1398       if (options->time_limit > 0.0)
1399         options->progress_usec = 250000;
1400     }
1401
1402   /* Initialize MC. */
1403   mc->class = class;
1404   mc->options = options;
1405   mc->results = mc_results_create ();
1406
1407   mc->hash = (mc->options->hash_bits > 0
1408               ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT))
1409               : NULL);
1410
1411   mc->queue = NULL;
1412   deque_init_null (&mc->queue_deque);
1413
1414   mc_path_init (&mc->path);
1415   mc_path_push (&mc->path, 0);
1416   ds_init_empty (&mc->path_string);
1417   mc->state_named = false;
1418   mc->state_error = false;
1419
1420   mc->progress = 0;
1421   mc->next_progress = mc->options->progress_usec != 0 ? 100 : UINT_MAX;
1422   mc->prev_progress = 0;
1423   mc->prev_progress_time = mc->results->start;
1424
1425   if (mc->options->strategy == MC_RANDOM
1426       || options->queue_limit_strategy == MC_DROP_RANDOM)
1427     srand (mc->options->seed);
1428
1429   mc->interrupted = false;
1430   mc->saved_interrupted_ptr = interrupted_ptr;
1431   interrupted_ptr = &mc->interrupted;
1432   mc->saved_sigint = signal (SIGINT, sigint_handler);
1433
1434   class->init (mc);
1435 }
1436
1437 /* Complete the model checker run for MC. */
1438 static void
1439 finish_mc (struct mc *mc)
1440 {
1441   /* Restore signal handlers. */
1442   signal (SIGINT, mc->saved_sigint);
1443   interrupted_ptr = mc->saved_interrupted_ptr;
1444
1445   /* Mark the run complete. */
1446   stop (mc, MC_SUCCESS);
1447   gettimeofday (&mc->results->end, NULL);
1448
1449   /* Empty the queue. */
1450   mc->results->queued_unprocessed_states = deque_count (&mc->queue_deque);
1451   while (!deque_is_empty (&mc->queue_deque))
1452     {
1453       struct mc_state *state = mc->queue[deque_pop_front (&mc->queue_deque)];
1454       free_state (mc, state);
1455     }
1456
1457   /* Notify the progress function of completion. */
1458   mc->options->progress_func (mc);
1459
1460   /* Free memory. */
1461   mc_path_destroy (&mc->path);
1462   ds_destroy (&mc->path_string);
1463   free (mc->options);
1464   free (mc->queue);
1465   free (mc->hash);
1466 }