"Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
"\n"
"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"
"Usage: <program name> [MC_OPTIONS] -- [PROGRAM ARGUMENTS]\n"
"\n"
"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"
"-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 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"
"-f Specify a fairness window in which actions that are\n"
" enabled sufficiently many times should receive\n"
" priority for execution. Default: %d\n"
"-e Enabled count. Default: %d\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"
"-e Enabled count. Default: %d\n"
-params->maxreads, params->maxfuturedelay, params->fairwindow, params->enabledcount);
+params->maxreads, params->maxfuturevalues, params->maxfuturedelay, params->expireslop, params->fairwindow, params->enabledcount, params->bound);
/* Wait for all threads to complete */
model->finish_execution();
} while (model->next_execution());
/* Wait for all threads to complete */
model->finish_execution();
} while (model->next_execution());
/* Let's jump in quickly and start running stuff */
initSnapshotLibrary(10000, 1024, 1024, 4000, &model_main);
}
/* Let's jump in quickly and start running stuff */
initSnapshotLibrary(10000, 1024, 1024, 4000, &model_main);
}