Skip to content

Commit

Permalink
Merge branch 'propose_vote_request' of https://github.com/achamayou/CCF…
Browse files Browse the repository at this point in the history 
… into propose_vote_request
  • Loading branch information
@achamayou
achamayou committed Oct 2, 2023
2 parents a957986 + cc4d806 commit 286a7fb
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 25 deletions.
24 changes: 12 additions & 12 deletions .azure-pipelines-templates/trace_validation.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,16 +9,16 @@ steps:
- script: |
set -x
cd tla/
JSON=../build/replicate.ndjson java -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 -XX:+UseParallelGC -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 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
displayName: "Run trace validation"
6 changes: 3 additions & 3 deletions .github/workflows/tlaplus.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,13 +22,13 @@ jobs:
run: |
set -exo pipefail
cd tla/
java -XX:+UseParallelGC -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
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
- name: MCccfraftWithReconfig.cfg
run: |
set -exo pipefail
cd tla/
java -XX:+UseParallelGC -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
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
- name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
uses: actions/upload-artifact@v2
Expand All @@ -49,7 +49,7 @@ jobs:
run: |
set -exo pipefail
cd tla/
java -XX:+UseParallelGC -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
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
- name: Upload TLC's out file as an artifact. Can be imported into the TLA+ Toolbox.
uses: actions/upload-artifact@v2
Expand Down
10 changes: 1 addition & 9 deletions tla/install_deps.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,20 +85,12 @@ def _parse_args() -> argparse.Namespace:

def install_tlc():

java = "java -XX:+UseParallelGC"
java = "java"
tlaplus_path = "~/.vscode-remote/extensions/alygin.vscode-tlaplus-nightly-*/tools/tla2tools.jar"
tlcmax_args = "-Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet -Dtlc2.tool.ModelChecker.BAQueue=true"
copy_tlaplus = f"-cp {tlaplus_path} tlc2.TLC"

def get_run_tlc_max(size: int) -> str:
return f"{java} -XX:MaxDirectMemorySize={size}g {tlcmax_args} {copy_tlaplus}"

set_alias("tlcrepl", f"{java} -cp {tlaplus_path} tlc2.REPL")
set_alias("tlc", f"{java} {copy_tlaplus}")
set_alias("tlcmax4", get_run_tlc_max(4))
set_alias("tlcmax8", get_run_tlc_max(8))
set_alias("tlcmax16", get_run_tlc_max(16))
set_alias("tlcmax32", get_run_tlc_max(32))


def install_deps(args: argparse.Namespace):
Expand Down
2 changes: 1 addition & 1 deletion tla/tlc.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
# Licensed under the Apache 2.0 License.
# Original License below
# Adapted from: https://github.com/pmer/tla-bin
exec java -XX:+IgnoreUnrecognizedVMOptions -XX:+UseParallelGC -Xms2G -Xmx2G -cp tla2tools.jar:CommunityModules-deps.jar tlc2.TLC "$@" -workers auto
exec java -cp tla2tools.jar:CommunityModules-deps.jar tlc2.TLC "$@" -workers auto


# Original License
Expand Down

0 comments on commit 286a7fb

Please sign in to comment.