[Pspp-cvs] pspp/src data/datasheet.c language/tests/check-... [simpler-proc]

[Ben Pfaff]

CVSROOT:        /cvsroot/pspp
Module name:    pspp
Branch:         simpler-proc
Changes by:     Ben Pfaff <blp> 07/04/15 05:15:17

Modified files:
        src/data       : datasheet.c 
        src/language/tests: check-model.q 
        src/libpspp    : model-checker.c model-checker.h 

Log message:
        Start cleaning up model checker.

CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/pspp/src/data/datasheet.c?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.5&r2=1.1.2.6
http://cvs.savannah.gnu.org/viewcvs/pspp/src/language/tests/check-model.q?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.2&r2=1.1.2.3
http://cvs.savannah.gnu.org/viewcvs/pspp/src/libpspp/model-checker.c?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.2&r2=1.1.2.3
http://cvs.savannah.gnu.org/viewcvs/pspp/src/libpspp/model-checker.h?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.1&r2=1.1.2.2

Patches:
Index: data/datasheet.c
===================================================================
RCS file: /cvsroot/pspp/pspp/src/data/Attic/datasheet.c,v
retrieving revision 1.1.2.5
retrieving revision 1.1.2.6
diff -u -b -r1.1.2.5 -r1.1.2.6
--- data/datasheet.c    14 Apr 2007 23:01:54 -0000      1.1.2.5
+++ data/datasheet.c    15 Apr 2007 05:15:17 -0000      1.1.2.6
@@ -1070,8 +1070,6 @@
 {
   struct datasheet *ds;
   struct range_map_node *r;
-  size_t row_cnt, column_cnt;
-  size_t row, column;
 
   /* Clone ODS into DS. */
   ds = *ds_ = xmalloc (sizeof *ds);
@@ -1090,11 +1088,7 @@
   ds->column_min_alloc = ods->column_min_alloc;
 
   /* Clone ODATA into DATA. */
-  row_cnt = datasheet_get_row_cnt (ds);
-  column_cnt = datasheet_get_column_cnt (ds);
-  for (row = 0; row < row_cnt; row++)
-    for (column = 0; column < column_cnt; column++)
-      data[row][column] = odata[row][column];
+  memcpy (data, odata, MAX_ROWS * MAX_COLS * sizeof **data);
 }
 
 static void
@@ -1312,7 +1306,7 @@
       datasheet_mc_destroy,
     };
 
-  params->next_value = 0;
+  params->next_value = 1;
   params->max_rows = MIN (params->max_rows, MAX_ROWS);
   params->max_cols = MIN (params->max_cols, MAX_COLS);
   params->backing_rows = MIN (params->backing_rows, params->max_rows);

Index: language/tests/check-model.q
===================================================================
RCS file: /cvsroot/pspp/pspp/src/language/tests/Attic/check-model.q,v
retrieving revision 1.1.2.2
retrieving revision 1.1.2.3
diff -u -b -r1.1.2.2 -r1.1.2.3
--- language/tests/check-model.q        14 Apr 2007 23:02:45 -0000      1.1.2.2
+++ language/tests/check-model.q        15 Apr 2007 05:15:17 -0000      1.1.2.3
@@ -39,6 +39,7 @@
     search=strategy:broad/deep/random,
            :mxd(n:max_depth),
            :hash(n:hash_bits);
+    path=integer list;
     queue=:limit(n:queue_limit,"%s>0"),
           drop:newest/oldest/random;
     seed=integer;
@@ -122,6 +123,30 @@
                              : cmd.strategy == CHM_DEEP ? MC_DEEP
                              : cmd.strategy == CHM_RANDOM ? MC_RANDOM
                              : -1);
+  if (cmd.sbc_path > 0)
+    {
+      if (cmd.sbc_search > 0)
+        msg (SW, _("PATH and SEARCH subcommands are mutually exclusive.  "
+                   "Ignoring PATH."));
+      else 
+        {
+          struct subc_list_int *list = &cmd.il_path[0];
+          int count = subc_list_int_count (list);
+          if (count > 0)
+            {
+              struct mc_path path;
+              int i;
+          
+              mc_path_init (&path);
+              for (i = 0; i < count; i++)
+                mc_path_push (&path, subc_list_int_at (list, i));
+              mc_options_set_follow_path (options, &path);
+              mc_path_destroy (&path);
+            }
+          else
+            msg (SW, _("At least one value must be specified on PATH."));
+        }
+    }
   if (cmd.max_depth != NOT_LONG)
     mc_options_set_max_depth (options, cmd.max_depth);
   if (cmd.hash_bits != NOT_LONG) 
