GitHub Actions

A workflow

Save this as .github/workflows/p-model.yml, with working-directory set to the folder that has your .pproj file (or your .p files):

name: P model

on:
  pull_request:
  push:
    branches: [main]

permissions:
  contents: read

jobs:
  check:
    runs-on: ubuntu-latest
    timeout-minutes: 15
    defaults:
      run:
        working-directory: model
    steps:
      - uses: actions/checkout@v7

      - name: Install snappea
        run: curl -fsSL https://raw.githubusercontent.com/crowecawcaw/snappea/main/scripts/install.sh | sh -s -- --version 0.1.0

      - name: Check the model
        run: snappea check --timeout 2m

      - uses: actions/upload-artifact@v7
        if: failure()
        with:
          name: snappea-output
          path: model/PCheckerOutput

• Install. The install script downloads the release, checks its checksum, and adds snappea to the PATH of later steps. Pin a version so a new release can't change your results without a commit; leave out -s -- --version ... for the latest.
• Check. snappea check with no arguments finds the sources and checks every test case. The job fails on exit status 1 (a bug) or 2 (an error, such as a type error).
• Output. On a failure, the artifact has the failing schedule's log (bug.txt) and a bug.schedule file. Download it from the run page and run snappea replay bug.schedule locally to step through the same bug.

This repository runs the same workflow on its example model: check-model.yml, linked from examples/model/github-workflow.yml.

How long to explore

Search strategies are selected automatically. The default is ten seconds per test; choose a larger timeout for CI when needed. Exhaustive completion ends a check early:

The checker uses every CPU core by default. A slower nightly job with a larger budget (on: schedule) is a good complement to a quick check on each pull request.

Test cases that should fail

A model often keeps a test case for a design you rejected, to show why. Name the test cases that should pass (globs work: snappea check 'tcSafe*'), or check that the rejected one still finds its bug, so it keeps proving the point:

      - name: The check-then-reserve design oversells
        run: |
          status=0
          snappea check tcCheckThenReserve || status=$?
          test "$status" -eq 1

Many test cases

To spread a large model over several runners, list the test cases with snappea tests and check one per job:

jobs:
  list:
    runs-on: ubuntu-latest
    outputs:
      tests: ${{ steps.list.outputs.tests }}
    steps:
      - uses: actions/checkout@v7
      - run: curl -fsSL https://raw.githubusercontent.com/crowecawcaw/snappea/main/scripts/install.sh | sh -s -- --version 0.1.0
      - id: list
        working-directory: model
        run: echo "tests=$(snappea tests | jq -R . | jq -sc .)" >> "$GITHUB_OUTPUT"

  check:
    needs: list
    strategy:
      fail-fast: false
      matrix:
        test: ${{ fromJSON(needs.list.outputs.tests) }}
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - run: curl -fsSL https://raw.githubusercontent.com/crowecawcaw/snappea/main/scripts/install.sh | sh -s -- --version 0.1.0
      - working-directory: model
        run: snappea check "${{ matrix.test }}" --timeout 5m

macOS and Windows runners

The script works on macos-latest and, in a bash step, on windows-latest. For a PowerShell step on Windows:

      - name: Install snappea
        shell: pwsh
        env:
          SNAPPEA_VERSION: 0.1.0
        run: irm https://raw.githubusercontent.com/crowecawcaw/snappea/main/scripts/install.ps1 | iex

Specs in your language's tests

The language helpers check P specs inside your ordinary unit tests and bring the checker with them, so CI needs no install step: see Python, Rust, Go and Java. Run pytest, go test, cargo test or your Maven or Gradle build as usual.