From: Ben Pfaff <blp@gnu.org>
Date: Tue, 5 May 2009 05:27:05 +0000 (-0700)
Subject: model-checker: Revise advice on checking for duplicates.
X-Git-Tag: v0.7.3~91
X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pspp-builds.git;a=commitdiff_plain;h=d724fe4838db898a323102e4f2981af90c9ea132

model-checker: Revise advice on checking for duplicates.

Until now the documentation on the model checker has advised checking for
a duplicate state before checking for consistency, but in fact this can
cause bugs to be missed if only some paths to a given state yield
incorrect results.  So revise the advice to check for consistency before
checking for a duplicate state.
---

diff --git a/src/libpspp/model-checker.h b/src/libpspp/model-checker.h
index 1e756119..205c3fac 100644
--- a/src/libpspp/model-checker.h
+++ b/src/libpspp/model-checker.h
@@ -150,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);
                 }
           }
 
@@ -204,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