Commit 380f320f authored by Etienne Renault's avatar Etienne Renault

bench: propagate use of multithreading

* benchs/run-benchmark.sh: Here.
parent ec0f2d13
Pipeline #26033 passed with stage
in 4 minutes and 31 seconds
......@@ -133,12 +133,12 @@ for model in $LTLFILES; do
# Compute LTSmin Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s.%N)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -backend ltsmin 2>&1)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$($filename/go2pins-mc -ltl "$formulae" 2>&1)
RESS=$($filename/go2pins-mc -ltl "$formulae" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
......@@ -194,12 +194,12 @@ for model in $FILES; do
# Compute LTSmin and Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s.%N)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -backend ltsmin 2>&1)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -nb-threads $NBTHREADS -backend ltsmin 2>&1)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s.%N)
RESS=$($filename/go2pins-mc -ltl "$formulae" 2>&1)
RESS=$($filename/go2pins-mc -ltl "$formulae" -nb-threads $NBTHREADS -backend spot 2>&1)
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment