X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Flibpspp%2Fmodel-checker.h;h=be97d389bcc7219c8dd325e02900f829b2082077;hb=81579d9e9f994fb2908f50af41c3eb033d216e58;hp=adef475d3289c47b9616cefc24a5a72f07c9ecd3;hpb=f5c108becd49d78f4898cab11352291f5689d24e;p=pspp-builds.git

diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h
index adef475d..be97d389 100644
--- a/src/libpspp/model-checker.h
+++ b/src/libpspp/model-checker.h
@@ -1,20 +1,18 @@
-/* PSPP - computes sample statistics.
-   Copyright (C) 2007 Free Software Foundation, Inc.
+/* PSPP - a program for statistical analysis.
+   Copyright (C) 2007, 2009, 2011 Free Software Foundation, Inc.
 
-   This program is free software; you can redistribute it and/or
-   modify it under the terms of the GNU General Public License as
-   published by the Free Software Foundation; either version 2 of the
-   License, or (at your option) any later version.
+   This program is free software: you can redistribute it and/or modify
+   it under the terms of the GNU General Public License as published by
+   the Free Software Foundation, either version 3 of the License, or
+   (at your option) any later version.
 
-   This program is distributed in the hope that it will be useful, but
-   WITHOUT ANY WARRANTY; without even the implied warranty of
-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-   General Public License for more details.
+   This program is distributed in the hope that it will be useful,
+   but WITHOUT ANY WARRANTY; without even the implied warranty of
+   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+   GNU General Public License for more details.
 
    You should have received a copy of the GNU General Public License
-   along with this program; if not, write to the Free Software
-   Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
-   02110-1301, USA. */
+   along with this program.  If not, see <http://www.gnu.org/licenses/>. */
 
 /* Implementation-level model checker.
 
@@ -152,14 +150,12 @@
                   mc_name_operation (mc, "do operation %s", ...);
                   clone = clone_foo (state);
                   do_operation (clone);
-                  if (!mc_discard_dup_state (mc, hash_foo (clone)))
-                    {
-                      if (!state_is_consistent (clone))
-                        mc_error (mc, "inconsistent state");
-                      mc_add_state (mc, clone);
-                    }
-                  else
+                  if (!state_is_consistent (clone))
+                    mc_error (mc, "inconsistent state");
+                  if (mc_discard_dup_state (mc, hash_foo (clone)))
                     destroy_foo (clone);
+                  else
+                    mc_add_state (mc, clone);
                 }
           }
 
@@ -206,10 +202,10 @@
             the metadata.
 
             mc_discard_dup_state may be called before or after
-            checking for consistency, but calling it first avoids
-            wasting time checking duplicate states for
-            consistency, which again can be a significant
-            performance boost.
+            checking for consistency.  Calling it after checking
+            may make checking a given number of unique states
+            take longer, but it also ensures that all paths to a
+            given state produce correct results.
 
           - The mc_error function reports errors.  It may be
             called as many times as desired to report each kind
@@ -302,7 +298,7 @@
 #include <stdio.h>
 #include <sys/time.h>
 
-#include <libpspp/compiler.h>
+#include "libpspp/compiler.h"
 
 /* An active model checking run. */
 struct mc;
@@ -420,6 +416,10 @@ FILE *mc_options_get_output_file (const struct mc_options *);
 void mc_options_set_output_file (struct mc_options *, FILE *);
 
 typedef bool mc_progress_func (struct mc *);
+mc_progress_func mc_progress_dots;
+mc_progress_func mc_progress_fancy;
+mc_progress_func mc_progress_verbose;
+
 int mc_options_get_progress_usec (const struct mc_options *);
 void mc_options_set_progress_usec (struct mc_options *, int progress_usec);
 mc_progress_func *mc_options_get_progress_func (const struct mc_options *);
@@ -427,6 +427,11 @@ void mc_options_set_progress_func (struct mc_options *, mc_progress_func *);
 
 void *mc_options_get_aux (const struct mc_options *);
 void mc_options_set_aux (struct mc_options *, void *aux);
+
+struct argv_parser;
+void mc_options_register_argv_parser (struct mc_options *,
+                                      struct argv_parser *);
+void mc_options_usage (void);
 
 /* Reason that a model checking run terminated. */
 enum mc_stop_reason
@@ -462,4 +467,6 @@ struct timeval mc_results_get_start (const struct mc_results *);
 struct timeval mc_results_get_end (const struct mc_results *);
 double mc_results_get_duration (const struct mc_results *);
 
+void mc_results_print (const struct mc_results *, FILE *);
+
 #endif /* libpspp/model-checker.h */