-"Options:\n"
-"-h Display this help message and exit\n"
-"-m Maximum times a thread can read from the same write\n"
-" while other writes exist. Default: %d\n"
-"-M Maximum number of future values that can be sent to\n"
-" the same read. Default: %d\n"
-"-s Maximum actions that the model checker will wait for\n"
-" a write from the future past the expected number of\n"
-" actions. Default: %d\n"
-"-S Future value expiration sloppiness. Default: %u\n"
-"-f Specify a fairness window in which actions that are\n"
-" enabled sufficiently many times should receive\n"
-" priority for execution. Default: %d\n"
-"-y Turn on CHESS yield-based fairness support.\n"
-" Default: %d\n"
-"-e Enabled count. Default: %d\n"
-"-b Upper length bound. Default: %d\n"
-"-v Print verbose execution information.\n"
-"-u Value for uninitialized reads. Default: %u\n"
-"-c Use SC Trace Analysis.\n"
-"-- Program arguments follow.\n\n",
-params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->yieldon, params->enabledcount, params->bound, params->uninitvalue);
+"MODEL-CHECKER OPTIONS can be any of the model-checker options listed below. Arguments\n"
+"provided after the `--' (the PROGRAM ARGS) are passed to the user program.\n"
+"\n"
+"Model-checker options:\n"
+"-h, --help Display this help message and exit\n"
+"-m, --liveness=NUM Maximum times a thread can read from the same write\n"
+" while other writes exist.\n"
+" Default: %d\n"
+"-M, --maxfv=NUM Maximum number of future values that can be sent to\n"
+" the same read.\n"
+" Default: %d\n"
+"-s, --maxfvdelay=NUM Maximum actions that the model checker will wait for\n"
+" a write from the future past the expected number\n"
+" of actions.\n"
+" Default: %d\n"
+"-S, --fvslop=NUM Future value expiration sloppiness.\n"
+" Default: %u\n"
+"-y, --yield Enable CHESS-like yield-based fairness support.\n"
+" Default: %s\n"
+"-Y, --yieldblock Prohibit an execution from running a yield.\n"
+" Default: %s\n"
+"-f, --fairness=WINDOW Specify a fairness window in which actions that are\n"
+" enabled sufficiently many times should receive\n"
+" priority for execution (not recommended).\n"
+" Default: %d\n"
+"-e, --enabled=COUNT Enabled count.\n"
+" Default: %d\n"
+"-b, --bound=MAX Upper length bound.\n"
+" Default: %d\n"
+"-v, --verbose Print verbose execution information.\n"
+"-u, --uninitialized=VALUE Return VALUE any load which may read from an\n"
+" uninitialized atomic.\n"
+" Default: %u\n"
+"-t, --analysis=NAME Use Analysis Plugin.\n"
+"-o, --options=NAME Option for previous analysis plugin. \n"
+" -o help for a list of options\n"
+" -- Program arguments follow.\n\n",
+ program_name,
+ params->maxreads,
+ params->maxfuturevalues,
+ params->maxfuturedelay,
+ params->expireslop,
+ params->yieldon ? "enabled" : "disabled",
+ params->yieldblock ? "enabled" : "disabled",
+ params->fairwindow,
+ params->enabledcount,
+ params->bound,
+ params->uninitvalue);
+ model_print("Analysis plug ins:\n");
+ for(unsigned int i=0;i<registeredanalysis->size();i++) {
+ TraceAnalysis * analysis=(*registeredanalysis)[i];
+ model_print("%s\n", analysis->name());
+ }