From f3a6fc6949b0b3f17ca77f1a87036a1996a4ae21 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 22 Jul 2018 14:17:26 +0100
Subject: [PATCH] Benchmarking script

---
 drs_benchmark.sh | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100755 drs_benchmark.sh

diff --git a/drs_benchmark.sh b/drs_benchmark.sh
new file mode 100755
index 0000000..cd69944
--- /dev/null
+++ b/drs_benchmark.sh
@@ -0,0 +1,35 @@
+#!/bin/sh
+
+TMPINPUT="tmp_$RANDOM$RANDOM.rs"
+
+CMD="./reactics -b -B"
+
+for i in `seq 2 10`;do
+
+	echo "[i] n=$i; generating input file"
+	in/gen_drs_mutex.py $i > $TMPINPUT
+
+	for f in `seq 1 2`; do
+
+		echo "[i] Testing formula f$f"
+
+		TMPCMD="$CMD -c f$f $TMPINPUT"
+		echo "[i] running reactics: $TMPCMD"
+
+		res=$($TMPCMD | grep STAT)
+		mem=$(echo $res | cut -d';' -f 5)
+		time=$(echo $res | cut -d';' -f 6)
+
+		echo "[.] Finished. time:$time, mem:$mem"
+
+		echo "$i $time $mem"  >> results_f$f.out
+
+	done
+
+	echo 
+	
+done
+
+rm -f $TMPINPUT
+
+# EOF
\ No newline at end of file