Merge pull request #4259 from smowton/smowton/admin/benchmark-script-improvements

Benchmark script improvements

Author: tautschnig

scripts/benchmark/README.md

@@ -14,7 +14,7 @@ Assuming there is a java maven module installed in `project-name/module-core/`,
 and the `jbmc` main directory is in `/path/to/jbmc`, go to
 `project-name/module-core/target/classes`, and run:
 
-    /path/to/scripts/benchmark/benchmark_java_project.js /path/to/jbmc -l method_list_example.txt -a java_arguments.json -m path/to/jbmc/lib/java-models-library/target/core-models.jar | tee result.json
+    /path/to/scripts/benchmark/benchmark_java_project.js /path/to/jbmc -l method_list_example.txt -a jbmc_arguments_example.json -m path/to/jbmc/lib/java-models-library/target/core-models.jar | tee result.json
 
 This will display the results and save them into the file `result.json`.
 
@@ -29,9 +29,9 @@ This will create a `result.csv` file containing the results.
 # Comparing two runs
 
 Assuming the results have been converted to csv and saved into two files named
-benchmark1.csv and benchmark2.csv:
+develop.csv and branch.csv:
 
      gnuplot draw_scatter.gp
 
-will create a png file `perf_out.png` with the time from the first run on the
-`y` axis and the second on the `x` axis.
+will create a png file `perf_out.png` with the time from the branch / changed run on the
+`y` axis and the develop / original run on the `x` axis.

scripts/benchmark/benchmark_java_project.js

@@ -66,7 +66,7 @@ function readNumberOfGoals(stdout) {
     return 0;
 }
 function readJsonFile(fileName) {
-    return JSON.parse(fs.readFileSync(filename, 'utf8'));
+    return JSON.parse(fs.readFileSync(fileName, 'utf8'));
 }
 
 /// Read the options from tools.json and launch the executable
@@ -92,7 +92,7 @@ function run(executable, modelsPath, argumentsFile, functionName,
     // timeout isn't a jbmc option but only used by this script
     const timeout = config.timeout;
     config['timeout'] = false;
-    commandLine = `${executable} ${classFile} ${configToString(config)}`
+    commandLine = `${executable} ${classFile} ${argsToString(config)}`
     const startTime = new Date();
     try {
         const timeCommand = "export TIME=\"%U\"; /usr/bin/time --quiet -o tmp_time.out "

scripts/benchmark/draw_scatter.gp

@@ -7,8 +7,8 @@ set xrange [30:60000]
 set yrange [30:60000]
 set logscale x 10
 set logscale y 10
-set ylabel 'time (sec.) on branch'
 set xlabel 'time (sec.) on develop'
+set ylabel 'time (sec.) on branch'
 
-plot '< join benchmark1.csv benchmark2.csv' using 6:3 with points, \
+plot '< join develop.csv branch.csv' using 3:6 with points, \
   x with lines