main.yml

name: Regression tests
on: [push, pull_request]

jobs:
  build:
    runs-on: ubuntu-latest
    steps:

    - uses: actions/checkout@v2
      with:
        # Number of commits to fetch. 0 indicates all history.
        fetch-depth: '0'
        
    - name: Set up JDK 11
      uses: actions/setup-java@v1
      with:
        java-version: 11.0.3

      ##
      ## Fetch tla2tools.
      ##
    - name: Fetch TLC
      run: |
        mkdir tools
        wget https://nightly.tlapl.us/dist/tla2tools.jar --output-document=tools/tla2tools.jar

      ##
      ## Fetch CommunityModules.
      ##
    - name: Fetch CommunityModules
      run: |
        wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output-document=tools/CommunityModules-deps.jar

      ##
      ## Run TLA+ regression tests.
      ##
    - name: Run regression tests
      run: |
        cd .github/
        java -jar ../tools/tla2tools.jar -config Regressions.tla Regressions.tla