README: more edits, for -h info

diff --git a/README b/README
index 10af03de4e050fb4e4bfdfbbf19199214eb35d30..e403c487616d30438edb5c71dfe9bbf56892e572 100644 (file)
--- a/README
+++ b/README
@@ -25,9 +25,29 @@ variable, for instance.
 
 Sample run instructions:
 
-  make
-  export LD_LIBRARY_PATH=.
-  # run test program
+$ make
+$ export LD_LIBRARY_PATH=.
+$ ./test/userprog.o                   # Runs simple test program
+$ ./test/userprog.o -h                # Prints help information
+Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]
+
+Options:
+-h                    Display this help message and exit
+-m                    Maximum times a thread can read from the same write
+                      while other writes exist. Default: 0
+-M                    Maximum number of future values that can be sent to
+                      the same read. Default: 0
+-s                    Maximum actions that the model checker will wait for
+                      a write from the future past the expected number of
+                      actions. Default: 100
+-S                    Future value expiration sloppiness. Default: 10
+-f                    Specify a fairness window in which actions that are
+                      enabled sufficiently many times should receive
+                      priority for execution. Default: 0
+-e                    Enabled count. Default: 1
+-b                    Upper length bound. Default: 0
+--                    Program arguments follow.
+
 
 Note that we also provide a series of benchmarks, placed under the benchmarks/
 directory. After building CDSChecker, you can build and run the benchmarks as