@@ -196,6 +221,7 @@
            reason == MC_SUCCESS ? "state space exhaustion"
            : reason == MC_MAX_UNIQUE_STATES ? "reaching max unique states"
            : reason == MC_MAX_ERROR_COUNT ? "reaching max error count"
+           : reason == MC_END_OF_PATH ? "reached end of specified path"
            : reason == MC_TIMEOUT ? "reaching time limit"
            : reason == MC_INTERRUPTED ? "user interruption"
            : "unknown reason");

Index: libpspp/model-checker.c
===================================================================
RCS file: /cvsroot/pspp/pspp/src/libpspp/Attic/model-checker.c,v
retrieving revision 1.1.2.2
retrieving revision 1.1.2.3
diff -u -b -r1.1.2.2 -r1.1.2.3
--- libpspp/model-checker.c     14 Apr 2007 23:03:44 -0000      1.1.2.2
+++ libpspp/model-checker.c     15 Apr 2007 05:15:17 -0000      1.1.2.3
@@ -38,6 +38,76 @@
 #include "minmax.h"
 #include "xalloc.h"
 
+void
+mc_path_init (struct mc_path *path) 
+{
+  path->states = NULL;
+  path->length = 0;
+  path->capacity = 0;
+}
+
+void
+mc_path_copy (struct mc_path *new, const struct mc_path *old) 
+{
+  if (old->length > new->capacity) 
+    {
+      new->capacity = old->length + 1;
+      free (new->states);
+      new->states = xnmalloc (new->capacity, sizeof *new->states);
+    }
+  new->length = old->length;
+  memcpy (new->states, old->states, old->length * sizeof *new->states);
+}
+
+void
+mc_path_push (struct mc_path *new, int new_state) 
+{
+  if (new->length >= new->capacity) 
+    new->states = xnrealloc (new->states,
+                             ++new->capacity, sizeof *new->states);
+  new->states[new->length++] = new_state;
+}
+
+void
+mc_path_pop (struct mc_path *path) 
+{
+  assert (path->length > 0);
+  path->length--;
+}
+
+void
+mc_path_destroy (struct mc_path *path) 
+{
+  free (path->states);
+  path->states = NULL;
+}
+
+int
+mc_path_get_state (const struct mc_path *path, size_t index) 
+{
+  assert (index < path->length);
+  return path->states[index];
+}
+
+size_t
+mc_path_get_length (const struct mc_path *path) 
+{
+  return path->length;
+}
+
+static void
+mc_path_to_string (const struct mc_path *path, struct string *string) 
+{
+  size_t i;
+
+  for (i = 0; i < mc_path_get_length (path); i++) 
+    {
+      if (i > 0)
+        ds_put_char (string, ' ');
+      ds_put_format (string, "%d", mc_path_get_state (path, i)); 
+    }
+}
+
 /* Search options. */
 struct mc_options 
   {
@@ -45,6 +115,7 @@
     int max_depth;
     int hash_bits;
     unsigned int seed;
+    struct mc_path follow_path;
 
     int queue_limit;
     enum mc_queue_limit_strategy queue_limit_strategy;
@@ -88,6 +159,7 @@
   options->max_depth = INT_MAX;
   options->hash_bits = 20;
   options->seed = 0;
+  mc_path_init (&options->follow_path);
   
   options->queue_limit = 10000;
   options->queue_limit_strategy = MC_DROP_RANDOM;
@@ -116,6 +188,7 @@
 void
 mc_options_destroy (struct mc_options *options) 
 {
+  mc_path_destroy (&options->follow_path);
   free (options);
 }
 
@@ -171,6 +244,22 @@
   options->hash_bits = MIN (hash_bits, 31);
 }
 
