TraceLink Implementation

.github/workflows/ci.yml

@@ -22,6 +22,8 @@ jobs:
     - uses: VirtusLab/scala-cli-setup@main
       with:
         jvm: ${{ matrix.java-version }}
+    - name: 'Setup TLA+ Tools'
+      run: scala-cli run . --main-class setup_sc
     - name: 'Run tests'
       run: scala-cli test . -- -l org.scalatest.tags.Slow
     - name: 'Upload Fuzz Test Results on Test Failure (in case there are some)'

distsys/trace/recorder.go

@@ -2,6 +2,7 @@ package trace
 
 import (
 	"encoding/json"
+	"fmt"
 	"os"
 	"sync"
 )
@@ -17,6 +18,10 @@ type localFileRecorder struct {
 }
 
 func MakeLocalFileRecorder(filename string) Recorder {
+	_, err := os.Stat(filename)
+	if err == nil {
+		panic(fmt.Sprintf("log file %s already exists", filename))
+	}
 	file, err := os.Create(filename)
 	if err != nil {
 		panic(err)

project.scala

@@ -1,23 +1,28 @@
 // Main
-//> using scala "2.13.15"
-//> using options "-deprecation"
+//> using scala 3.5.2
+//> using options -deprecation -Ximport-suggestion-timeout 0
+// note: disable import suggestions because this projects stackoverflows it every time (somehow)
+//       if this ever gets fixed, you can re-enable it. Try it on new compiler releases...
 
-//> using dependency "com.lihaoyi:::ammonite:3.0.0"
 //> using dependency "com.lihaoyi::os-lib:0.11.3"
-//> using dependency "com.lihaoyi::upickle:1.5.0"
-//> using dependency "io.github.java-diff-utils:java-diff-utils:4.12"
-//> using dependency "org.rogach::scallop:5.1.0"
+//> using dependency "com.lihaoyi::upickle:4.1.0"
+//> using dependency "io.github.java-diff-utils:java-diff-utils:4.15"
+//> using dependency "org.rogach::scallop:5.2.0"
 //> using dependency "org.scala-lang.modules::scala-parser-combinators:2.4.0"
-//> using dependency "org.scala-lang:scala-reflect:2.13.15"
 
 //> using exclude "systems/"
 
+// run setup.sc to populate
+//> using resourceDir .tools/
+
+// setup.sc
+//> using dep "com.lihaoyi::requests:0.9.0"
+
 // Test
 //> using testFramework org.scalatest.tools.Framework
 //> using test.dependency "com.github.daddykotex::courier:3.2.0"
 //> using test.dependency "com.lihaoyi::mainargs:0.7.6"
 //> using test.dependency "com.lihaoyi::pprint:0.9.0"
-//> using test.dependency "com.lihaoyi::upickle:4.0.2"
 //> using test.dependency "org.scalacheck::scalacheck:1.18.1"
 //> using test.dependency "org.scalatest::scalatest:3.2.19"
 

raftkvsgen.sc

@@ -0,0 +1,195 @@
+
+val aClientDefns = List(
+  "AClient.reqCh=mapping:client_reqCh",
+  "AClient.net=mapping:network",
+  "AClient.req=local:req",
+  "AClient.reqIdx=local:reqIdx",
+  "AClient.leader=local:leader0",
+  "AClient.resp=local:resp",
+  "AClient.respCh=mapping:client_respCh",
+)
+
+def withPrefix(prefix: String)(assigns: String*): Seq[String] =
+  assigns.map(assign => s"$prefix.$assign")
+
+val aServerDefns = withPrefix("AServer")(
+  "idx=local:idx",
+  "m=local:m",
+  "srvId=local:srvId",
+  "net=mapping:network",
+  "netLen=mapping:networkLen",
+  "state=global:state",
+  "currentTerm=global:currentTerm",
+  "votedFor=global:votedFor",
+  "votesResponded=global:votesResponded",
+  "votesGranted=global:votesGranted",
+  "leader=global:leader",
+  "leaderTimeout=global:leaderTimeout",
+  "commitIndex=global:commitIndex",
+  "nextIndex=global:nextIndex",
+  "matchIndex=global:matchIndex",
+  "log=global:log",
+  "plog=mapping:persistentLog",
+  "sm=global:sm",
+  "smDomain=global:smDomain",
+  "becomeLeaderCh=mapping:becomeLeaderCh",
+  "appendEntriesCh=mapping:appendEntriesCh",
+  "fd=mapping:fd",
+)
+
+val aServerRequestVoteDefns = withPrefix("AServerRequestVote")(
+  "idx=local:idx0",
+  "srvId=local:srvId0",
+  "net=mapping:network",
+  "netLen=mapping:networkLen",
+  "state=global:state",
+  "currentTerm=global:currentTerm",
+  "votedFor=global:votedFor",
+  "votesResponded=global:votesResponded",
+  "votesGranted=global:votesGranted",
+  "leader=global:leader",
+  "leaderTimeout=global:leaderTimeout",
+  "log=global:log",
+  "fd=mapping:fd",
+)
+
+val aServerAppendEntriesDefns = withPrefix("AServerAppendEntries")(
+  "idx=local:idx1",
+  "srvId=local:srvId1",
+  "net=mapping:network",
+  "netLen=mapping:networkLen",
+  "state=global:state",
+  "currentTerm=global:currentTerm",
+  "votedFor=global:votedFor",
+  "votesResponded=global:votesResponded",
+  "votesGranted=global:votesGranted",
+  "commitIndex=global:commitIndex",
+  "nextIndex=global:nextIndex",
+  "matchIndex=global:matchIndex",
+  "leader=global:leader",
+  "leaderTimeout=global:leaderTimeout",
+  "appendEntriesCh=mapping:appendEntriesCh",
+  "log=global:log",
+  "fd=mapping:fd",
+)
+
+val aServerAdvanceCommitIndex = withPrefix("AServerAdvanceCommitIndex")(
+  "newCommitIndex=local:newCommitIndex",
+  "srvId=local:srvId2",
+  "net=mapping:network",
+  "netLen=mapping:networkLen",
+  "state=global:state",
+  "currentTerm=global:currentTerm",
+  "votedFor=global:votedFor",
+  "votesResponded=global:votesResponded",
+  "votesGranted=global:votesGranted",
+  "leader=global:leader",
+  "commitIndex=global:commitIndex",
+  "nextIndex=global:nextIndex",
+  "matchIndex=global:matchIndex",
+  "sm=global:sm",
+  "smDomain=global:smDomain",
+  "leaderTimeout=global:leaderTimeout",
+  "log=global:log",
+  "plog=mapping:persistentLog",
+)
+
+val aServerBecomeLeader = withPrefix("AServerBecomeLeader")(
+  "srvId=local:srvId3",
+  "becomeLeaderCh=mapping:becomeLeaderCh",
+  "state=global:state",
+  "votedFor=global:votedFor",
+  "votesResponded=global:votesResponded",
+  "votesGranted=global:votesGranted",
+  "log=global:log",
+  "plog=mapping:persistentLog",
+  "commitIndex=global:commitIndex",
+  "nextIndex=global:nextIndex",
+  "matchIndex=global:matchIndex",
+  "leader=global:leader",
+  "currentTerm=global:currentTerm",
+  "appendEntriesCh=mapping:appendEntriesCh",
+  "becomeLeaderCh=mapping:becomeLeaderCh",
+)
+
+val aServerCrasher = withPrefix("AServerCrasher")(
+  "srvId=local:srvId4",
+)
+
+val proc =
+  os.proc(
+    "scala-cli",
+    "run",
+    ".",
+    "--",
+    "tracegen",
+    "-d", "tmp2/",
+    "--model-name", "raftkvs",
+    "--trace-files", os.list(os.pwd / "systems" / "raftkvs").filter(_.ext == "log"),
+    "--mpcal-variable-defns",
+    aClientDefns,
+    aServerDefns,
+    aServerRequestVoteDefns,
+    aServerAppendEntriesDefns,
+    aServerAdvanceCommitIndex,
+    aServerBecomeLeader,
+    aServerCrasher,
+    "--mpcal-state-vars",
+    "plog",
+    "becomeLeaderCh",
+    "respCh",
+    "requestVoteSrvId",
+    "appendEntriesSrvId",
+    "advanceCommitIndexSrvId",
+    "becomeLeaderSrvId",
+    "crasherSrvId",
+    "allReqs",
+    "timeout",
+    "fd",
+    "network",
+    "reqCh",
+    "appendEntriesCh",
+    "--mpcal-constant-defns",
+    "Debug=FALSE",
+    "ExploreFail=FALSE",
+    "BufferSize=100",
+    "MaxTerm=999999",
+    "MaxCommitIndex=999999",
+    "MaxNodeFail=99",
+    "LeaderTimeoutReset=100",
+    "NumServers=3",
+    "NumClients=1",
+    "--model-values",
+    "LogConcat",
+    "LogPop",
+    "NumRequests", // ignored apparently
+  )
+
+/* CONSTANT ExploreFail
+CONSTANT Debug
+
+CONSTANT NumServers
+CONSTANT NumClients
+
+CONSTANT BufferSize
+
+CONSTANT MaxTerm
+CONSTANT MaxCommitIndex
+
+CONSTANT MaxNodeFail
+
+CONSTANT LogConcat
+CONSTANT LogPop
+
+CONSTANT LeaderTimeoutReset
+
+\* This is only used for model checking / simulation
+CONSTANT NumRequests */
+
+println(proc.commandChunks.mkString(" "))
+
+val result = proc.call(cwd = os.pwd, check = false, mergeErrIntoOut = true)
+
+if result.exitCode == 0
+then println("generated ok")
+else result.out.lines().foreach(println)

setup.sc

@@ -0,0 +1,31 @@
+val toolsVersion = "1.8.0"
+val communityModulesVersion = "202409181925"
+val toolsDir = os.pwd / ".tools"
+val toolsPath = toolsDir / s"tla2tools-$toolsVersion.jar"
+val communityModulesPath = toolsDir / s"CommunityModules-deps.jar"
+
+if os.exists(toolsDir)
+then
+  os.list(toolsDir)
+    .filter(_.last.startsWith("tla2tools-"))
+    .filter(_ != toolsPath)
+    .foreach(os.remove)
+
+  os.list(toolsDir)
+    .filter(_.last.startsWith("CommunityModules-"))
+    .filter(_ != communityModulesPath)
+    .foreach(os.remove)
+
+if !os.exists(toolsPath)
+then
+  val result = requests.get(
+    s"https://github.com/tlaplus/tlaplus/releases/download/v$toolsVersion/tla2tools.jar"
+  )
+  os.write(toolsPath, result.bytes, createFolders = true)
+
+if !os.exists(communityModulesPath)
+then
+  val result = requests.get(
+    "https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar"
+  )
+  os.write(communityModulesPath, result.bytes, createFolders = true)