Merge pull request #339 from amazon-mq/fix/cold-cache-remote-skip #208
This file contains hidden or 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: TLA+ Model Check | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| paths: | |
| - 'tla/**' | |
| - '.github/workflows/tla-model-check.yaml' | |
| schedule: | |
| - cron: '0 6 * * 1' # Every Monday at 06:00 UTC | |
| permissions: | |
| contents: read | |
| jobs: | |
| changes: | |
| runs-on: ubuntu-latest | |
| outputs: | |
| osiris: ${{ steps.filter.outputs.osiris }} | |
| manifest: ${{ steps.filter.outputs.manifest }} | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| fetch-depth: 0 | |
| - name: Detect changed paths | |
| id: filter | |
| run: | | |
| if [ "${{ github.event_name }}" = "pull_request" ]; then | |
| BASE=${{ github.event.pull_request.base.sha }} | |
| else | |
| BASE=${{ github.event.before }} | |
| fi | |
| # github.event.before can be the zero SHA (first push to a branch) or | |
| # a commit unreachable from history (e.g. a squash/rebase merge | |
| # rewrote main), which makes `git diff` fail. Fall back to treating | |
| # every path as changed so the affected jobs run instead of erroring out. | |
| if [ -z "$BASE" ] || [ "$BASE" = "0000000000000000000000000000000000000000" ] || ! git cat-file -e "$BASE^{commit}" 2>/dev/null; then | |
| CHANGED=$(git ls-tree -r --name-only HEAD) | |
| else | |
| CHANGED=$(git diff --name-only "$BASE" HEAD) | |
| fi | |
| echo "osiris=false" >> "$GITHUB_OUTPUT" | |
| echo "manifest=false" >> "$GITHUB_OUTPUT" | |
| echo "$CHANGED" | grep -q '^tla/osiris-replication/' && echo "osiris=true" >> "$GITHUB_OUTPUT" || true | |
| echo "$CHANGED" | grep -q '^tla/manifest-replication/' && echo "manifest=true" >> "$GITHUB_OUTPUT" || true | |
| echo "$CHANGED" | grep -q '^\.github/workflows/tla-model-check\.yaml' && { echo "osiris=true" >> "$GITHUB_OUTPUT"; echo "manifest=true" >> "$GITHUB_OUTPUT"; } || true | |
| osiris-replication: | |
| needs: changes | |
| if: needs.changes.outputs.osiris == 'true' || github.event_name == 'schedule' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: actions/setup-java@03ad4de0992f5dab5e18fcb136590ce7c4a0ac95 # v5.6.0 | |
| with: | |
| distribution: temurin | |
| java-version: '21' | |
| - name: Download tla2tools | |
| run: curl -fsSL -o tla2tools.jar https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar | |
| - name: Run TLC simulation (5 min) | |
| run: | | |
| cd tla/osiris-replication | |
| timeout 300 java -XX:+UseParallelGC -jar ../../tla2tools.jar -simulate -depth 500 -workers auto -deadlock MC.tla || [ $? -eq 124 ] | |
| manifest-replication: | |
| needs: changes | |
| if: needs.changes.outputs.manifest == 'true' || github.event_name == 'schedule' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - uses: actions/setup-java@03ad4de0992f5dab5e18fcb136590ce7c4a0ac95 # v5.6.0 | |
| with: | |
| distribution: temurin | |
| java-version: '21' | |
| - name: Download tla2tools | |
| run: curl -fsSL -o tla2tools.jar https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar | |
| - name: Run TLC simulation (2 min) | |
| run: | | |
| cd tla/manifest-replication | |
| timeout 120 java -XX:+UseParallelGC -jar ../../tla2tools.jar -simulate -depth 200 -workers auto ManifestReplicationMC -config ManifestReplication.cfg || [ $? -eq 124 ] |