+const struct mc_path *
+mc_options_get_follow_path (const struct mc_options *options) 
+{
+  assert (options->strategy == MC_PATH);
+  return &options->follow_path;
+}
+
+void
+mc_options_set_follow_path (struct mc_options *options,
+                            const struct mc_path *follow_path) 
+{
+  assert (mc_path_get_length (follow_path) > 0);
+  options->strategy = MC_PATH;
+  mc_path_copy (&options->follow_path, follow_path);
+}
+
 int
 mc_options_get_queue_limit (const struct mc_options *options) 
 {
@@ -331,8 +420,7 @@
     int max_depth_reached;
     struct moments1 *depth_moments;
 
-    int *error_path;
-    size_t error_path_len;
+    struct mc_path error_path;
 
     int duplicate_dropped_states;
     int off_path_dropped_states;
@@ -360,7 +448,7 @@
   if (results != NULL) 
     {
       moments1_destroy (results->depth_moments);
-      free (results->error_path);
+      mc_path_destroy (&results->error_path);
       free (results);
     }
 }
@@ -397,22 +485,10 @@
   return mean != SYSMIS ? mean : 0.0;
 }
 
-bool
-mc_results_get_last_error_path (const struct mc_results *results,
-                                const int **path, size_t *path_len) 
+const struct mc_path *
+mc_results_get_error_path (const struct mc_results *results) 
 {
-  if (results->error_count > 0) 
-    {
-      *path = results->error_path;
-      *path_len = results->error_path_len;
-      return true;
-    }
-  else 
-    {
-      *path = NULL;
-      *path_len = 0;
-      return false;
-    }
+  return results->error_count > 0 ? &results->error_path : NULL;
 }
 
 int
@@ -503,19 +579,20 @@
     struct mc_options *options;
     struct mc_results *results;
 
-    unsigned char *seen_states;
+    unsigned char *hash;
 
     struct deque state_deque;
     struct mc_state **states;
+    size_t follow_path_idx;
 
     struct mc_state *state;
+    struct mc_path substate_path;
+    struct string substate_path_string;
     int substate;
 
     bool named_state;
     bool error_state;
 
-    int include_substate;
-
     unsigned int progress;
     unsigned int next_progress;
     unsigned int prev_progress;
@@ -528,17 +605,24 @@
 
 struct mc_state
   {
-    int depth;
-    int *sequence;
+    struct mc_path path;
     void *data;
   };
 
+static const char *
+substate_path_string (struct mc *mc) 
+{
+  ds_clear (&mc->substate_path_string);
+  mc_path_to_string (&mc->substate_path, &mc->substate_path_string);
+  return ds_cstr (&mc->substate_path_string);
+}
+
 static void
 free_state (const struct mc_class *class, struct mc_state *state) 
 {
   if (state->data != NULL)
     class->destroy (state->data);
-  free (state->sequence);
+  mc_path_destroy (&state->path);
   free (state);
 }
 
@@ -552,18 +636,10 @@
 static struct mc_state *
 make_child_state (const struct mc *mc, void *data) 
 {
-  const struct mc_state *parent = mc->state;
   struct mc_state *new = xmalloc (sizeof *new);
-  
-  new->depth = parent->depth + 1;
-
-  new->sequence = xnmalloc (new->depth, sizeof *new->sequence);
-  memcpy (new->sequence, parent->sequence,
-          (new->depth - 1) * sizeof *parent->sequence);
-  new->sequence[new->depth - 1] = mc->substate;
-
+  mc_path_init (&new->path);
+  mc_path_copy (&new->path, &mc->substate_path);
   new->data = data;
-
   return new;
 }
 
@@ -580,9 +656,9 @@
 {
   size_t idx;
 
-  if (new->depth > mc->results->max_depth_reached)
-    mc->results->max_depth_reached = new->depth;
-  moments1_add (mc->results->depth_moments, new->depth, 1.0);
+  if (new->path.length > mc->results->max_depth_reached)
+    mc->results->max_depth_reached = new->path.length;
+  moments1_add (mc->results->depth_moments, new->path.length, 1.0);
 
   if (deque_count (&mc->state_deque) < mc->options->queue_limit) 
     {
@@ -608,6 +684,15 @@
           else
             idx = deque_push_front (&mc->state_deque);
           break;
+        case MC_PATH:
+          assert (deque_is_empty (&mc->state_deque));
+          assert (mc->substate == mc_path_get_state (&mc->options->follow_path,
+                                                     mc->state->path.length));
+          idx = deque_push_back (&mc->state_deque);
+          if (mc->state->path.length + 1
+              >= mc_path_get_length (&mc->options->follow_path))
+            stop (mc, MC_END_OF_PATH);
+          break;
         default:
           NOT_REACHED ();
         }
@@ -618,6 +703,7 @@
     {
       /* Queue has reached limit, so replace an existing
          state. */
+      assert (mc->options->strategy != MC_PATH);
       assert (!deque_is_empty (&mc->state_deque));
       mc->results->queue_dropped_states++;
       switch (mc->options->queue_limit_strategy) 
@@ -634,7 +720,8 @@
             case MC_DEEP:
               idx = deque_back (&mc->state_deque, 0);
               break;
-            case MC_DROP_RANDOM:
+            case MC_RANDOM:
+            case MC_PATH:
             default:
               NOT_REACHED ();
             }
@@ -650,20 +737,6 @@
   mc->states[idx] = new;
 }
 
