/* PSPP - a program for statistical analysis.
- Copyright (C) 2007, 2009 Free Software Foundation, Inc.
+ Copyright (C) 2007, 2009, 2010, 2011, 2013 Free Software Foundation, Inc.
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
#include <config.h>
-#include <libpspp/model-checker.h>
+#include "libpspp/model-checker.h"
#include <limits.h>
#include <signal.h>
#include <string.h>
#include <sys/time.h>
-#include <libpspp/argv-parser.h>
-#include <libpspp/bit-vector.h>
-#include <libpspp/compiler.h>
-#include <libpspp/deque.h>
-#include <libpspp/misc.h>
-#include <libpspp/str.h>
+#include "libpspp/argv-parser.h"
+#include "libpspp/bit-vector.h"
+#include "libpspp/compiler.h"
+#include "libpspp/deque.h"
+#include "libpspp/misc.h"
+#include "libpspp/str.h"
-#include "error.h"
-#include "minmax.h"
-#include "xalloc.h"
+#include "gl/error.h"
+#include "gl/minmax.h"
+#include "gl/xalloc.h"
\f
/* Initializes PATH as an empty path. */
void
for (i = 0; i < mc_path_get_length (path); i++)
{
if (i > 0)
- ds_put_char (string, ' ');
+ ds_put_byte (string, ' ');
ds_put_format (string, "%d", mc_path_get_operation (path, i));
}
}
mc_options_set_strategy (options, MC_RANDOM);
else
error (1, 0,
- "strategy must be \"broad\", \"deep\", or \"random\"");
+ "strategy must be `broad', `deep', or `random'");
break;
case OPT_MAX_DEPTH:
else if (!strcmp (optarg, "random"))
mc_options_set_queue_limit_strategy (options, MC_DROP_RANDOM);
else
- error (1, 0, "--queue-drop argument must be \"newest\", "
- "\"oldest\", or \"random\"");
+ error (1, 0, "--queue-drop argument must be `newest' "
+ "`oldest' or `random'");
break;
case OPT_SEED:
static struct mc_results *
mc_results_create (void)
{
- struct mc_results *results = xcalloc (1, sizeof (struct mc_results));
+ struct mc_results *results = XCALLOC (1, struct mc_results);
results->stop_reason = MC_CONTINUING;
gettimeofday (&results->start, NULL);
return results;
/* Array of 2**(options->hash_bits) bits representing states
already visited. */
- unsigned char *hash;
+ unsigned long int *hash;
/* State queue. */
struct mc_state **queue; /* Array of pointers to states. */
if (!mc->state_error && mc->options->hash_bits > 0)
{
hash &= (1u << mc->options->hash_bits) - 1;
- if (TEST_BIT (mc->hash, hash))
+ if (bitvector_is_set (mc->hash, hash))
{
if (mc->options->verbosity > 2)
fprintf (mc->options->output_file,
next_operation (mc);
return true;
}
- SET_BIT (mc->hash, hash);
+ bitvector_set1 (mc->hash, hash);
}
return false;
}
mc->results = mc_results_create ();
mc->hash = (mc->options->hash_bits > 0
- ? xcalloc (1, DIV_RND_UP (1 << mc->options->hash_bits, CHAR_BIT))
+ ? bitvector_allocate (1 << mc->options->hash_bits)
: NULL);
mc->queue = NULL;
/* Free memory. */
mc_path_destroy (&mc->path);
ds_destroy (&mc->path_string);
- free (mc->options);
+ mc_options_destroy (mc->options);
free (mc->queue);
free (mc->hash);
}