Commit ad6feb7a authored by Etienne Renault's avatar Etienne Renault
Browse files

bench: fix timing options

* benchs/run-benchmark.sh: Here;
parent 85c0e480
Pipeline #24474 passed with stage
in 2 minutes and 12 seconds
......@@ -99,14 +99,14 @@ for model in $LTLFILES; do
# Compute Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s)
start=$(date +%s.%N)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -backend ltsmin 2>&1)
end=$(date +%s)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s)
start=$(date +%s.%N)
RESS=$($filename/go2pins-mc -ltl "$formulae" 2>&1)
end=$(date +%s)
end=$(date +%s.%N)
spot_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
......@@ -149,14 +149,14 @@ for model in $FILES; do
# Compute Spot resolution time
LTSMIN_F=$(echo $formulae | sed 's/"//g')
start=$(date +%s)
start=$(date +%s.%N)
RESL=$($filename/go2pins-mc -ltl "$LTSMIN_F" -backend ltsmin 2>&1)
end=$(date +%s)
end=$(date +%s.%N)
ltsmin_time=$(python -c "print ('%.3f' % (${end} - ${start}))")
start=$(date +%s)
start=$(date +%s.%N)
RESS=$($filename/go2pins-mc -ltl "$formulae" 2>&1)
end=$(date +%s)
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