"model-check/strategy",
"Specify the the kind of heuristic to use for guided model-checking",
"none",
- {{"none", "No specific strategy: simply pick the first available transistion and act as a DFS."},
+ {{"none", "No specific strategy: simply pick the first available transition and act as a DFS."},
{"max_match_comm", "Try to minimize the number of in-fly communication by appairing matching send and receive."},
{"min_match_comm", "Try to maximize the number of in-fly communication by not appairing matching send and receive."},
{"uniform", "No specific strategy: choices are made randomly based on a uniform sampling."}
(name, path, binary, filename) = sys.argv
for test in mbi.parse_one_code(filename):
- execcmd = test['cmd'].replace("mpirun", f"{path}/smpi_script/bin/smpirun -wrapper '{path}/bin/simgrid-mc --log=mc_safety.t:info' -platform ./cluster.xml -analyze --cfg=smpi/barrier-finalization:on --cfg=smpi/list-leaks:10 --cfg=model-check/max-depth:10000")
+ execcmd = test['cmd'].replace("mpirun", f"{path}/smpi_script/bin/smpirun -wrapper '{path}/bin/simgrid-mc --cfg=model-check/reduction:odpor --log=mc_safety.t:info' -platform ./cluster.xml -analyze --cfg=smpi/barrier-finalization:on --cfg=smpi/list-leaks:10 --cfg=model-check/max-depth:10000")
execcmd = execcmd.replace('${EXE}', binary)
execcmd = execcmd.replace('$zero_buffer', "--cfg=smpi/buffering:zero")
execcmd = execcmd.replace('$infty_buffer', "--cfg=smpi/buffering:infty")