Skip to content

docs: clarify nondeterministic action parameters and quantifiers #180

docs: clarify nondeterministic action parameters and quantifiers

docs: clarify nondeterministic action parameters and quantifiers #180

Workflow file for this run

name: CI
on:
push:
branches: [main]
pull_request:
jobs:
check:
runs-on: ubuntu-latest
defaults:
run:
working-directory: specl
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
with:
workspaces: specl
- run: cargo fmt --check
- run: cargo clippy --workspace -- -D warnings -A clippy::too_many_arguments
- run: cargo test --workspace --exclude specl-tla
- run: cargo test -p specl-tla --test translate_corpus -- --skip benchmark_tla_files_translate
- name: Lint showcase examples
run: |
for f in examples/showcase/*.specl; do
cargo run -q --bin specl -- fmt "$f" --lint || exit 1
done
soundness:
runs-on: ubuntu-latest
if: github.event_name == 'push' && github.ref == 'refs/heads/main'
defaults:
run:
working-directory: specl
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
with:
workspaces: specl
- name: Proptest soundness (512 cases)
run: PROPTEST_CASES=512 cargo test -p specl-soundness -- --test-threads=1
timeout-minutes: 60