[tracelink] add missing "no critical sections" patch

src/pgo/PGo.scala

@@ -67,6 +67,8 @@ object PGo {
             s"missing or incorrect prefix for $str",
           )
 
+  final case class ConfigExit(code: Int) extends RuntimeException
+
   class Config(arguments: Seq[String]) extends ScallopConf(arguments) {
     banner("PGo compiler")
 
@@ -282,6 +284,13 @@ object PGo {
         descr = "directory containing log files to use",
         default = Some(destDir()),
       )
+      validate(logsDir): logsDir =>
+        if os.list(logsDir).filter(_.last.endsWith(".log")).isEmpty
+        then
+          Left(
+            s"$logsDir has no .log files - you need to pass a folder formatted as if harvest-traces generated it",
+          )
+        else Right(())
       val cfgFragmentSuffix = opt[String](
         descr =
           "suffix to add to {model_name}Validate{suffix}.cfg, when looking for a manual config file",
@@ -438,7 +447,7 @@ object PGo {
         println(s"$printedName: $line")
       }
       printHelp()
-      sys.exit(1)
+      throw ConfigExit(1)
     }
 
     verify()
@@ -560,7 +569,10 @@ object PGo {
 
   def main(args: Array[String]): Unit = {
     val startTime = System.currentTimeMillis()
-    val errors = run(ArraySeq.unsafeWrapArray(args))
+    val errors = try
+        run(ArraySeq.unsafeWrapArray(args))
+      catch case ConfigExit(code) =>
+        sys.exit(code)
     val endTime = System.currentTimeMillis()
     val duration = Duration(length = endTime - startTime, unit = MILLISECONDS)
     if (errors.nonEmpty) {

src/pgo/tracing/HarvestTraces.scala

@@ -50,7 +50,7 @@ object HarvestTraces:
 
     val workspaceRoot = System.getenv("MILL_WORKSPACE_ROOT") match
       case null => os.pwd
-      case path => path
+      case path => os.Path(path, os.pwd)
 
     // Add a go.work that resolves the library module relative to the dev checkout
     if os.exists(tmpDir / "go.mod")
@@ -59,7 +59,7 @@ object HarvestTraces:
         tmpDir / "go.work",
         s"""go 1.24.0
            |
-           |use ${os.pwd / "distsys"}
+           |use ${workspaceRoot / "distsys"}
            |use $tmpDir
            |""".stripMargin,
       )

src/pgo/tracing/JSONToTLA.scala

@@ -471,9 +471,13 @@ final class JSONToTLA private (
                |  /\\ __clock = <<>>
                |  /\\ __action = <<>>
                |
-               |__Next_self(self, __commit(_, _)) ==${allValidateLabels
-                .map(name => s"\n  \\/ $name(self, __commit)")
-                .mkString}
+               |__Next_self(self, __commit(_, _)) ==${
+                if allValidateLabels.size == 0 then "FALSE"
+                else
+                  allValidateLabels
+                    .map(name => s"\n  \\/ $name(self, __commit)")
+                    .mkString
+              }
                |
                |__Next ==
                |  \\E self \\in __self_values :

test/pgo/CLITests.scala

@@ -0,0 +1,22 @@
+package pgo
+
+class CLITests extends munit.FunSuite:
+  val dqueueTLA = pgo.projectRoot / "systems" / "dqueue" / "dqueue.tla"
+  test("tracegen with no log files in dir: errors returned"):
+    val tmp = os.temp.dir()
+    try
+      val Nil = pgo.PGo.run(scala.collection.immutable.ArraySeq(
+        "tracegen", dqueueTLA.toString, tmp.toString
+      ))
+      fail("didn't exit with config error")
+    catch
+      case PGo.ConfigExit(1) => () // intended
+
+  test("tracegen with one empty log file: no errors"):
+    val tmp = os.temp.dir()
+    os.write(tmp / "foo.log", "")
+    assertEquals(pgo.PGo.run(scala.collection.immutable.ArraySeq(
+      "tracegen", dqueueTLA.toString, tmp.toString
+    )), Nil)
+end CLITests
+

test/pgo/TracingTests.scala

@@ -1,7 +1,6 @@
 package pgo
 
 import pgo.util.TLC
-import os.makeDir.all
 import scala.concurrent.duration.{MINUTES, Duration}
 
 class TracingTests extends munit.FunSuite: