let verify_arg_spec () = [
(arg_spec_of_symbols
"-mc-engine"
mc_engine_names
mc_engine_opt
"Model-checking engine")
;
(arg_spec_of_symbols
"-tc-engine"
tc_engine_names
tc_engine_opt
"Trace-checking engine")
;
(arg_spec_of_integer
"-k-min"
(-1)
k_min_opt
"Minimum value of extrapolation parameter")
;
(arg_spec_of_integer
"-k-max"
0
k_max_opt
"Maximum value of extrapolation parameter")
;
("-tc-discard-states",
Arg.Set tc_discard_states_opt,
" Ignore abstract states for trace checking")
;
("-tc-validate",
Arg.Set tc_validate_opt,
" Validate all trace-checking results")
;
(arg_spec_of_integer
"-limit"
0
limit_opt
"Maximum number of model-checker iterations")
;
("-no-scm-consistency-check",
Arg.Clear scm_consistency_check_opt,
" Disable consistency check of input SCM description")
;
("-no-validation",
Arg.Clear result_validation_opt,
" Disable validation of the model-checking result")
;
("-statistics",
Arg.Set show_statistics_opt,
" Show performance statistics")
]
Loading...