Merge branch 'main' into propose_vote_request

achamayou · Oct 3, 2023 · c9756e1 · c9756e1
2 parents 0d27c6c + d57d603
commit c9756e1
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 17 deletions.
diff --git a/.azure-pipelines-templates/trace_validation.yml b/.azure-pipelines-templates/trace_validation.yml
@@ -9,16 +9,16 @@ steps:
   - script: |
       set -x
       cd tla/
-      JSON=../build/replicate.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/election.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/multi_election.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/check_quorum.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/reconnect.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/reconnect_node.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/bad_network.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/fancy_election.1.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/fancy_election.2.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/suffix_collision.1.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/suffix_collision.2.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
-      JSON=../build/suffix_collision.3.ndjson java -Dtlc2.value.Values.width=1000 -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -Dtlc2.tool.impl.Tool.cdot=true -cp tla2tools.jar tlc2.TLC -lncheck final Traceccfraft.tla 2>&1
+      JSON=../build/replicate.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/election.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/multi_election.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/check_quorum.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/reconnect.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/reconnect_node.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/bad_network.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/fancy_election.1.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/fancy_election.2.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/suffix_collision.1.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/suffix_collision.2.ndjson ./tlc.sh Traceccfraft.tla 2>&1
+      JSON=../build/suffix_collision.3.ndjson ./tlc.sh Traceccfraft.tla 2>&1
     displayName: "Run trace validation"
diff --git a/.github/workflows/tlaplus.yml b/.github/workflows/tlaplus.yml
@@ -22,13 +22,13 @@ jobs:
         run: |
           set -exo pipefail
           cd tla/
-          java -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60 -coverage 60 -tool MCccfraft.tla 2>&1 | tee MCccfraft.out
+          ./tlc.sh -workers auto MCccfraft.tla 2>&1 | tee MCccfraft.out
 
       - name: MCccfraftWithReconfig.cfg
         run: |
           set -exo pipefail
           cd tla/
-          java -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60 -coverage 60 -tool -config MCccfraftWithReconfig.cfg MCccfraft.tla 2>&1 | tee MCccfraftWithReconfig.out
+          ./tlc.sh -workers auto -config MCccfraftWithReconfig.cfg MCccfraft.tla 2>&1 | tee MCccfraftWithReconfig.out
 
       - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
         uses: actions/upload-artifact@v2
@@ -49,7 +49,7 @@ jobs:
         run: |
           set -exo pipefail
           cd tla/
-          java -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601 -cp tla2tools.jar tlc2.TLC -workers auto -lncheck final -checkpoint 60 -coverage 60 -tool -simulate -depth 500 SIMccfraft.tla 2>&1 | tee SIMccfraft.out
+          ./tlc.sh -workers auto -simulate -depth 500 SIMccfraft.tla 2>&1 | tee SIMccfraft.out
 
       - name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
         uses: actions/upload-artifact@v2

diff --git a/js/ccf-app/package.json b/js/ccf-app/package.json
@@ -30,6 +30,6 @@
     "ts-node": "^10.4.0",
     "typedoc": "^0.25.0",
     "typescript": "^5.0.2",
-    "get-func-name": "2.0.0"
+    "get-func-name": "3.0.0"
   }
 }
diff --git a/tla/tlc.sh b/tla/tlc.sh
@@ -3,7 +3,14 @@
 # Licensed under the Apache 2.0 License.
 # Original License below
 # Adapted from: https://github.com/pmer/tla-bin
-exec java -cp tla2tools.jar:CommunityModules-deps.jar tlc2.TLC "$@" -workers auto
+
+TLC_OPTIONS=()
+
+if [ "${CI}" ] || [ "${SYSTEM_TEAMFOUNDATIONCOLLECTIONURI}" ]; then
+    JVM_OPTIONS=("-Dtlc2.TLC.ide=Github" "-Dutil.ExecutionStatisticsCollector.id=be29f6283abeed2fb1fd0be898bc6601")
+fi
+
+exec java -XX:+UseParallelGC -Dtlc2.tool.impl.Tool.cdot=true "${JVM_OPTIONS[@]}" -cp tla2tools.jar:CommunityModules-deps.jar tlc2.TLC "$@" -lncheck final "${TLC_OPTIONS[@]}"
 
 
 # Original License