Merge pull request #53 from amandasystems/empty-sets-zero

Configure experiments

120s-experiments.sh

@@ -0,0 +1,15 @@
+#!/bin/bash
+set -x
+RESTART_AFTER=10
+export CATRA_TIMEOUT=120000
+export CATRA_CONFIGS="baseline,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"

Makefile

@@ -1,10 +1,21 @@
-current_version = $(shell git rev-parse --short HEAD)
+current_version = $(shell sbt -Dsbt.supershell=false -error "print version")
 TIMEOUT_MS = 30000
 EXPERIMENT_DIR = parikh-plus
 
 .PHONY: all
 all: experiments
 
+catra-experiments.zip: build.sbt
+	sbt benchmark/assembly
+	zip catra-experiments.zip \
+		-r 120s-experiments.* \
+		$(shell ls -1t benchmark/target/scala-2.13/*.jar | head -1)
+
+catra-${current_version}.zip:
+	sbt assembly
+	zip catra-${current_version}.zip  bin/catra target/scala-2.13/uuverifiers/catra-assembly-${current_version}.jar	
+
+
 clean:
 	sbt clean
 

benchmark/src/main/scala/RunBenchmarks.scala

@@ -10,54 +10,43 @@ import scala.util.{Failure, Random, Success, Try}
 
 object RunBenchmarks extends App {
   import catra.SolveRegisterAutomata.measureTime
-  private val regularTimeout = sys.env.getOrElse("CATRA_TIMEOUT", "30000").toInt
-  private val nrMaterialiseEager = 500
+  private val timeout =
+    sys.env.getOrElse("CATRA_TIMEOUT", "30000").toInt
+  private val nrMaterialiseEager = 200
   private val nrMaterialiseLazy = 1
-  private val cactusTimeout = "120000"
   private val baseConfigurations = Map(
     "nuxmv" -> Array("--backend", "nuxmv"),
     "baseline" -> Array("--backend", "baseline"),
-    "lazy-new" -> Array("--backend", "lazy"),
-    "lazy-old" -> Array("--backend", "lazy", "--old-behaviour") /*,
-    // Cactus plot entries:
-
-    "baseline-cactus" -> Array(
+    "lazy" -> Array("--backend", "lazy"),
+    "lazy-no-clauselearning" -> Array(
       "--backend",
-      "baseline",
-      "--timeout",
-      cactusTimeout
+      "lazy",
+      "--no-clause-learning"
     ),
-    "lazy-cactus" -> Array("--backend", "lazy", "--timeout", cactusTimeout),
-    "lazy-no-clauselearning" -> Array(
+    "lazy-no-clauselearning-no-restarts" -> Array(
       "--backend",
       "lazy",
       "--no-restarts",
-      "--no-clause-learning",
-      "--timeout",
-      cactusTimeout
+      "--no-clause-learning"
     ),
     s"lazy-eager-$nrMaterialiseEager" -> Array(
       "--backend",
       "lazy",
       "--nr-unknown-to-start-materialise",
-      nrMaterialiseEager.toString,
-      "--timeout",
-      cactusTimeout
+      nrMaterialiseEager.toString
     ),
     s"lazy-lazy-$nrMaterialiseLazy" -> Array(
       "--backend",
       "lazy",
       "--nr-unknown-to-start-materialise",
-      nrMaterialiseLazy.toString,
-      "--timeout",
-      cactusTimeout
-    )*/
+      nrMaterialiseLazy.toString
+    )
   ).view
     .mapValues(
       c =>
         catra.CommandLineOptions
           .parse(
-            Array("solve-satisfy", "--timeout", regularTimeout.toString) ++ c
+            Array("solve-satisfy", "--timeout", timeout.toString) ++ c
           )
           .get
     )
