[Pspp-cvs] pspp/src/libpspp model-checker.h model-checker.c [simpler-proc]

[Ben Pfaff]

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

Modified files:
        src/libpspp    : model-checker.h model-checker.c 

Log message:
        Improve model checker according to review comments from John
        Darrington.

CVSWeb URLs:
http://cvs.savannah.gnu.org/viewcvs/pspp/src/libpspp/model-checker.h?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/libpspp/model-checker.c?cvsroot=pspp&only_with_tag=simpler-proc&r1=1.1.2.4&r2=1.1.2.5

Patches:
Index: model-checker.h
===================================================================
RCS file: /cvsroot/pspp/pspp/src/libpspp/Attic/model-checker.h,v
retrieving revision 1.1.2.5
retrieving revision 1.1.2.6
diff -u -b -r1.1.2.5 -r1.1.2.6
--- model-checker.h     19 Apr 2007 03:59:40 -0000      1.1.2.5
+++ model-checker.h     22 Apr 2007 17:05:30 -0000      1.1.2.6
@@ -87,7 +87,7 @@
    pursuing a few stratagems:
 
      1. Limit the maximum size of the system; for example, limit
-        the number of rows and columns in the implmentation of a
+        the number of rows and columns in the implementation of a
         table being checked.  The client of the model checker is
         responsible for implementing such limits.
 
@@ -336,9 +336,9 @@
 
 /* Functions for use from client-supplied "init", "mutate", and
    "destroy" functions. */
-const struct mc_options *mc_get_options (struct mc *);
-const struct mc_results *mc_get_results (struct mc *);
-void *mc_get_aux (struct mc *);
+const struct mc_options *mc_get_options (const struct mc *);
+const struct mc_results *mc_get_results (const struct mc *);
+void *mc_get_aux (const struct mc *);
 
 /* A path of operations through a model to arrive at some
    particular state. */

Index: model-checker.c
===================================================================
RCS file: /cvsroot/pspp/pspp/src/libpspp/Attic/model-checker.c,v
retrieving revision 1.1.2.4
retrieving revision 1.1.2.5
diff -u -b -r1.1.2.4 -r1.1.2.5
--- model-checker.c     18 Apr 2007 05:07:32 -0000      1.1.2.4
+++ model-checker.c     22 Apr 2007 17:05:30 -0000      1.1.2.5
@@ -334,7 +334,7 @@
 mc_options_set_hash_bits (struct mc_options *options, int hash_bits) 
 {
   assert (hash_bits >= 0);
-  options->hash_bits = MIN (hash_bits, 31);
+  options->hash_bits = MIN (hash_bits, CHAR_BIT * sizeof (unsigned int) - 1);
 }
 
 /* Returns the path set in OPTIONS by mc_options_set_follow_path.
@@ -1118,7 +1118,7 @@
 /* Returns the options that were passed to mc_run for model
    checker MC. */
 const struct mc_options *
-mc_get_options (struct mc *mc) 
+mc_get_options (const struct mc *mc) 
 {
   return mc->options;
 }
@@ -1130,7 +1130,7 @@
    Not all of the results are meaningful before model checking
    completes. */
 const struct mc_results *
-mc_get_results (struct mc *mc) 
+mc_get_results (const struct mc *mc) 
 {
   return mc->results;
 }
@@ -1138,7 +1138,7 @@
 /* Returns the auxiliary data set on the options passed to mc_run
    with mc_options_set_aux. */
 void *
-mc_get_aux (struct mc *mc) 
+mc_get_aux (const struct mc *mc) 
 {
   return mc_options_get_aux (mc_get_options (mc));
 }