experiments.sc

def recordResults(
    tracesFolder: os.Path,
    spec: os.Path,
    cfgFile: os.Path,
    dfs: Boolean,
    progressInv: Boolean
): Unit =
  val specName = spec.last.stripSuffix(".tla")
  var specIdent = specName
  if dfs then specIdent += "_dfs"
  if !progressInv then specIdent += "_noprogressinv"

  // Check the existence of files from replica 2 or 3, since in principle
  // the common usage will be to run without replicas. Otherwise,
  // a kick-the-tires run will start filling in data that we do have
  // but not from replica 1.
  val altCheckFiles = List(
    tracesFolder / s"2_${specIdent}_check.txt",
    tracesFolder / s"3_${specIdent}_check.txt",
  )
  // Note: if you actually want to use replicas, remove this check
  // (replace the list with Nil or something), then write
  // `specIdent = s"2_$specIdent"` for replica 2, or similar for 3.
  // Then, you get filenames that won't clash between replicas and you
  // can manually scp them over. The analysis scripts understand these
  // prefixes.

  val checkOutFile = tracesFolder / s"${specIdent}_check.txt"

  // This one result was actually lost on all replicas. Comment this out
  // if you're re-running from scratch and you want to evaluate it.
  if checkOutFile == os.Path("systems/raftkvs/traces_found_5/6434682755345117408/raftkvs_dfs_check.txt", os.pwd)
  then
    println(s"avoiding originally missing file $checkOutFile")
    return

  if os.exists(checkOutFile) || altCheckFiles.exists(os.exists)
  then println(s"skipping $checkOutFile")
  else
    println(s"processing $spec in $tracesFolder ($cfgFile)")
    val genProc = os.proc(
      "time",
      os.pwd / "pgo.jar",
      "tracegen",
      if dfs then "--noall-paths" else "--all-paths",
      if progressInv then "--progress-inv" else "--noprogress-inv",
      "--cfg-file",
      cfgFile,
      spec,
      tracesFolder
    )
    val genOutFile = tracesFolder / s"${specIdent}_gen.txt"
    println(
      s"$$ ${genProc.commandChunks.mkString(" ")}; streaming to $genOutFile"
    )
    genProc.call(
      cwd = os.pwd,
      mergeErrIntoOut = true,
      stdout = os.PathRedirect(genOutFile),
      check = true
    )

    val checkProc = os.proc(
      "time",
      os.pwd / "pgo.jar",
      "tlc",
      if dfs then Some("--dfs") else None,
      "--",
      tracesFolder / s"${specName}Validate.tla",
      "-checkpoint",
      "0"
    )
    println(
      s"$$ ${checkProc.commandChunks.mkString(" ")}; streaming to $checkOutFile"
    )
    val checkResult = checkProc.call(
      cwd = os.pwd,
      mergeErrIntoOut = true,
      stdout = os.PathRedirect(checkOutFile),
      check = false
    )
    println(if checkResult.exitCode == 0 then "...ok" else "...error")

def processCollection(
    metaFolder: os.Path,
    spec: os.Path,
    cfgFile: os.Path,
    dfs: Boolean,
    progressInv: Boolean
): Unit =
  os.list(metaFolder)
    .filter(os.isDir)
    .foreach(
      recordResults(_, spec, cfgFile, dfs = dfs, progressInv = progressInv)
    )

// --- instantiations go here

// dqueue
for
  metaFolderName <- List("traces_found", "traces_found_bad_vclocks")
  dfs <- List(true, false)
  progressInv <- List(true, false)
  spec <- List(os.sub / "dqueue.tla")
do
  val root = os.pwd / "systems" / "dqueue"
  processCollection(
    metaFolder = root / metaFolderName,
    spec = root / spec,
    cfgFile = root / "dqueueValidate.cfg",
    dfs = dfs,
    progressInv = progressInv
  )
end for

// locksvc
for
  metaFolderName <- List("traces_found", "traces_found_bad_vclocks")
  dfs <- List(true, false)
  progressInv <- List(true, false)
  spec <- List(os.sub / "locksvc.tla", os.sub / "badspecs" / "locksvc_tcp.tla")
do
  val root = os.pwd / "systems" / "locksvc"
  processCollection(
    metaFolder = root / metaFolderName,
    spec = root / spec,
    cfgFile = root / "locksvcValidate.cfg",
    dfs = dfs,
    progressInv = progressInv
  )
end for

extension (lhs: Boolean)
  def ==>(rhs: => Boolean): Boolean =
    if lhs then rhs else true

// raftkvs
for
  (metaFolderName, cfgFile) <- List(
    ("traces_found_1", os.sub / "raftkvsValidate1.cfg"),
    ("traces_found_2", os.sub / "raftkvsValidate2.cfg"),
    ("traces_found_3", os.sub / "raftkvsValidate3.cfg"),
    ("traces_found_4", os.sub / "raftkvsValidate4.cfg"),
    ("traces_found_5", os.sub / "raftkvsValidate5.cfg"),
    ("traces_found_3_fail", os.sub / "raftkvsValidate3.cfg"),
    ("traces_found_3_netLen", os.sub / "raftkvsValidate3.cfg"),
    ("traces_found_3_bad_vclocks", os.sub / "raftkvsValidate3.cfg")
  )
  progressInv <- List(true, false)
  root = os.pwd / "systems" / "raftkvs"
  spec <- List(root / "raftkvs.tla") ++ os.list(root / "badspecs")
  if (metaFolderName == "traces_found_3_bad_vclocks") ==> ((spec / os.up).last != "badspecs")
do
  processCollection(
    metaFolder = root / metaFolderName,
    spec = spec,
    cfgFile = root / cfgFile,
    dfs = true,
    progressInv = progressInv
  )
end for