Finitizing monotonic systems (#97) #231
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Check Specs & Metadata | |
| on: | |
| push: | |
| branches: | |
| - master | |
| pull_request: | |
| branches: | |
| - master | |
| repository_dispatch: | |
| types: [tlaplus-dispatch] | |
| jobs: | |
| validate: | |
| name: Validate Manifest, Specs, & Models | |
| runs-on: ${{ matrix.os }} | |
| strategy: | |
| matrix: | |
| include: | |
| - { os: windows-latest } | |
| - { os: ubuntu-latest } | |
| - { os: macos-latest } | |
| fail-fast: false | |
| env: | |
| SCRIPT_DIR: .github/scripts | |
| TLAPS_VERSION: 202210041448 | |
| defaults: | |
| run: | |
| shell: bash | |
| steps: | |
| - name: Clone repo | |
| uses: actions/checkout@v3 | |
| - name: Install python | |
| uses: actions/setup-python@v4 | |
| with: | |
| python-version: '3.11' | |
| - name: Install Java | |
| uses: actions/setup-java@v3 | |
| with: | |
| distribution: adopt | |
| java-version: 17 | |
| - name: Download TLA⁺ dependencies | |
| if: matrix.os == 'windows-latest' | |
| run: | | |
| # Print out tool version information | |
| java --version | |
| python --version | |
| pip --version | |
| # Install python packages | |
| pip install -r $SCRIPT_DIR/requirements.txt | |
| # Put all dependencies in their own directory to ensure they aren't included implicitly | |
| mkdir deps | |
| # Get tree-sitter-tlaplus | |
| curl -LO https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.zip | |
| 7z x main.zip | |
| rm main.zip | |
| mv tree-sitter-tlaplus-main deps/tree-sitter-tlaplus | |
| # Get TLA⁺ tools | |
| mkdir deps/tools | |
| curl -LO http://nightly.tlapl.us/dist/tla2tools.jar | |
| mv tla2tools.jar deps/tools/tla2tools.jar | |
| # Get TLA⁺ community modules | |
| mkdir deps/community | |
| curl -LO https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar | |
| mv CommunityModules-deps.jar deps/community/modules.jar | |
| # Get TLAPS modules | |
| curl -LO https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.zip | |
| 7z x $TLAPS_VERSION.zip | |
| rm $TLAPS_VERSION.zip | |
| mv tlapm-$TLAPS_VERSION deps/tlapm | |
| - name: Download TLA⁺ dependencies | |
| if: matrix.os != 'windows-latest' | |
| run: | | |
| # Print out tool version information | |
| java --version | |
| python --version | |
| pip --version | |
| cc --version | |
| cpp --version | |
| # Install python packages | |
| pip install -r $SCRIPT_DIR/requirements.txt | |
| # Put all dependencies in their own directory to ensure they aren't included implicitly | |
| mkdir deps | |
| # Get tree-sitter-tlaplus | |
| wget -nv https://github.com/tlaplus-community/tree-sitter-tlaplus/archive/main.tar.gz | |
| tar -xf main.tar.gz | |
| rm main.tar.gz | |
| mv tree-sitter-tlaplus-main deps/tree-sitter-tlaplus | |
| # Get TLA⁺ tools | |
| mkdir deps/tools | |
| wget -nv http://nightly.tlapl.us/dist/tla2tools.jar -O deps/tools/tla2tools.jar | |
| # Get TLA⁺ community modules | |
| mkdir deps/community | |
| wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \ | |
| -O deps/community/modules.jar | |
| # Get TLAPS modules | |
| wget -nv https://github.com/tlaplus/tlapm/archive/refs/tags/$TLAPS_VERSION.tar.gz | |
| tar -xf $TLAPS_VERSION.tar.gz | |
| rm $TLAPS_VERSION.tar.gz | |
| mv tlapm-$TLAPS_VERSION deps/tlapm | |
| # Install TLAPS | |
| if [[ "${{ runner.os }}" == "Linux" ]]; then | |
| TLAPM_BIN_TYPE=x86_64-linux-gnu | |
| elif [[ "${{ runner.os }}" == "macOS" ]]; then | |
| TLAPM_BIN_TYPE=i386-darwin | |
| else | |
| echo "Unknown OS" | |
| exit 1 | |
| fi | |
| TLAPM_BIN="tlaps-1.5.0-$TLAPM_BIN_TYPE-inst.bin" | |
| wget -nv https://github.com/tlaplus/tlapm/releases/download/$TLAPS_VERSION/$TLAPM_BIN | |
| chmod +x $TLAPM_BIN | |
| # Workaround for https://github.com/tlaplus/tlapm/issues/88 | |
| set +e | |
| for ((attempt = 1; attempt <= 5; attempt++)); do | |
| rm -rf deps/tlapm-install | |
| ./$TLAPM_BIN -d deps/tlapm-install | |
| if [ $? -eq 0 ]; then | |
| exit 0 | |
| fi | |
| done | |
| exit 1 | |
| - name: Check manifest.json format | |
| run: | | |
| python $SCRIPT_DIR/check_manifest_schema.py \ | |
| --manifest_path manifest.json \ | |
| --schema_path manifest-schema.json | |
| - name: Check manifest files | |
| run: | | |
| python $SCRIPT_DIR/check_manifest_files.py \ | |
| --manifest_path manifest.json \ | |
| --ci_ignore_path .ciignore | |
| - name: Check manifest feature flags | |
| run: | | |
| python $SCRIPT_DIR/check_manifest_features.py \ | |
| --manifest_path manifest.json \ | |
| --ts_path deps/tree-sitter-tlaplus | |
| - name: Parse all modules | |
| run: | | |
| python $SCRIPT_DIR/parse_modules.py \ | |
| --tools_jar_path deps/tools/tla2tools.jar \ | |
| --tlapm_lib_path deps/tlapm/library \ | |
| --community_modules_jar_path deps/community/modules.jar \ | |
| --manifest_path manifest.json | |
| - name: Check small models | |
| run: | | |
| python $SCRIPT_DIR/check_small_models.py \ | |
| --tools_jar_path deps/tools/tla2tools.jar \ | |
| --tlapm_lib_path deps/tlapm/library \ | |
| --community_modules_jar_path deps/community/modules.jar \ | |
| --manifest_path manifest.json | |
| - name: Smoke-test large models | |
| run: | | |
| # SimKnuthYao requires certain number of states to have been generated | |
| # before termination or else it fails. This makes it not amenable to | |
| # smoke testing. | |
| SKIP=("specifications/KnuthYao/SimKnuthYao.cfg") | |
| # SimTokenRing does not work on Windows systems. | |
| if [[ "${{ runner.os }}" == "Windows" ]]; then | |
| SKIP+=("specifications/ewd426/SimTokenRing.cfg") | |
| fi | |
| python $SCRIPT_DIR/smoke_test_large_models.py \ | |
| --tools_jar_path deps/tools/tla2tools.jar \ | |
| --tlapm_lib_path deps/tlapm/library \ | |
| --community_modules_jar_path deps/community/modules.jar \ | |
| --manifest_path manifest.json \ | |
| --skip "${SKIP[@]}" | |
| - name: Check proofs | |
| if: matrix.os != 'windows-latest' | |
| run: | | |
| SKIP=( | |
| # Failing; see https://github.com/tlaplus/Examples/issues/67 | |
| specifications/Bakery-Boulangerie/Bakery.tla | |
| specifications/Bakery-Boulangerie/Boulanger.tla | |
| specifications/Paxos/Consensus.tla | |
| specifications/PaxosHowToWinATuringAward/Consensus.tla | |
| specifications/lamport_mutex/LamportMutex_proofs.tla | |
| specifications/ewd998/EWD998_proof.tla | |
| # Long-running; see https://github.com/tlaplus/tlapm/issues/85 | |
| specifications/LoopInvariance/Quicksort.tla | |
| specifications/LoopInvariance/SumSequence.tla | |
| specifications/bcastByz/bcastByz.tla | |
| specifications/MisraReachability/ReachabilityProofs.tla | |
| ) | |
| python $SCRIPT_DIR/check_proofs.py \ | |
| --tlapm_path deps/tlapm-install \ | |
| --manifest_path manifest.json \ | |
| --skip "${SKIP[@]}" | |
| - name: Smoke-test manifest generation script | |
| run: | | |
| rm -r deps/tree-sitter-tlaplus/build | |
| python $SCRIPT_DIR/generate_manifest.py \ | |
| --manifest_path manifest.json \ | |
| --ci_ignore_path .ciignore \ | |
| --ts_path deps/tree-sitter-tlaplus | |
| git diff -a | |