@@ -67,8 +56,8 @@ object RunBenchmarks extends App {
     .getOrElse("CATRA_CONFIGS", baseConfigurations.keys.mkString(","))
     .split(",")
     .toSet
-  private val filteredConfigurations = baseConfigurations
-  //  baseConfigurations.view.filterKeys(selectConfigurations).toMap
+  private val filteredConfigurations =
+    baseConfigurations.view.filterKeys(selectConfigurations.contains).toMap
 
   private val instanceFiles =
     args.flatMap(catra.CommandLineOptions.expandFileNameOrDirectoryOrGlob)
@@ -104,8 +93,7 @@ object RunBenchmarks extends App {
   }.toSeq)
 
   private val runtime = Runtime.getRuntime
-//  private val nrWorkers = runtime.availableProcessors / 4
-  private val nrWorkers = 1
+  private val nrWorkers = sys.env.getOrElse("CATRA_THREADS", "6").toInt
 
   print(
     s"INFO ${Calendar.getInstance().getTime} JVM version: ${System.getProperty("java.version")}"
@@ -123,41 +111,50 @@ object RunBenchmarks extends App {
     .solveSatisfy(instances(0)._2)
   println("...warm-up done!")
 
-  private val (_, totalTimeSpent) = measureTime {
+  private val (exitCode, totalTimeSpent) = measureTime {
     val runner = new ExperimentRunner(experiments, nrWorkers)
 
     println(s"CONFIGS ${configNames.mkString("\t")}")
     filteredConfigurations.foreachEntry {
       case (name, config) =>
         println(s"CONFIG $name IS $config")
     }
-    println(s"TIMEOUT $regularTimeout")
+    println(s"TIMEOUT $timeout")
 
     val safetyMargin = 1000 * experiments.length
     val maxTimeout = Duration(
-      (experiments.length * regularTimeout) + safetyMargin,
+      (experiments.length * timeout) + safetyMargin,
       duration.MILLISECONDS
     )
 
     println(s"HARD TIMEOUT $maxTimeout FOR ALL")
 
-    runner.results(maxTimeout) match {
-      case Failure(_: TimeoutException) =>
+    val exitCode = runner.results(maxTimeout) match {
+      case Failure(_: TimeoutException) => {
         println("ERR hard timeout, some experiment is misbehaving!")
-      case Failure(e) => println(s"ERR unknown error running experiments: $e")
-      case Success(outcomes) =>
+        1
+      }
+      case Failure(e) => {
+        println(s"ERR unknown error running experiments: $e")
+        1
+      }
+      case Success(outcomes) => {
         for ((instance, rs) <- outcomes) {
           val rsMap = rs.toMap
           println(
             s"RESULT $instance\t${configNames.map(c => fmtResult(rsMap(c))).mkString("\t")}"
           )
         }
+        0
+      }
     }
     runner.stop()
+    exitCode
   }
 
   println(
     s"INFO ${Calendar.getInstance().getTime} Executed ${experiments.length} experiments with ${filteredConfigurations.size} configurations and ${instances.length} instances in $totalTimeSpent."
   )
+  System.exit(exitCode)
 
 }

bin/experiments.sh

@@ -11,6 +11,6 @@ echo "" > $LOGFILE
 
 echo "${CURRENT_VERSION}: Executing experiments in parallel, logging to ${LOGFILE}"
 find "$@" -type f | xargs -n $RESTART_AFTER -- \
-  java -XX:MaxRAMPercentage=90.0 -jar "$JARFILE" | tee -a "$LOGFILE"
+  java -Xmx100G -jar "$JARFILE" | tee -a "$LOGFILE"
 
 echo "Done with all experiments!" >> "$LOGFILE"

build.sbt

@@ -45,7 +45,7 @@ lazy val root = (project in file("."))
 lazy val benchmark = (project in file("benchmark"))
   .settings(
     name := "catra-benchmark",
-    version := s"${version.value}-7", // Version scheme is CATRA version - benchmark version
+    version := s"${version.value}-9", // Version scheme is CATRA version - benchmark version
     assembly / mainClass := Some(
       "uuverifiers.RunBenchmarks"
     )