From 6fca912a465128b36b5c6b107bfc73547df88044 Mon Sep 17 00:00:00 2001 From: Amanda Stjerna Date: Thu, 7 Mar 2024 21:26:18 +0100 Subject: [PATCH] Add a straightforward experiment runner --- 120s-baseline.sh | 18 ------------------ 120s-experiments.sh | 15 --------------- oopsla-experiments.sh | 11 +++++++++-- 3 files changed, 9 insertions(+), 35 deletions(-) delete mode 100755 120s-baseline.sh delete mode 100755 120s-experiments.sh mode change 100644 => 100755 oopsla-experiments.sh diff --git a/120s-baseline.sh b/120s-baseline.sh deleted file mode 100755 index 6ab5f9fe..00000000 --- a/120s-baseline.sh +++ /dev/null @@ -1,18 +0,0 @@ -#!/bin/bash -set -x - -LOGFILE="baseline-120s.log" -JARFILE=$(ls -1t target/scala-2.13/uuverifiers/*.jar | head -1) - -echo "" > "$LOGFILE" - -for instance in 120s-experiments.d/* -do - timeout --signal 9 --preserve-status 300s \ - java -Xmx20G -jar $JARFILE \ - solve-satisfy --backend baseline \ - --timeout 120000 $instance $instance -done | tee -a "$LOGFILE" - - -echo "Done with all experiments!" >> "$LOGFILE" \ No newline at end of file diff --git a/120s-experiments.sh b/120s-experiments.sh deleted file mode 100755 index ceacc261..00000000 --- a/120s-experiments.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/bash -set -x -RESTART_AFTER=10 -export CATRA_TIMEOUT=120000 -export CATRA_CONFIGS="nuxmv,lazy" -export CATRA_THREADS=1 -LOGFILE="${CATRA_CONFIGS}-catra-${RESTART_AFTER}.${CATRA_TIMEOUT}.log" -JARFILE=$(ls -1t benchmark/target/scala-2.13/*.jar | head -1) - -echo "" > "$LOGFILE" - -find 120s-experiments.d -type f | xargs -n $RESTART_AFTER -- \ - java -Xmx10G -jar "$JARFILE" | tee -a "$LOGFILE" - -echo "Done with all experiments!" >> "$LOGFILE" diff --git a/oopsla-experiments.sh b/oopsla-experiments.sh old mode 100644 new mode 100755 index 3f542054..de0ba95f --- a/oopsla-experiments.sh +++ b/oopsla-experiments.sh @@ -1,4 +1,11 @@ #!/bin/sh -CATRA_TAG=".cactus" CATRA_TIMEOUT="120000" ./bin/experiments.sh ../parikh-plus-selected -CATRA_TIMEOUT="30000" CATRA_CONFIGS="nuxmv,baseline,lazy" ./bin/experiments.sh ../deduped-benchmarks +# 120s benchmarks: +CATRA_TIMEOUT=120000\ + CATRA_CONFIGS="nuxmv,lazy,lazy-no-clauselearning-no-restarts,lazy-eager-1,lazy-lazy-200" \ + CATRA_THREADS=4 ./bin/experiments.sh 120s-experiments.d +CATRA_TIMEOUT=120000 CATRA_CONFIGS=baseline CATRA_THREADS=2 ./bin/experiments.sh 120s-experiments.d + +# 30s benchmarks: +CATRA_TIMEOUT=30000 CATRA_CONFIGS=lazy,nuxmv CATRA_THREADS=6 ./bin/experiments.sh deduped-benchmarks +CATRA_TIMEOUT=30000 CATRA_CONFIGS=baseline CATRA_THREADS=2 ./bin/experiments.sh deduped-benchmarks