-static const char *
-state_path_string (const struct mc *mc) 
-{
-  static struct string s = DS_EMPTY_INITIALIZER;
-  size_t i;
-
-  ds_clear (&s);
-  for (i = 0; i < mc->state->depth; i++) 
-    ds_put_format (&s, "%d ", mc->state->sequence[i]);
-  ds_put_format (&s, "%d", mc->substate);
-
-  return ds_cstr (&s);
-}
-
 static void
 do_error_state (struct mc *mc)
 {
@@ -671,23 +744,21 @@
   if (mc->results->error_count >= mc->options->max_errors)
     stop (mc, MC_MAX_ERROR_COUNT);
 
+  mc_path_copy (&mc->results->error_path, &mc->substate_path);
+      
   if (mc->options->failure_verbosity > mc->options->verbosity)
     {
       struct mc_options *path_options;
-      struct mc_state *state;
 
       fprintf (mc->options->output_file, "[%s] retracing error path:\n",
-               state_path_string (mc));
+               substate_path_string (mc));
       path_options = mc_options_clone (mc->options);
       mc_options_set_verbosity (path_options, mc->options->failure_verbosity);
       mc_options_set_failure_verbosity (path_options, 0);
+      mc_options_set_follow_path (path_options, &mc->substate_path);
 
-      state = make_child_state (mc, NULL);
-      
-      mc_results_destroy (mc_follow_path (mc->class, path_options,
-                                          state->sequence, state->depth));
+      mc_results_destroy (mc_run (mc->class, path_options));
 
-      free_state (mc->class, state);
       putc ('\n', mc->options->output_file);
     }
 }
@@ -698,16 +769,13 @@
   if (mc->named_state) 
     fprintf (mc->options->output_file, "  [%s] warning: duplicate call "
              "to mc_name_state (missing call to mc_add_state?)\n",
-             state_path_string (mc));
+             substate_path_string (mc));
   mc->named_state = true;
 
   if (mc->options->verbosity > 1) 
     {
-
-      fprintf (mc->options->output_file, "  [%s] ", state_path_string (mc));
-
+      fprintf (mc->options->output_file, "  [%s] ", substate_path_string (mc));
       vfprintf (mc->options->output_file, name, args);
-
       putc ('\n', mc->options->output_file);
     }
 }
@@ -726,6 +794,9 @@
 next_substate (struct mc *mc) 
 {
   mc->substate++;
+  mc_path_pop (&mc->substate_path);
+  mc_path_push (&mc->substate_path, mc->substate);
+  mc->error_state = false;
   mc->named_state = false;
 
   if (++mc->progress >= mc->next_progress) 
@@ -777,23 +848,35 @@
   if (mc->options->hash_bits > 0)
     {
       hash &= (1u << mc->options->hash_bits) - 1;
-      if (TEST_BIT (mc->seen_states, hash)) 
+      if (TEST_BIT (mc->hash, hash)) 
         {
+          if (mc->options->verbosity > 2)
+            fprintf (mc->options->output_file,
+                     "    [%s] discard duplicate state\n",
+                     substate_path_string (mc));
           mc->results->duplicate_dropped_states++;
           next_substate (mc);
           return true;
         }
-      SET_BIT (mc->seen_states, hash);
+      SET_BIT (mc->hash, hash);
     }
   return false; 
 }
 
