X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=main.cc;h=122539811e8f36c0b86f7fadbe823ca6cdbee29a;hb=17b667f2d53729212d23e62a3f9464b8180e01f6;hp=635b8da70bc213e3db6524c964e78301b1b28ebf;hpb=15fabc6f4e6591341940a8087a8dd088af59bb5c;p=model-checker.git diff --git a/main.cc b/main.cc index 635b8da..1225398 100644 --- a/main.cc +++ b/main.cc @@ -20,9 +20,13 @@ static void param_defaults(struct model_params * params) { params->fairwindow = 0; params->enabledcount = 1; params->bound = 0; + params->maxfuturevalues = 0; } static void print_usage(struct model_params *params) { + /* Reset defaults before printing */ + param_defaults(params); + printf( "Usage: [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n" "\n" @@ -30,6 +34,8 @@ static void print_usage(struct model_params *params) { "-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" @@ -39,12 +45,12 @@ static void print_usage(struct model_params *params) { "-e Enabled count. Default: %d\n" "-b Upper length bound. Default: %d\n" "-- Program arguments follow.\n\n", -params->maxreads, params->maxfuturedelay, params->fairwindow, params->enabledcount, params->bound); +params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->fairwindow, params->enabledcount, params->bound); exit(EXIT_SUCCESS); } static void parse_options(struct model_params *params, int *argc, char ***argv) { - const char *shortopts = "hm:s:f:e:b:"; + const char *shortopts = "hm:M:s:f:e:b:"; int opt; bool error = false; while (!error && (opt = getopt(*argc, *argv, shortopts)) != -1) { @@ -67,6 +73,9 @@ static void parse_options(struct model_params *params, int *argc, char ***argv) case 'm': params->maxreads = atoi(optarg); break; + case 'M': + params->maxfuturevalues = atoi(optarg); + break; default: /* '?' */ error = true; break;