Skip to content

docs: update CSP usage in formal full run #1897

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ootakazuhiko wants to merge 2 commits into
base: main
Choose a base branch
from
Open

docs: update CSP usage in formal full run #1897

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d5c7925
docs: update CSP backends in formal full-run
ootakazuhiko Feb 3, 2026
e08fe6d
docs: clarify CSP CI status and backends
ootakazuhiko Feb 3, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 20 additions & 8 deletions docs/quality/formal-full-run.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@

This guide shows how to run **all formal verification tools** end-to-end for a smoke test.

### Recommended: CI (covers Apalache / SMT / Alloy / TLA / Kani / SPIN / Lean; CSP is stub)
### Recommended: CI (covers Apalache / SMT / Alloy / TLA / Kani / SPIN / Lean; CSP is non-blocking unless a backend is available)

1) **Label-gated (PR)**
- Add label `run-formal` to the PR.
Expand Down Expand Up @@ -43,7 +43,7 @@ Pre-reqs:
- Optional: Alloy jar, Apalache, Kani
- Optional: SPIN (`spin` + `gcc`)
- Optional: Lean4 (`elan` + `lake`)
- Optional: CSP tool (configure via `CSP_RUN_CMD`)
- Optional: CSP tool (`refines` or `cspmchecker`, or configure via `CSP_RUN_CMD`)

#### 1) Base run (conformance + alloy + TLA + SMT + Apalache + Kani + SPIN + CSP + Lean + aggregate)
```bash
Expand Down Expand Up @@ -94,8 +94,14 @@ pnpm run verify:lean

#### 8) Run CSP (when configured)
```bash
# {file} will be replaced with the absolute file path
CSP_RUN_CMD='echo Running CSP tool on {file}' pnpm run verify:csp -- --file spec/csp/sample.cspm
# Typecheck (safe default):
pnpm run verify:csp -- --file spec/csp/sample.cspm --mode typecheck

# Assertions (requires FDR `refines`):
pnpm run verify:csp -- --file spec/csp/sample.cspm --mode assertions

# Or, run via custom backend command (shell). {file} is replaced with the absolute file path:
CSP_RUN_CMD='echo Running CSP tool on {file}' pnpm run verify:csp -- --file spec/csp/sample.cspm --mode typecheck
```

#### 9) Model check (TLC/Alloy scan)
Expand All @@ -114,7 +120,7 @@ Outputs:

この手順は、**すべての形式検査ツールをまとめて動作確認**するためのスモークテストです。

### 推奨: CI（Apalache / SMT / Alloy / TLA / Kani / SPIN / Lean をまとめて実行。CSP は stub）
### 推奨: CI（Apalache / SMT / Alloy / TLA / Kani / SPIN / Lean をまとめて実行。CSP はバックエンドが無い場合は non-blocking）

1) **PRラベル実行**
- PR に `run-formal` ラベルを付与
Expand Down Expand Up @@ -149,7 +155,7 @@ Outputs:
- 任意: Alloy jar / Apalache / Kani
- 任意: SPIN（`spin` + `gcc`）
- 任意: Lean4（`elan` + `lake`）
- 任意: CSP ツール（`CSP_RUN_CMD` で設定）
- 任意: CSP ツール（`refines` / `cspmchecker` または `CSP_RUN_CMD` で設定）

#### 1) ベース実行（conformance + alloy + TLA + SMT + Apalache + Kani + SPIN + CSP + Lean + 集約）
```bash
Expand Down Expand Up @@ -200,8 +206,14 @@ pnpm run verify:lean

#### 8) CSP を実行（設定済みの場合）
```bash
# {file} は絶対パスへ置換されます
CSP_RUN_CMD='echo Running CSP tool on {file}' pnpm run verify:csp -- --file spec/csp/sample.cspm
# Typecheck（安全な既定）:
pnpm run verify:csp -- --file spec/csp/sample.cspm --mode typecheck

# Assertions（FDR `refines` が必要）:
pnpm run verify:csp -- --file spec/csp/sample.cspm --mode assertions

# 任意のバックエンドをコマンドで実行（シェル経由）。{file} は絶対パスへ置換されます:
CSP_RUN_CMD='echo Running CSP tool on {file}' pnpm run verify:csp -- --file spec/csp/sample.cspm --mode typecheck
```

#### 9) モデル検査（TLC/Alloy スキャン）
Expand Down
12 changes: 8 additions & 4 deletions spec/csp/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,10 @@ This directory contains CSP / CSPM-style specifications for concurrency/protocol

## Current status

- CI integration is provided as a **non-blocking stub** until a concrete toolchain is selected.
- To execute CSP checks, set `CSP_RUN_CMD` (see below) or install a supported tool.
- CI integration is wired as **non-blocking**.
- On GitHub-hosted runners it will typically report `tool_not_available` unless a CSP backend is available.
- For CI execution, consider a self-hosted runner (with `refines`/`cspmchecker`) or a trusted `CSP_RUN_CMD` setup.
- To execute CSP checks locally, set `CSP_RUN_CMD` (see below) or install a supported tool.

## Toolchain options (local)

Expand Down Expand Up @@ -71,8 +73,10 @@ Artifacts:

### 現状

- CI 統合は **non-blocking stub** として提供します（ツールチェーン未確定のため）。
- 実際に CSP ツールを実行する場合は `CSP_RUN_CMD` を設定してください。
- CI 統合は **non-blocking** です。
- GitHub-hosted runner では CSP バックエンドが無い限り `tool_not_available` になります。
- CI で実行したい場合は self-hosted runner（`refines`/`cspmchecker`）または信頼できる `CSP_RUN_CMD` の運用を検討してください。
- 実際に CSP ツールを実行する場合は `CSP_RUN_CMD` を設定するか、対応ツール（`refines`/`cspmchecker`）を導入してください。

### ローカル実行（例）

Expand Down
Loading