From: Brian Norris <banorris@uci.edu>
Date: Wed, 14 Nov 2012 04:05:45 +0000 (-0800)
Subject: README: more edits, for -h info
X-Git-Tag: pldi2013
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=6b87c110fbda87ccec4f58b1e292d5f9434c8691

README: more edits, for -h info
---

diff --git a/README b/README
index 10af03d..e403c48 100644
--- 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