+static bool
+is_off_path (const struct mc *mc) 
+{
+  return (mc->options->strategy == MC_PATH
+          && mc->substate != mc_path_get_state (&mc->options->follow_path,
+                                                mc->state->path.length));
+}
+
 void
 mc_add_state (struct mc *mc, void *data) 
 {
   if (!mc->named_state)
     fprintf (mc->options->output_file, "  [%s] warning: unnamed state\n",
-             state_path_string (mc));
+             substate_path_string (mc));
 
   if (mc->results->stop_reason != MC_CONTINUING)
     {
@@ -801,10 +884,9 @@
     }
   else if (mc->error_state) 
     do_error_state (mc);
-  else if (mc->include_substate >= 0
-           && mc->substate != mc->include_substate) 
+  else if (is_off_path (mc))
     mc->results->off_path_dropped_states++;
-  else if (mc->state->depth + 1 > mc->options->max_depth)
+  else if (mc->state->path.length + 1 > mc->options->max_depth)
     mc->results->depth_dropped_states++;
   else 
     {
@@ -817,7 +899,6 @@
       return;
     }
 
-  mc->error_state = false;
   mc->class->destroy (data);
   next_substate (mc);
 }
@@ -834,13 +915,19 @@
 init_mc (struct mc *mc, const struct mc_class *class,
          struct mc_options *options) 
 {
-  struct mc_state null_state = {0, NULL, NULL};
+  struct mc_state null_state = { { NULL, 0 }, NULL };
 
   mc->class = class;
   
   mc->options = options != NULL ? options : mc_options_create ();
   check_options (mc->options);
 
+  if (mc->options->strategy == MC_PATH) 
+    {
+      mc->options->max_depth = INT_MAX;
+      mc->options->hash_bits = 0;
+    }
+
   if (mc->options->progress_usec == 0) 
     {
       mc->options->progress_func = null_progress;
@@ -852,17 +939,18 @@
   gettimeofday (&mc->results->start, NULL);
 
   if (mc->options->hash_bits > 0) 
-    mc->seen_states = xcalloc (1, (1u << mc->options->hash_bits) / CHAR_BIT);
+    mc->hash = xcalloc (1, (1u << mc->options->hash_bits) / CHAR_BIT);
   else
-    mc->seen_states = NULL;
+    mc->hash = NULL;
   mc->states = NULL;
   deque_init_null (&mc->state_deque);
 
   mc->substate = 0;
+  mc_path_init (&mc->substate_path);
+  mc_path_push (&mc->substate_path, mc->substate);
+  ds_init_empty (&mc->substate_path_string);
   mc->state = &null_state;
 
-  mc->include_substate = -1;
-
   mc->named_state = false;
   mc->error_state = false;
 
@@ -901,9 +989,11 @@
 
   mc->options->progress_func (mc);
 
+  mc_path_destroy (&mc->substate_path);
+  ds_destroy (&mc->substate_path_string);
   free (mc->options);
   free (mc->states);
-  free (mc->seen_states);
+  free (mc->hash);
 }
 
 static void
@@ -924,6 +1014,8 @@
     {
       mc.substate = 0;
       mc.state = mc.states[deque_pop_front (&mc.state_deque)];
+      mc_path_copy (&mc.substate_path, &mc.state->path);
+      mc_path_push (&mc.substate_path, mc.substate);
       class->mutate (&mc, mc.state->data);
       free_state (class, mc.state);
       periodic_mc (&mc);
@@ -933,39 +1025,6 @@
   return mc.results;
 }
 
-/* Should return "void *" reached by path? */
-struct mc_results *
-mc_follow_path (const struct mc_class *class, struct mc_options *options,
-                int *path, size_t path_len) 
-{
-  struct mc mc;
-  size_t i;
-
-  init_mc (&mc, class, options);
-  for (i = 1; i < path_len; i++) 
-    {
-      if (deque_is_empty (&mc.state_deque)) 
-        {
-          fprintf (options->output_file,
-                   "No state found after %zu elements in path (out of %zu)\n",
-                   i, path_len);
-          break;
-        }
-      assert (deque_count (&mc.state_deque) == 1);
-
-      mc.substate = 0;
-      mc.state = mc.states[deque_pop_front (&mc.state_deque)];
-      mc.include_substate = path[i];
-      class->mutate (&mc, mc.state->data);
-      free_state (class, mc.state);
-
-      periodic_mc (&mc);
-    }
-  finish_mc (&mc);
-
-  return mc.results;
-}
-
 void
 mc_error (struct mc *mc, const char *message, ...) 
 {
@@ -976,7 +1035,8 @@
 
   if (mc->options->verbosity > 1)
     fputs ("    ", mc->options->output_file);
-  fprintf (mc->options->output_file, "[%s] error: ", state_path_string (mc));
+  fprintf (mc->options->output_file, "[%s] error: ",
+           substate_path_string (mc));
   va_start (args, message);
   vfprintf (mc->options->output_file, message, args);
   va_end (args);
@@ -990,11 +1050,12 @@
 {
   if (mc->results->stop_reason != MC_CONTINUING)
     return false;
-  if (mc->include_substate >= 0 && mc->substate != mc->include_substate) 
+  else if (is_off_path (mc))
     {
-      mc->substate++;
+      next_substate (mc);
       return false; 
     }
+  else
   return true;
 }
 

Index: libpspp/model-checker.h
===================================================================
RCS file: /cvsroot/pspp/pspp/src/libpspp/Attic/model-checker.h,v
retrieving revision 1.1.2.1
retrieving revision 1.1.2.2
diff -u -b -r1.1.2.1 -r1.1.2.2
--- libpspp/model-checker.h     14 Apr 2007 05:04:23 -0000      1.1.2.1
+++ libpspp/model-checker.h     15 Apr 2007 05:15:17 -0000      1.1.2.2
@@ -36,6 +36,22 @@
     void (*destroy) (void *);
   };
 
+struct mc_path 
+  {
+    int *states;
+    size_t length;
+    size_t capacity;
+  };
+
+void mc_path_init (struct mc_path *);
+void mc_path_copy (struct mc_path *, const struct mc_path *);
+void mc_path_push (struct mc_path *, int new_state);
+void mc_path_pop (struct mc_path *);
+void mc_path_destroy (struct mc_path *);
+
+int mc_path_get_state (const struct mc_path *, size_t index);
+size_t mc_path_get_length (const struct mc_path *);
+
 struct mc_options *mc_options_create (void);
 struct mc_options *mc_options_clone (const struct mc_options *);
 void mc_options_destroy (struct mc_options *);
@@ -45,11 +61,13 @@
   {
     MC_BROAD,           /* Breadth-first search. */
     MC_DEEP,            /* Depth-first search. */
-    MC_RANDOM           /* Randomly ordered search. */
+    MC_RANDOM,          /* Randomly ordered search. */
+    MC_PATH             /* Follow one explicit path. */
   };
 
 enum mc_strategy mc_options_get_strategy (const struct mc_options *);
 void mc_options_set_strategy (struct mc_options *, enum mc_strategy);
+const struct mc_path *mc_options_get_follow_path (const struct mc_options *);
 unsigned int mc_options_get_seed (const struct mc_options *);
 void mc_options_set_seed (struct mc_options *, unsigned int seed);
 int mc_options_get_max_depth (const struct mc_options *);
@@ -57,6 +75,8 @@
 int mc_options_get_hash_bits (const struct mc_options *);
 void mc_options_set_hash_bits (struct mc_options *, int hash_bits);
 
+void mc_options_set_follow_path (struct mc_options *, const struct mc_path *);
+
 enum mc_queue_limit_strategy 
   {
     MC_DROP_NEWEST,
@@ -102,6 +122,7 @@
     MC_SUCCESS,
     MC_MAX_UNIQUE_STATES,
     MC_MAX_ERROR_COUNT,
+    MC_END_OF_PATH,
     MC_TIMEOUT,
     MC_INTERRUPTED
   };
@@ -117,8 +138,7 @@
 int mc_results_get_max_depth_reached (const struct mc_results *);
 double mc_results_get_mean_depth_reached (const struct mc_results *);
 
-bool mc_results_get_last_error_path (const struct mc_results *,
-                                     const int **path, size_t *path_len);
+const struct mc_path *mc_results_get_error_path (const struct mc_results *);
 
 int mc_results_get_duplicate_dropped_states (const struct mc_results *);
 int mc_results_get_off_path_dropped_states (const struct mc_results *);
@@ -132,9 +152,6 @@
 double mc_results_get_duration (const struct mc_results *);
 
 struct mc_results *mc_run (const struct mc_class *, struct mc_options *);
-struct mc_results *mc_follow_path (const struct mc_class *,
-                                   struct mc_options *,
-                                   int *path, size_t path_len);
 
 bool mc_include_state (struct mc *);
 bool mc_discard_dup_state (struct mc *, unsigned int hash);