patchPSPP - Patches: patch #5873, Model checker and initial...

 
 

You are not allowed to post comments on this tracker with your current authentication level.

patch #5873: Model checker and initial datasheet review

Submitter:  Ben Pfaff <blp>
Submitted:  Wed 18 Apr 2007 11:28:41 PM UTC
   
 
Category:  None Item Group:  None
Status:  Done Assigned to:  None
Open/Closed:  Closed

Mon 23 Apr 2007 01:27:13 AM UTC, comment #4: 

I checked this in.

Ben Pfaff <blp>
Group administrator
Sun 22 Apr 2007 08:47:41 PM UTC, comment #3: 

Oops, some more feedback I missed on first pass.

>in datasheet.c, where you have NDEBUG should this be replaced by
>DEBUGGING ?


I think I'll just delete it, anything here will be caught by Valgrind runs.

>The comment in the body of check_datasheet is not grammatically
>correct.


Thanks, fixed.

Ben Pfaff <blp>
Group administrator
Sun 22 Apr 2007 05:05:55 PM UTC, comment #2: 

Thanks for the review.

>Regarding the model checker, I haven't read the references you
>gave, but it seems that it's important to realize that it's
>testing only the model, and the 2nd implementation of it. Errors
>in the real implementation will go unchecked. Could the 2nd
>implementation not be a wrapper around the 1st?


I think that you misunderstand.  The model checker essentially compares the two implementations.  Any differences between them will be found (given a few provisos).  Thus, any error in either implementation will be found, as long as both implementations don't have the same error.

>There's a typo on model-checker.h:90


Thanks, fixed.

>mc_get_options, mc_get_results and mc_get_aux could take const arguments.


Ditto.

>The 2nd arg of mc_run could also be const ?


Actually, no, it destroys that argument.

> In mc_options_set_hash_bits, from whence comes the number 31 ?
>Should this be higher on 64 bit machines?


I wanted a value such that (1u << hash_bits) is guaranteed to be well-defined.  I'll rewrite it as CHAR_BIT * sizeof (unsigned int) - 1 to make this more clear.

>I'm not sure about the portability of gettimeofday


There's a gnulib module that makes it portable, which I'm using (I didn't add this change to the tarball, so you didn't spot it).

>The datasheet looks promising. I hope it'll be able to displace
>much of the code in lib/gtksheet and probably
>psppire-data-store.* and others.


I've done some of that work in the simpler-proc branch already.  It compiles; I haven't tried to run it yet.

>It will be necessary for struct datasheet to have a whole bunch
>of user specified callback functions which get called whenever
>something in the datasheet changes. 


OK.

>Presumably struct casereader is a different animal to the
>structure that we currently have with that identifier?


Yes, very much so.  Don't worry, I'll document it and put it up for review, etc., before it gets into mainline.

> In datasheet_move_rows, the only thing the comments don't make
>clear is whether or not the source and destination ranges are
>permitted to overlap.


Overlap can't happen, because of the way that the move occurs.  I added the following to the comment.  Does it make the way that the move occurs clear?

   Equivalent to
   deleting the given rows, then inserting them at what becomes
   position NEW_START after the deletion.

And similarly for datasheet_move_columns.




Ben Pfaff <blp>
Group administrator
Sat 21 Apr 2007 05:07:27 AM UTC, comment #1: 

Regarding the model checker, I haven't read the references you gave, but it seems that it's important to realize that it's testing only the model, and the 2nd implementation of it.  Errors in the real implementation will go unchecked.  Could the 2nd implementation not be a wrapper around the 1st?


There's a typo on model-checker.h:90

model-checker.c:

mc_get_options, mc_get_results and mc_get_aux could take const arguments.

The 2nd arg of mc_run could also be const ?

In mc_options_set_hash_bits, from whence comes the number 31 ?  Should this be higher on 64 bit machines?

I'm not sure about the portability of gettimeofday


The datasheet looks promising.  I hope it'll be able to displace much of the code in lib/gtksheet and probably psppire-data-store.* and others.

It will be necessary for struct datasheet to have a whole bunch of user specified callback functions which get called whenever something in the datasheet changes.

Presumably struct casereader is a different animal to the structure that we currently have with that identifier?

In datasheet_move_rows, the only thing the comments don't make clear is whether or not the source and destination ranges are permitted to overlap.


in datasheet.c, where you have NDEBUG should this be replaced by DEBUGGING ?

The comment in the body of check_datasheet is not grammatically correct.




John Darrington <jmd>
Group administrator
Wed 18 Apr 2007 11:28:41 PM UTC, original submission:  

This set of changes implements a model checker and a PSPP syntax interface to the model checker.  My goal is to check these into the main branch after applying reviewers' comments; they are already in the simpler-proc branch.

These changes also include the current draft of the datasheet implementation for use by the GUI.  This is because the datasheet code is currently the model checker's only client, so it can serve as an example use of the model checker for the enlightenment of reviewers.  I don't intend to immediately check the datasheet code into the main branch, because it depends on the casereader code that isn't yet in the main branch (and is not itself ready for check-in), and because the datasheet's name is likely to change before final check-in (and I don't think we came to a final decision on its new name).  I'd still be happy to receive any or all feedback on the datasheet's code or design.

A model checker is a tool for software testing and verification
that works by exploring all the possible states in a system and
verifying their internal consistency.  A conventional model
checker requires that the code in a system be translated into a
specification language.  The model checker then verifies the
specification, rather than the code.

This is instead an implementation-level model checker, which does
not require a separate specification.  Instead, the model checker
requires writing a second implementation of the system being
checked.  The second implementation can usually be made almost
trivial in comparison to the one being checked, because it's
usually acceptable for its performance to be comparatively poor,
e.g. O(N^2) instead of O(lg N), and thus to use much simpler
algorithms.

The "models" used by model checkers have little or nothing to do with the "models" used in statistics.  I didn't use the prefix "model_" for that reason; PSPP is about statistics, not about model checking, so it seems better to reserve "model_" for statistical purposes.

Ben Pfaff <blp>
Group administrator

 

(Note: upload size limit is set to 16384 kB, after insertion of the required escape characters.)

Attached Files
file #12524:  datasheet.tar.gz added by blp (32KiB - application/gzip)

 

Depends on the following items: None found

Items that depend on this one: None found

 

Carbon-Copy List
  • -email is unavailable- added by jmd (Posted a comment)
  • -email is unavailable- added by blp (Submitted the item)
  •  

    There are 0 votes so far. Votes easily highlight which items people would like to see resolved in priority, independently of the priority of the item set by tracker managers.

     

    Follow 3 latest changes.

    Date Changed by Updated Field Previous Value => Replaced by
    2007-04-23 blp StatusReady For Test/Review Done
        Open/ClosedOpen Closed
    2007-04-18 blp Attached File- Added datasheet.tar.gz, #12524

    Back to the top

    Powered by Savane 3.13-02a9.
    Corresponding source code