1 /* PSPP - a program for statistical analysis.
2 Copyright (C) 2007, 2009 Free Software Foundation, Inc.
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.
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.
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/>. */
19 #include <libpspp/model-checker.h>
29 #include <libpspp/bit-vector.h>
30 #include <libpspp/compiler.h>
31 #include <libpspp/deque.h>
32 #include <libpspp/misc.h>
33 #include <libpspp/str.h>
39 /* Initializes PATH as an empty path. */
41 mc_path_init (struct mc_path *path)
48 /* Copies the contents of OLD into NEW. */
50 mc_path_copy (struct mc_path *new, const struct mc_path *old)
52 if (old->length > new->capacity)
54 new->capacity = old->length;
56 new->ops = xnmalloc (new->capacity, sizeof *new->ops);
58 new->length = old->length;
59 memcpy (new->ops, old->ops, old->length * sizeof *new->ops);
62 /* Adds OP to the end of PATH. */
64 mc_path_push (struct mc_path *path, int op)
66 if (path->length >= path->capacity)
67 path->ops = xnrealloc (path->ops, ++path->capacity, sizeof *path->ops);
68 path->ops[path->length++] = op;
71 /* Removes and returns the operation at the end of PATH. */
73 mc_path_pop (struct mc_path *path)
75 int back = mc_path_back (path);
80 /* Returns the operation at the end of PATH. */
82 mc_path_back (const struct mc_path *path)
84 assert (path->length > 0);
85 return path->ops[path->length - 1];
90 mc_path_destroy (struct mc_path *path)
96 /* Returns the operation in position INDEX in PATH.
97 INDEX must be less than the length of PATH. */
99 mc_path_get_operation (const struct mc_path *path, size_t index)
101 assert (index < path->length);
102 return path->ops[index];
105 /* Returns the number of operations in PATH. */
107 mc_path_get_length (const struct mc_path *path)
112 /* Appends the operations in PATH to STRING, separating each one
113 with a single space. */
115 mc_path_to_string (const struct mc_path *path, struct string *string)
119 for (i = 0; i < mc_path_get_length (path); i++)
122 ds_put_char (string, ' ');
123 ds_put_format (string, "%d", mc_path_get_operation (path, i));
127 /* Search options. */
130 /* Search strategy. */
131 enum mc_strategy strategy; /* Type of strategy. */
132 int max_depth; /* Limit on depth (or INT_MAX). */
133 int hash_bits; /* Number of bits to hash (or 0). */
134 unsigned int seed; /* Random seed for MC_RANDOM
135 or MC_DROP_RANDOM. */
136 struct mc_path follow_path; /* Path for MC_PATH. */
138 /* Queue configuration. */
139 int queue_limit; /* Maximum length of queue. */
140 enum mc_queue_limit_strategy queue_limit_strategy;
141 /* How to choose state to drop
144 /* Stop conditions. */
145 int max_unique_states; /* Maximum unique states to process. */
146 int max_errors; /* Maximum errors to detect. */
147 double time_limit; /* Maximum time in seconds. */
149 /* Output configuration. */
150 int verbosity; /* 0=low, 1=normal, 2+=high. */
151 int failure_verbosity; /* If greater than verbosity,
152 verbosity of error replays. */
153 FILE *output_file; /* File to receive output. */
155 /* How to report intermediate progress. */
156 int progress_usec; /* Microseconds between reports. */
157 mc_progress_func *progress_func; /* Function to call on each report. */
163 /* Default progress function. */
165 mc_progress_dots (struct mc *mc)
167 if (mc_results_get_stop_reason (mc_get_results (mc)) == MC_CONTINUING)
174 /* Progress function that prints a one-line summary of the
175 current state on stderr. */
177 mc_progress_fancy (struct mc *mc)
179 const struct mc_results *results = mc_get_results (mc);
180 if (mc_results_get_stop_reason (results) == MC_CONTINUING)
181 fprintf (stderr, "Processed %d unique states, max depth %d, "
182 "dropped %d duplicates...\r",
183 mc_results_get_unique_state_count (results),
184 mc_results_get_max_depth_reached (results),
185 mc_results_get_duplicate_dropped_states (results));
191 /* Progress function that displays a detailed summary of the
192 current state on stderr. */
194 mc_progress_verbose (struct mc *mc)
196 const struct mc_results *results = mc_get_results (mc);
198 /* VT100 clear screen and home cursor. */
199 fprintf (stderr, "\033[H\033[2J");
201 if (mc_results_get_stop_reason (results) == MC_CONTINUING)
202 mc_results_print (results, stderr);
207 /* Do-nothing progress function. */
209 null_progress (struct mc *mc UNUSED)
214 /* Creates and returns a set of options initialized to the
217 mc_options_create (void)
219 struct mc_options *options = xmalloc (sizeof *options);
221 options->strategy = MC_BROAD;
222 options->max_depth = INT_MAX;
223 options->hash_bits = 20;
225 mc_path_init (&options->follow_path);
227 options->queue_limit = 10000;
228 options->queue_limit_strategy = MC_DROP_RANDOM;
230 options->max_unique_states = INT_MAX;
231 options->max_errors = 1;
232 options->time_limit = 0.0;
234 options->verbosity = 1;
235 options->failure_verbosity = 2;
236 options->output_file = stdout;
237 options->progress_usec = 250000;
238 options->progress_func = mc_progress_dots;
245 /* Returns a copy of the given OPTIONS. */
247 mc_options_clone (const struct mc_options *options)
249 return xmemdup (options, sizeof *options);
252 /* Destroys OPTIONS. */
254 mc_options_destroy (struct mc_options *options)
256 mc_path_destroy (&options->follow_path);
260 /* Returns the search strategy used for OPTIONS. The choices
263 - MC_BROAD (the default): Breadth-first search. First tries
264 all the operations with depth 1, then those with depth 2,
265 then those with depth 3, and so on.
267 This search algorithm finds the least number of operations
268 needed to trigger a given bug.
270 - MC_DEEP: Depth-first search. Searches downward in the tree
271 of states as fast as possible. Good for finding bugs that
272 require long sequences of operations to trigger.
274 - MC_RANDOM: Random-first search. Searches through the tree
275 of states in random order. The standard C library's rand
276 function selects the search path; you can control the seed
277 passed to srand using mc_options_set_seed.
279 - MC_PATH: Explicit path. Applies an explicitly specified
280 sequence of operations. */
282 mc_options_get_strategy (const struct mc_options *options)
284 return options->strategy;
287 /* Sets the search strategy used for OPTIONS to STRATEGY.
289 This function cannot be used to set MC_PATH as the search
290 strategy. Use mc_options_set_follow_path instead. */
292 mc_options_set_strategy (struct mc_options *options, enum mc_strategy strategy)
294 assert (strategy == MC_BROAD
295 || strategy == MC_DEEP
296 || strategy == MC_RANDOM);
297 options->strategy = strategy;
300 /* Returns OPTION's random seed used by MC_RANDOM and
303 mc_options_get_seed (const struct mc_options *options)
305 return options->seed;
308 /* Set OPTION's random seed used by MC_RANDOM and MC_DROP_RANDOM
311 mc_options_set_seed (struct mc_options *options, unsigned int seed)
313 options->seed = seed;
316 /* Returns the maximum depth to which OPTIONS's search will
317 descend. The initial states are at depth 1, states produced
318 as their mutations are at depth 2, and so on. */
320 mc_options_get_max_depth (const struct mc_options *options)
322 return options->max_depth;
325 /* Sets the maximum depth to which OPTIONS's search will descend
326 to MAX_DEPTH. The initial states are at depth 1, states
327 produced as their mutations are at depth 2, and so on. */
329 mc_options_set_max_depth (struct mc_options *options, int max_depth)
331 options->max_depth = max_depth;
334 /* Returns the base-2 log of the number of bits in OPTIONS's hash
335 table. The hash table is used for dropping states that are
336 probably duplicates: any state with a given hash value, as
337 will only be processed once. A return value of 0 indicates
338 that the model checker will not discard duplicate states based
341 The hash table is a power of 2 bits long, by default 2**20
342 bits (128 kB). Depending on how many states you expect the
343 model checker to check, how much memory you're willing to let
344 the hash table take up, and how worried you are about missing
345 states due to hash collisions, you could make it larger or
348 The "birthday paradox" points to a reasonable way to size your
349 hash table. If you expect the model checker to check about
350 2**N states, then, assuming a perfect hash, you need a hash
351 table of 2**(N+1) bits to have a 50% chance of seeing a hash
352 collision, 2**(N+2) bits to have a 25% chance, and so on. */
354 mc_options_get_hash_bits (const struct mc_options *options)
356 return options->hash_bits;
359 /* Sets the base-2 log of the number of bits in OPTIONS's hash
360 table to HASH_BITS. A HASH_BITS value of 0 requests that the
361 model checker not discard duplicate states based on their
362 hashes. (This causes the model checker to never terminate in
365 mc_options_set_hash_bits (struct mc_options *options, int hash_bits)
367 assert (hash_bits >= 0);
368 options->hash_bits = MIN (hash_bits, CHAR_BIT * sizeof (unsigned int) - 1);
371 /* Returns the path set in OPTIONS by mc_options_set_follow_path.
372 May be used only if the search strategy is MC_PATH. */
373 const struct mc_path *
374 mc_options_get_follow_path (const struct mc_options *options)
376 assert (options->strategy == MC_PATH);
377 return &options->follow_path;
380 /* Sets, in OPTIONS, the search algorithm to MC_PATH and the path
381 to be the explicit path specified in FOLLOW_PATH. */
383 mc_options_set_follow_path (struct mc_options *options,
384 const struct mc_path *follow_path)
386 assert (mc_path_get_length (follow_path) > 0);
387 options->strategy = MC_PATH;
388 mc_path_copy (&options->follow_path, follow_path);
391 /* Returns the maximum number of queued states in OPTIONS. The
392 default value is 10,000. The primary reason to limit the
393 number of queued states is to conserve memory, so if you can
394 afford the memory and your model needs more room in the queue,
395 you can raise the limit. Conversely, if your models are large
396 or memory is constrained, you can reduce the limit.
398 Following the execution of the model checker, you can find out
399 the maximum queue length during the run by calling
400 mc_results_get_max_queue_length. */
402 mc_options_get_queue_limit (const struct mc_options *options)
404 return options->queue_limit;
407 /* Sets the maximum number of queued states in OPTIONS to
410 mc_options_set_queue_limit (struct mc_options *options, int queue_limit)
412 assert (queue_limit > 0);
413 options->queue_limit = queue_limit;
416 /* Returns the queue limit strategy used by OPTIONS, that is,
417 when a new state must be inserted into a full state queue is
418 full, how the state to be dropped is chosen. The choices are:
420 - MC_DROP_NEWEST: Drop the newest state; that is, do not
421 insert the new state into the queue at all.
423 - MC_DROP_OLDEST: Drop the state that has been enqueued for
426 - MC_DROP_RANDOM (the default): Drop a randomly selected state
427 from the queue. The standard C library's rand function
428 selects the state to drop; you can control the seed passed
429 to srand using mc_options_set_seed. */
430 enum mc_queue_limit_strategy
431 mc_options_get_queue_limit_strategy (const struct mc_options *options)
433 return options->queue_limit_strategy;
436 /* Sets the queue limit strategy used by OPTIONS to STRATEGY.
438 This setting has no effect unless the model being checked
439 causes the state queue to overflow (see
440 mc_options_get_queue_limit). */
442 mc_options_set_queue_limit_strategy (struct mc_options *options,
443 enum mc_queue_limit_strategy strategy)
445 assert (strategy == MC_DROP_NEWEST
446 || strategy == MC_DROP_OLDEST
447 || strategy == MC_DROP_RANDOM);
448 options->queue_limit_strategy = strategy;
451 /* Returns OPTIONS's maximum number of unique states that the
452 model checker will examine before terminating. The default is
455 mc_options_get_max_unique_states (const struct mc_options *options)
457 return options->max_unique_states;
460 /* Sets OPTIONS's maximum number of unique states that the model
461 checker will examine before terminating to
464 mc_options_set_max_unique_states (struct mc_options *options,
465 int max_unique_states)
467 options->max_unique_states = max_unique_states;
470 /* Returns the maximum number of errors that OPTIONS will allow
471 the model checker to encounter before terminating. The
474 mc_options_get_max_errors (const struct mc_options *options)
476 return options->max_errors;
479 /* Sets the maximum number of errors that OPTIONS will allow the
480 model checker to encounter before terminating to
483 mc_options_set_max_errors (struct mc_options *options, int max_errors)
485 options->max_errors = max_errors;
488 /* Returns the maximum amount of time, in seconds, that OPTIONS will allow the
489 model checker to consume before terminating. The
490 default of 0.0 means that time consumption is unlimited. */
492 mc_options_get_time_limit (const struct mc_options *options)
494 return options->time_limit;
497 /* Sets the maximum amount of time, in seconds, that OPTIONS will
498 allow the model checker to consume before terminating to
499 TIME_LIMIT. A value of 0.0 means that time consumption is
500 unlimited; otherwise, the return value will be positive. */
502 mc_options_set_time_limit (struct mc_options *options, double time_limit)
504 assert (time_limit >= 0.0);
505 options->time_limit = time_limit;
508 /* Returns the level of verbosity for output messages specified
509 by OPTIONS. The default verbosity level is 1.
511 A verbosity level of 0 inhibits all messages except for
512 errors; a verbosity level of 1 also allows warnings; a
513 verbosity level of 2 also causes a description of each state
514 added to be output; a verbosity level of 3 also causes a
515 description of each duplicate state to be output. Verbosity
516 levels less than 0 or greater than 3 are allowed but currently
517 have no additional effect. */
519 mc_options_get_verbosity (const struct mc_options *options)
521 return options->verbosity;
524 /* Sets the level of verbosity for output messages specified
525 by OPTIONS to VERBOSITY. */
527 mc_options_set_verbosity (struct mc_options *options, int verbosity)
529 options->verbosity = verbosity;
532 /* Returns the level of verbosity for failures specified by
533 OPTIONS. The default failure verbosity level is 2.
535 The failure verbosity level has an effect only when an error
536 is reported, and only when the failure verbosity level is
537 higher than the regular verbosity level. When this is the
538 case, the model checker replays the error path at the higher
539 verbosity level specified. This has the effect of outputting
540 an explicit, human-readable description of the sequence of
541 operations that caused the error. */
543 mc_options_get_failure_verbosity (const struct mc_options *options)
545 return options->failure_verbosity;
548 /* Sets the level of verbosity for failures specified by OPTIONS
549 to FAILURE_VERBOSITY. */
551 mc_options_set_failure_verbosity (struct mc_options *options,
552 int failure_verbosity)
554 options->failure_verbosity = failure_verbosity;
557 /* Returns the output file used for messages printed by the model
558 checker specified by OPTIONS. The default is stdout. */
560 mc_options_get_output_file (const struct mc_options *options)
562 return options->output_file;
565 /* Sets the output file used for messages printed by the model
566 checker specified by OPTIONS to OUTPUT_FILE.
568 The model checker does not automatically close the specified
569 output file. If this is desired, the model checker's client
572 mc_options_set_output_file (struct mc_options *options,
575 options->output_file = output_file;
578 /* Returns the number of microseconds between calls to the
579 progress function specified by OPTIONS. The default is
580 250,000 (1/4 second). A value of 0 disables progress
583 mc_options_get_progress_usec (const struct mc_options *options)
585 return options->progress_usec;
588 /* Sets the number of microseconds between calls to the progress
589 function specified by OPTIONS to PROGRESS_USEC. A value of 0
590 disables progress reporting. */
592 mc_options_set_progress_usec (struct mc_options *options, int progress_usec)
594 assert (progress_usec >= 0);
595 options->progress_usec = progress_usec;
598 /* Returns the function called to report progress specified by
599 OPTIONS. The function used by default prints '.' to
602 mc_options_get_progress_func (const struct mc_options *options)
604 return options->progress_func;
607 /* Sets the function called to report progress specified by
608 OPTIONS to PROGRESS_FUNC. A non-null function must be
609 specified; to disable progress reporting, set the progress
610 reporting interval to 0.
612 PROGRESS_FUNC will be called zero or more times while the
613 model checker's run is ongoing. For these calls to the
614 progress function, mc_results_get_stop_reason will return
615 MC_CONTINUING. It will also be called exactly once soon
616 before mc_run returns, in which case
617 mc_results_get_stop_reason will return a different value. */
619 mc_options_set_progress_func (struct mc_options *options,
620 mc_progress_func *progress_func)
622 assert (options->progress_func != NULL);
623 options->progress_func = progress_func;
626 /* Returns the auxiliary data set in OPTIONS by the client. The
627 default is a null pointer.
629 This auxiliary data value can be retrieved by the
630 client-specified functions in struct mc_class during a model
631 checking run using mc_get_aux. */
633 mc_options_get_aux (const struct mc_options *options)
638 /* Sets the auxiliary data in OPTIONS to AUX. */
640 mc_options_set_aux (struct mc_options *options, void *aux)
645 /* Results of a model checking run. */
648 /* Overall results. */
649 enum mc_stop_reason stop_reason; /* Why the run ended. */
650 int unique_state_count; /* Number of unique states checked. */
651 int error_count; /* Number of errors found. */
653 /* Depth statistics. */
654 int max_depth_reached; /* Max depth state examined. */
655 unsigned long int depth_sum; /* Sum of depths. */
656 int n_depths; /* Number of depths in depth_sum. */
658 /* If error_count > 0, path to the last error reported. */
659 struct mc_path error_path;
661 /* States dropped... */
662 int duplicate_dropped_states; /* ...as duplicates. */
663 int off_path_dropped_states; /* ...as off-path (MC_PATH only). */
664 int depth_dropped_states; /* ...due to excessive depth. */
665 int queue_dropped_states; /* ...due to queue overflow. */
667 /* Queue statistics. */
668 int queued_unprocessed_states; /* Enqueued but never dequeued. */
669 int max_queue_length; /* Maximum queue length observed. */
672 struct timeval start; /* Start of model checking run. */
673 struct timeval end; /* End of model checking run. */
676 /* Creates, initializes, and returns a new set of results. */
677 static struct mc_results *
678 mc_results_create (void)
680 struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
681 results->stop_reason = MC_CONTINUING;
682 gettimeofday (&results->start, NULL);
686 /* Destroys RESULTS. */
688 mc_results_destroy (struct mc_results *results)
692 mc_path_destroy (&results->error_path);
697 /* Returns RESULTS's reason that the model checking run
698 terminated. The possible reasons are:
700 - MC_CONTINUING: The run is not actually yet complete. This
701 can only be returned before mc_run has returned, e.g. when
702 the progress function set by mc_options_set_progress_func
703 examines the run's results.
705 - MC_SUCCESS: The run completed because the queue emptied.
706 The entire state space might not have been explored due to a
707 requested limit on maximum depth, hash collisions, etc.
709 - MC_MAX_UNIQUE_STATES: The run completed because as many
710 unique states have been checked as were requested (using
711 mc_options_set_max_unique_states).
713 - MC_MAX_ERROR_COUNT: The run completed because the maximum
714 requested number of errors (by default, 1 error) was
717 - MC_END_OF_PATH: The run completed because the path specified
718 with mc_options_set_follow_path was fully traversed.
720 - MC_TIMEOUT: The run completed because the time limit set
721 with mc_options_set_time_limit was exceeded.
723 - MC_INTERRUPTED: The run completed because SIGINT was caught
724 (typically, due to the user typing Ctrl+C). */
726 mc_results_get_stop_reason (const struct mc_results *results)
728 return results->stop_reason;
731 /* Returns the number of unique states checked specified by
734 mc_results_get_unique_state_count (const struct mc_results *results)
736 return results->unique_state_count;
739 /* Returns the number of errors found specified by RESULTS. */
741 mc_results_get_error_count (const struct mc_results *results)
743 return results->error_count;
746 /* Returns the maximum depth reached during the model checker run
747 represented by RESULTS. The initial states are at depth 1,
748 their child states at depth 2, and so on. */
750 mc_results_get_max_depth_reached (const struct mc_results *results)
752 return results->max_depth_reached;
755 /* Returns the mean depth reached during the model checker run
756 represented by RESULTS. */
758 mc_results_get_mean_depth_reached (const struct mc_results *results)
760 return (results->n_depths == 0
762 : (double) results->depth_sum / results->n_depths);
765 /* Returns the path traversed to obtain the last error
766 encountered during the model checker run represented by
767 RESULTS. Returns a null pointer if the run did not report any
769 const struct mc_path *
770 mc_results_get_error_path (const struct mc_results *results)
772 return results->error_count > 0 ? &results->error_path : NULL;
775 /* Returns the number of states dropped as duplicates (based on
776 hash value) during the model checker run represented by
779 mc_results_get_duplicate_dropped_states (const struct mc_results *results)
781 return results->duplicate_dropped_states;
784 /* Returns the number of states dropped because they were off the
785 path specified by mc_options_set_follow_path during the model
786 checker run represented by RESULTS. A nonzero value here
787 indicates a missing call to mc_include_state in the
788 client-supplied mutation function. */
790 mc_results_get_off_path_dropped_states (const struct mc_results *results)
792 return results->off_path_dropped_states;
795 /* Returns the number of states dropped because their depth
796 exceeded the maximum specified with mc_options_set_max_depth
797 during the model checker run represented by RESULTS. */
799 mc_results_get_depth_dropped_states (const struct mc_results *results)
801 return results->depth_dropped_states;
804 /* Returns the number of states dropped from the queue due to
805 queue overflow during the model checker run represented by
808 mc_results_get_queue_dropped_states (const struct mc_results *results)
810 return results->queue_dropped_states;
813 /* Returns the number of states that were checked and enqueued
814 but never dequeued and processed during the model checker run
815 represented by RESULTS. This is zero if the stop reason is
816 MC_CONTINUING or MC_SUCCESS; otherwise, it is the number of
817 states in the queue at the time that the checking run
820 mc_results_get_queued_unprocessed_states (const struct mc_results *results)
822 return results->queued_unprocessed_states;
825 /* Returns the maximum length of the queue during the model
826 checker run represented by RESULTS. If this is equal to the
827 maximum queue length, then the queue (probably) overflowed
828 during the run; otherwise, it did not overflow. */
830 mc_results_get_max_queue_length (const struct mc_results *results)
832 return results->max_queue_length;
835 /* Returns the time at which the model checker run represented by
838 mc_results_get_start (const struct mc_results *results)
840 return results->start;
843 /* Returns the time at which the model checker run represented by
844 RESULTS ended. (This function may not be called while the run
845 is still ongoing.) */
847 mc_results_get_end (const struct mc_results *results)
849 assert (results->stop_reason != MC_CONTINUING);
853 /* Returns the number of seconds obtained by subtracting time Y
856 timeval_subtract (struct timeval x, struct timeval y)
858 /* From libc.info. */
861 /* Perform the carry for the later subtraction by updating Y. */
862 if (x.tv_usec < y.tv_usec) {
863 int nsec = (y.tv_usec - x.tv_usec) / 1000000 + 1;
864 y.tv_usec -= 1000000 * nsec;
867 if (x.tv_usec - y.tv_usec > 1000000) {
868 int nsec = (x.tv_usec - y.tv_usec) / 1000000;
869 y.tv_usec += 1000000 * nsec;
873 /* Compute the time remaining to wait.
874 `tv_usec' is certainly positive. */
875 difference = (x.tv_sec - y.tv_sec) + (x.tv_usec - y.tv_usec) / 1000000.0;
876 if (x.tv_sec < y.tv_sec)
877 difference = -difference;
882 /* Returns the duration, in seconds, of the model checker run
883 represented by RESULTS. (This function may not be called
884 while the run is still ongoing.) */
886 mc_results_get_duration (const struct mc_results *results)
888 assert (results->stop_reason != MC_CONTINUING);
889 return timeval_subtract (results->end, results->start);
892 /* Prints a description of RESULTS to stream F. */
894 mc_results_print (const struct mc_results *results, FILE *f)
896 enum mc_stop_reason reason = mc_results_get_stop_reason (results);
898 if (reason != MC_CONTINUING)
899 fprintf (f, "Stopped by: %s\n",
900 reason == MC_SUCCESS ? "state space exhaustion"
901 : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
902 : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
903 : reason == MC_END_OF_PATH ? "reached end of specified path"
904 : reason == MC_TIMEOUT ? "reaching time limit"
905 : reason == MC_INTERRUPTED ? "user interruption"
907 fprintf (f, "Errors found: %d\n\n", mc_results_get_error_count (results));
909 fprintf (f, "Unique states checked: %d\n",
910 mc_results_get_unique_state_count (results));
911 fprintf (f, "Maximum depth reached: %d\n",
912 mc_results_get_max_depth_reached (results));
913 fprintf (f, "Mean depth reached: %.2f\n\n",
914 mc_results_get_mean_depth_reached (results));
916 fprintf (f, "Dropped duplicate states: %d\n",
917 mc_results_get_duplicate_dropped_states (results));
918 fprintf (f, "Dropped off-path states: %d\n",
919 mc_results_get_off_path_dropped_states (results));
920 fprintf (f, "Dropped too-deep states: %d\n",
921 mc_results_get_depth_dropped_states (results));
922 fprintf (f, "Dropped queue-overflow states: %d\n",
923 mc_results_get_queue_dropped_states (results));
924 fprintf (f, "Checked states still queued when stopped: %d\n",
925 mc_results_get_queued_unprocessed_states (results));
926 fprintf (f, "Maximum queue length reached: %d\n",
927 mc_results_get_max_queue_length (results));
929 if (reason != MC_CONTINUING)
930 fprintf (f, "\nRuntime: %.2f seconds\n",
931 mc_results_get_duration (results));
934 /* An active model checking run. */
937 /* Related data structures. */
938 const struct mc_class *class;
939 struct mc_options *options;
940 struct mc_results *results;
942 /* Array of 2**(options->hash_bits) bits representing states
947 struct mc_state **queue; /* Array of pointers to states. */
948 struct deque queue_deque; /* Deque. */
950 /* State currently being built by "init" or "mutate". */
951 struct mc_path path; /* Path to current state. */
952 struct string path_string; /* Buffer for path_string function. */
953 bool state_named; /* mc_name_operation called? */
954 bool state_error; /* mc_error called? */
956 /* Statistics for calling the progress function. */
957 unsigned int progress; /* Current progress value. */
958 unsigned int next_progress; /* Next value to call progress func. */
959 unsigned int prev_progress; /* Last value progress func called. */
960 struct timeval prev_progress_time; /* Last time progress func called. */
962 /* Information for handling and restoring SIGINT. */
963 bool interrupted; /* SIGINT received? */
964 bool *saved_interrupted_ptr; /* Saved value of interrupted_ptr. */
965 void (*saved_sigint) (int); /* Saved SIGINT handler. */
968 /* A state in the queue. */
971 struct mc_path path; /* Path to this state. */
972 void *data; /* Client-supplied data. */
975 /* Points to the current struct mc's "interrupted" member. */
976 static bool *interrupted_ptr = NULL;
978 static const char *path_string (struct mc *);
979 static void free_state (const struct mc *, struct mc_state *);
980 static void stop (struct mc *, enum mc_stop_reason);
981 static struct mc_state *make_state (const struct mc *, void *);
982 static size_t random_queue_index (struct mc *);
983 static void enqueue_state (struct mc *, struct mc_state *);
984 static void do_error_state (struct mc *);
985 static void next_operation (struct mc *);
986 static bool is_off_path (const struct mc *);
987 static void sigint_handler (int signum);
988 static void init_mc (struct mc *,
989 const struct mc_class *, struct mc_options *);
990 static void finish_mc (struct mc *);
992 /* Runs the model checker on the client-specified CLASS with the
993 client-specified OPTIONS. OPTIONS may be a null pointer if
994 the defaults are acceptable. Destroys OPTIONS; use
995 mc_options_clone if a copy is needed.
997 Returns the results of the model checking run, which must be
998 destroyed by the client with mc_results_destroy.
1000 To pass auxiliary data to the functions in CLASS, use
1001 mc_options_set_aux on OPTIONS, which may be retrieved from the
1002 CLASS functions using mc_get_aux. */
1004 mc_run (const struct mc_class *class, struct mc_options *options)
1008 init_mc (&mc, class, options);
1009 while (!deque_is_empty (&mc.queue_deque)
1010 && mc.results->stop_reason == MC_CONTINUING)
1012 struct mc_state *state = mc.queue[deque_pop_front (&mc.queue_deque)];
1013 mc_path_copy (&mc.path, &state->path);
1014 mc_path_push (&mc.path, 0);
1015 class->mutate (&mc, state->data);
1016 free_state (&mc, state);
1018 stop (&mc, MC_INTERRUPTED);
1025 /* Tests whether the current operation is one that should be
1026 performed, checked, and enqueued. If so, returns true.
1027 Otherwise, returns false and, unless checking is stopped,
1028 advances to the next state. The caller should then advance
1029 to the next operation.
1031 This function should be called from the client-provided
1032 "mutate" function, according to the pattern explained in the
1033 big comment at the top of model-checker.h. */
1035 mc_include_state (struct mc *mc)
1037 if (mc->results->stop_reason != MC_CONTINUING)
1039 else if (is_off_path (mc))
1041 next_operation (mc);
1048 /* Tests whether HASH represents a state that has (probably)
1049 already been enqueued. If not, returns false and marks HASH
1050 so that it will be treated as a duplicate in the future. If
1051 so, returns true and advances to the next state. The
1052 caller should then advance to the next operation.
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. */
1058 mc_discard_dup_state (struct mc *mc, unsigned int hash)
1060 if (mc->options->hash_bits > 0)
1062 hash &= (1u << mc->options->hash_bits) - 1;
1063 if (TEST_BIT (mc->hash, hash))
1065 if (mc->options->verbosity > 2)
1066 fprintf (mc->options->output_file,
1067 " [%s] discard duplicate state\n", path_string (mc));
1068 mc->results->duplicate_dropped_states++;
1069 next_operation (mc);
1072 SET_BIT (mc->hash, hash);
1077 /* Names the current state NAME, which may contain
1078 printf-style format specifications. NAME should be a
1079 human-readable name for the current operation.
1081 This function should be called from the client-provided
1082 "mutate" function, according to the pattern explained in the
1083 big comment at the top of model-checker.h. */
1085 mc_name_operation (struct mc *mc, const char *name, ...)
1089 va_start (args, name);
1090 mc_vname_operation (mc, name, args);
1094 /* Names the current state NAME, which may contain
1095 printf-style format specifications, for which the
1096 corresponding arguments must be given in ARGS. NAME should be
1097 a human-readable name for the current operation.
1099 This function should be called from the client-provided
1100 "mutate" function, according to the pattern explained in the
1101 big comment at the top of model-checker.h. */
1103 mc_vname_operation (struct mc *mc, const char *name, va_list args)
1105 if (mc->state_named && mc->options->verbosity > 0)
1106 fprintf (mc->options->output_file, " [%s] warning: duplicate call "
1107 "to mc_name_operation (missing call to mc_add_state?)\n",
1109 mc->state_named = true;
1111 if (mc->options->verbosity > 1)
1113 fprintf (mc->options->output_file, " [%s] ", path_string (mc));
1114 vfprintf (mc->options->output_file, name, args);
1115 putc ('\n', mc->options->output_file);
1119 /* Reports the given error MESSAGE for the current operation.
1120 The resulting state should still be passed to mc_add_state
1121 when all relevant error messages have been issued. The state
1122 will not, however, be enqueued for later mutation of its own.
1124 By default, model checking stops after the first error
1127 This function should be called from the client-provided
1128 "mutate" function, according to the pattern explained in the
1129 big comment at the top of model-checker.h. */
1131 mc_error (struct mc *mc, const char *message, ...)
1135 if (mc->results->stop_reason != MC_CONTINUING)
1138 if (mc->options->verbosity > 1)
1139 fputs (" ", mc->options->output_file);
1140 fprintf (mc->options->output_file, "[%s] error: ",
1142 va_start (args, message);
1143 vfprintf (mc->options->output_file, message, args);
1145 putc ('\n', mc->options->output_file);
1147 mc->state_error = true;
1150 /* Enqueues DATA as the state corresponding to the current
1151 operation. The operation should have been named with a call
1152 to mc_name_operation, and it should have been checked by the
1153 caller (who should have reported any errors with mc_error).
1155 This function should be called from the client-provided
1156 "mutate" function, according to the pattern explained in the
1157 big comment at the top of model-checker.h. */
1159 mc_add_state (struct mc *mc, void *data)
1161 if (!mc->state_named && mc->options->verbosity > 0)
1162 fprintf (mc->options->output_file, " [%s] warning: unnamed state\n",
1165 if (mc->results->stop_reason != MC_CONTINUING)
1167 /* Nothing to do. */
1169 else if (mc->state_error)
1170 do_error_state (mc);
1171 else if (is_off_path (mc))
1172 mc->results->off_path_dropped_states++;
1173 else if (mc->path.length + 1 > mc->options->max_depth)
1174 mc->results->depth_dropped_states++;
1177 /* This is the common case. */
1178 mc->results->unique_state_count++;
1179 if (mc->results->unique_state_count >= mc->options->max_unique_states)
1180 stop (mc, MC_MAX_UNIQUE_STATES);
1181 enqueue_state (mc, make_state (mc, data));
1182 next_operation (mc);
1186 mc->class->destroy (mc, data);
1187 next_operation (mc);
1190 /* Returns the options that were passed to mc_run for model
1192 const struct mc_options *
1193 mc_get_options (const struct mc *mc)
1198 /* Returns the current state of the results for model checker
1199 MC. This function is appropriate for use from the progress
1200 function set by mc_options_set_progress_func.
1202 Not all of the results are meaningful before model checking
1204 const struct mc_results *
1205 mc_get_results (const struct mc *mc)
1210 /* Returns the auxiliary data set on the options passed to mc_run
1211 with mc_options_set_aux. */
1213 mc_get_aux (const struct mc *mc)
1215 return mc_options_get_aux (mc_get_options (mc));
1218 /* Expresses MC->path as a string and returns the string. */
1220 path_string (struct mc *mc)
1222 ds_clear (&mc->path_string);
1223 mc_path_to_string (&mc->path, &mc->path_string);
1224 return ds_cstr (&mc->path_string);
1227 /* Frees STATE, including client data. */
1229 free_state (const struct mc *mc, struct mc_state *state)
1231 mc->class->destroy (mc, state->data);
1232 mc_path_destroy (&state->path);
1236 /* Sets STOP_REASON as the reason that MC's processing stopped,
1237 unless MC is already stopped. */
1239 stop (struct mc *mc, enum mc_stop_reason stop_reason)
1241 if (mc->results->stop_reason == MC_CONTINUING)
1242 mc->results->stop_reason = stop_reason;
1245 /* Creates and returns a new state whose path is copied from
1246 MC->path and whose data is specified by DATA. */
1247 static struct mc_state *
1248 make_state (const struct mc *mc, void *data)
1250 struct mc_state *new = xmalloc (sizeof *new);
1251 mc_path_init (&new->path);
1252 mc_path_copy (&new->path, &mc->path);
1257 /* Returns the index in MC->queue of a random element in the
1260 random_queue_index (struct mc *mc)
1262 assert (!deque_is_empty (&mc->queue_deque));
1263 return deque_front (&mc->queue_deque,
1264 rand () % deque_count (&mc->queue_deque));
1267 /* Adds NEW to MC's state queue, dropping a state if necessary
1270 enqueue_state (struct mc *mc, struct mc_state *new)
1274 if (new->path.length > mc->results->max_depth_reached)
1275 mc->results->max_depth_reached = new->path.length;
1276 mc->results->depth_sum += new->path.length;
1277 mc->results->n_depths++;
1279 if (deque_count (&mc->queue_deque) < mc->options->queue_limit)
1281 /* Add new state to queue. */
1282 if (deque_is_full (&mc->queue_deque))
1283 mc->queue = deque_expand (&mc->queue_deque,
1284 mc->queue, sizeof *mc->queue);
1285 switch (mc->options->strategy)
1288 idx = deque_push_back (&mc->queue_deque);
1291 idx = deque_push_front (&mc->queue_deque);
1294 if (!deque_is_empty (&mc->queue_deque))
1296 idx = random_queue_index (mc);
1297 mc->queue[deque_push_front (&mc->queue_deque)]
1301 idx = deque_push_front (&mc->queue_deque);
1304 assert (deque_is_empty (&mc->queue_deque));
1305 assert (!is_off_path (mc));
1306 idx = deque_push_back (&mc->queue_deque);
1308 >= mc_path_get_length (&mc->options->follow_path))
1309 stop (mc, MC_END_OF_PATH);
1314 if (deque_count (&mc->queue_deque) > mc->results->max_queue_length)
1315 mc->results->max_queue_length = deque_count (&mc->queue_deque);
1319 /* Queue has reached limit, so replace an existing
1321 assert (mc->options->strategy != MC_PATH);
1322 assert (!deque_is_empty (&mc->queue_deque));
1323 mc->results->queue_dropped_states++;
1324 switch (mc->options->queue_limit_strategy)
1326 case MC_DROP_NEWEST:
1327 free_state (mc, new);
1329 case MC_DROP_OLDEST:
1330 switch (mc->options->strategy)
1333 idx = deque_front (&mc->queue_deque, 0);
1336 idx = deque_back (&mc->queue_deque, 0);
1344 case MC_DROP_RANDOM:
1345 idx = random_queue_index (mc);
1350 free_state (mc, mc->queue[idx]);
1352 mc->queue[idx] = new;
1355 /* Process an error state being added to MC. */
1357 do_error_state (struct mc *mc)
1359 mc->results->error_count++;
1360 if (mc->results->error_count >= mc->options->max_errors)
1361 stop (mc, MC_MAX_ERROR_COUNT);
1363 mc_path_copy (&mc->results->error_path, &mc->path);
1365 if (mc->options->failure_verbosity > mc->options->verbosity)
1367 struct mc_options *path_options;
1369 fprintf (mc->options->output_file, "[%s] retracing error path:\n",
1371 path_options = mc_options_clone (mc->options);
1372 mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
1373 mc_options_set_failure_verbosity (path_options, 0);
1374 mc_options_set_follow_path (path_options, &mc->path);
1376 mc_results_destroy (mc_run (mc->class, path_options));
1378 putc ('\n', mc->options->output_file);
1382 /* Advances MC to start processing the operation following the
1385 next_operation (struct mc *mc)
1387 mc_path_push (&mc->path, mc_path_pop (&mc->path) + 1);
1388 mc->state_error = false;
1389 mc->state_named = false;
1391 if (++mc->progress >= mc->next_progress)
1394 double elapsed, delta;
1396 if (mc->results->stop_reason == MC_CONTINUING
1397 && !mc->options->progress_func (mc))
1398 stop (mc, MC_INTERRUPTED);
1400 gettimeofday (&now, NULL);
1402 if (mc->options->time_limit > 0.0
1403 && (timeval_subtract (now, mc->results->start)
1404 > mc->options->time_limit))
1405 stop (mc, MC_TIMEOUT);
1407 elapsed = timeval_subtract (now, mc->prev_progress_time);
1410 /* Re-estimate the amount of progress to take
1411 progress_usec microseconds. */
1412 unsigned int progress = mc->progress - mc->prev_progress;
1413 double progress_sec = mc->options->progress_usec / 1000000.0;
1414 delta = progress / elapsed * progress_sec;
1418 /* No measurable time at all elapsed during that amount
1419 of progress. Try doubling the amount of progress
1421 delta = (mc->progress - mc->prev_progress) * 2;
1424 if (delta > 0.0 && delta + mc->progress + 1.0 < UINT_MAX)
1425 mc->next_progress = mc->progress + delta + 1.0;
1427 mc->next_progress = mc->progress + (mc->progress - mc->prev_progress);
1429 mc->prev_progress = mc->progress;
1430 mc->prev_progress_time = now;
1434 /* Returns true if we're tracing an explicit path but the current
1435 operation produces a state off that path, false otherwise. */
1437 is_off_path (const struct mc *mc)
1439 return (mc->options->strategy == MC_PATH
1440 && (mc_path_back (&mc->path)
1441 != mc_path_get_operation (&mc->options->follow_path,
1442 mc->path.length - 1)));
1445 /* Handler for SIGINT. */
1447 sigint_handler (int signum UNUSED)
1449 /* Just mark the model checker as interrupted. */
1450 *interrupted_ptr = true;
1453 /* Initializes MC as a model checker with the given CLASS and
1454 OPTIONS. OPTIONS may be null to use the default options. */
1456 init_mc (struct mc *mc, const struct mc_class *class,
1457 struct mc_options *options)
1459 /* Validate and adjust OPTIONS. */
1460 if (options == NULL)
1461 options = mc_options_create ();
1462 assert (options->queue_limit_strategy != MC_DROP_OLDEST
1463 || options->strategy != MC_RANDOM);
1464 if (options->strategy == MC_PATH)
1466 options->max_depth = INT_MAX;
1467 options->hash_bits = 0;
1469 if (options->progress_usec == 0)
1471 options->progress_func = null_progress;
1472 if (options->time_limit > 0.0)
1473 options->progress_usec = 250000;
1476 /* Initialize MC. */
1478 mc->options = options;
1479 mc->results = mc_results_create ();
1481 mc->hash = (mc->options->hash_bits > 0
1482 ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT))
1486 deque_init_null (&mc->queue_deque);
1488 mc_path_init (&mc->path);
1489 mc_path_push (&mc->path, 0);
1490 ds_init_empty (&mc->path_string);
1491 mc->state_named = false;
1492 mc->state_error = false;
1495 mc->next_progress = mc->options->progress_usec != 0 ? 100 : UINT_MAX;
1496 mc->prev_progress = 0;
1497 mc->prev_progress_time = mc->results->start;
1499 if (mc->options->strategy == MC_RANDOM
1500 || options->queue_limit_strategy == MC_DROP_RANDOM)
1501 srand (mc->options->seed);
1503 mc->interrupted = false;
1504 mc->saved_interrupted_ptr = interrupted_ptr;
1505 interrupted_ptr = &mc->interrupted;
1506 mc->saved_sigint = signal (SIGINT, sigint_handler);
1511 /* Complete the model checker run for MC. */
1513 finish_mc (struct mc *mc)
1515 /* Restore signal handlers. */
1516 signal (SIGINT, mc->saved_sigint);
1517 interrupted_ptr = mc->saved_interrupted_ptr;
1519 /* Mark the run complete. */
1520 stop (mc, MC_SUCCESS);
1521 gettimeofday (&mc->results->end, NULL);
1523 /* Empty the queue. */
1524 mc->results->queued_unprocessed_states = deque_count (&mc->queue_deque);
1525 while (!deque_is_empty (&mc->queue_deque))
1527 struct mc_state *state = mc->queue[deque_pop_front (&mc->queue_deque)];
1528 free_state (mc, state);
1531 /* Notify the progress function of completion. */
1532 mc->options->progress_func (mc);
1535 mc_path_destroy (&mc->path);
1536 ds_destroy (&mc->path_string);