diff --git a/README.txt b/README.txt index 39ed1d1599c3dd53310436bf6e33b1d748b1d194..ffdff443b40d50d4993399ca822fbd4f8bb2a23c 100644 --- a/README.txt +++ b/README.txt @@ -75,6 +75,15 @@ following columns: - states: Number of states in the resulting parity game. +## Getting the standard derivation + +This requires the additional tool `perf`. Install it with: + + apt install linux-tools-common + +and change the variable TIME_COMMAND in `bench_one_formula.sh` as +documented there. + ## More information The various scripts in `scripts` contain comments that explain how to diff --git a/scripts/bench_one_formula.sh b/scripts/bench_one_formula.sh index bf5b725a5ac866d1cdf559d3600c557f4864b216..2662ff74566ec56e2146d879a87a23801d01299f 100755 --- a/scripts/bench_one_formula.sh +++ b/scripts/bench_one_formula.sh @@ -21,6 +21,10 @@ # measurements and must output "X seconds time elapsed" for collect_output.pl to # be able to parse it. # +# `/usr/bin/time` doesn't run the program multiple times and computes no +# standard derivation. For this you'd have to install the Linux tool `perf` and +# set TIME_COMMAND as in the first example. +# # Examples: # - perf stat -rNUM # NUM is the repeat count # - /usr/bin/time --format "%e seconds time elapsed"