These are sources for "The SmlMC Model Checker" as described in
DrDobbs Journal. Notice that there is also a web page for this 
project:
  http://members.ams.chello.nl/w.m.boeke/SmlMC/index.html

To compile example file buffer.sml (supposing that Moscow ML
has been installed):

The first time:

- Go to directory sml_lib
- Edit the makefile, especially the path's.
- Command: make
- Go to directory SmlMC
- Edit the makefile

Later:

- In directory SmlMC, give command:
        make DUT=buffer
  (DUT means: Device Under Test)
- An executable file 'buffer' will have been created in
  directory 'examples'
- This can be run. Options are shown if run with option -h

Possible problems:

1 - The makefile for SmlMC contains a construct to maintain a 
    symbolic link called dut.sml to the file with your SML code.
    In Unix (shell: sh or bash) this works fine. In case of 
    trouble (Windows?) an alternative is given in the makefile.
    If this is chosen then recompilation will occur after each
    make command, also when it's not needed.

2 - It is supposed that Moscow ML version 2.01 has been
    installed. If your version is 2.0, then the compiler will
    complain that function hash_safe_param in file SmlMC_gen.sml
    is  unknown. In this case replace hash_safe_param with
    hash_param, which has the same functionality but does not
    check for references and loops in hashed data.

3 - Function hash_safe_param is parameterised with values
    500 and 1000. If in your code very big data structures are
    present then an error "hash: count limit exceeded" may be 
    reported. In this case increase these values.

Several demos are in directory 'examples', each with their own
peculiarities. See README.html for a description.
