diff --git a/.gitignore b/.gitignore index fe45ba58b..c9418ff7a 100644 --- a/.gitignore +++ b/.gitignore @@ -41,3 +41,7 @@ prism/\.settings/ prism/etc/jars/.gradle/ prism/etc/jars/build/ prism/etc/jars/local-libs/ + +# Claude Code local worktrees +.claude/worktrees/ +prism/.claude/worktrees/ diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 000000000..db05a5744 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1 @@ +@prism/CLAUDE.md diff --git a/prism/.claude/skills/prism-add-test/SKILL.md b/prism/.claude/skills/prism-add-test/SKILL.md new file mode 100644 index 000000000..a2acd50ab --- /dev/null +++ b/prism/.claude/skills/prism-add-test/SKILL.md @@ -0,0 +1,200 @@ +--- +name: prism-add-test +description: > + Add a PRISM regression test. Use this skill whenever the user wants to add, + create, or write a regression test (or "test case") for the PRISM model + checker — including after fixing a bug, verifying new behaviour, or exploring + a boundary condition. Triggers on phrases like "add this test", "write a + regression test", "add a test case", "capture this as a test", "put this in + prism-tests", or any request to create test files for a PRISM model/property + combination. +--- + +# Adding a PRISM Regression Test + +A test is three files: a model `.prism` (or historic aliases `.nm`/`.pm`/`.sm`), a properties file +`.prism.props`, and an optional engine-arguments file `.prism.props.args`. The test runner +(`prism-auto`) pairs them by name and runs each line in the `.args` file as a +separate PRISM invocation, checking that every `// RESULT:` comment in the +`.props` file matches actual output. + +--- + +## Step 1 — Identify what's being tested + +Clarify (or infer from context): +- **Model type**: DTMC, CTMC, MDP, PTA, POMDP, … +- **Property type**: reachability probability, expected reward, steady-state, LTL, … +- **Purpose**: new feature, bug fix, boundary/edge case, LP engine, … +- **Engines to cover**: explicit (`-ex`), sparse (`-s`), hybrid (`-h`), MTBDD (`-m`) + +If you already have a working `./bin/prism` invocation from the current session, +use that — you know the model and the expected result. + +--- + +## Step 2 — Pick the right directory + +All tests live under `../prism-tests/` (sibling of the `prism/` working +directory). Pick the most specific subdirectory that fits: + +| Situation | Directory | +|---|---| +| Bug fix (any model type) | `bugfixes/` | +| DTMC verification | `functionality/verify/dtmcs/` | +| CTMC verification | `functionality/verify/ctmcs/` | +| MDP reachability probability | `functionality/verify/mdps/reach/` | +| MDP expected rewards | `functionality/verify/mdps/rewards/` | +| MDP PCTL / LTL | `functionality/verify/mdps/pctl/` | +| PTA | `functionality/verify/ptas/` | +| Exact arithmetic | `functionality/verify/exact/` | +| Parametric | `functionality/verify/param/` | +| From a course or paper | `pmc/` or `papers/` | + +When in doubt, `bugfixes/` is always safe for anything fixing a known problem. + +Choose a short, descriptive file stem — e.g. `mdp_rmin_lp_inf` rather than +`test1`. Avoid generic names like `test` or `model`. + +--- + +## Step 3 — Create the model file + +Write the PRISM model as `.prism`. The extensions `.nm`, `.pm`, and `.sm` are historic aliases that still work but `.prism` is the modern default. +Do not create new tests with extension `.nm`, `.pm` or `.sm`. +Include a brief comment at the top explaining what the model demonstrates and +why it is interesting as a test case (future readers need to understand the +intent without running it). + +Working directory is `prism/`; the file goes in `../prism-tests//`. + +--- + +## Step 4 — Create the properties file (`.prism.props`) + +Every `// RESULT:` comment must appear on the line immediately before the +property it annotates. Property formulas must end with a semicolon (`;`). + +``` +// RESULT: 0.5 +Pmax=? [ F "done" ]; + +// RESULT: 10 +Rmin=? [ F "done" ]; +``` + +**Common result formats:** + +``` +// RESULT: 0.5 plain numeric +// RESULT: 1/3 exact fraction (preferred for exact values) +// RESULT: true boolean +// RESULT: Infinity infinite reward +// RESULT: [0.432,0.435] interval (floating-point bounds) +// RESULT: Error any error +// RESULT: Error:keyword error whose message contains "keyword" +// RESULT (N=2): 0.75 only applies when constant N=2 is set +// RESULT (exact=true): 1/3 conditional on a -const value from .args +``` + +**Key rules:** +- End every property formula with `;` — the test runner requires it. +- Use exact fractions (e.g. `5/3`) rather than decimals when the result is + mathematically exact — the test runner accepts both, but fractions are + preferred style in prism-tests. +- For iterative numerical methods, a decimal like `10.0` or an interval + `[9.999, 10.001]` is fine. +- `// RESULT: Infinity` (capital I) matches PRISM's literal output string. +- Multiple `// RESULT (...)` lines for the same property are OR'd — each is + checked against the engine configuration's constants/flags. + +--- + +## Step 5 — Get the actual result values + +Run the model with each intended engine to get the results you'll put in the +`.props` file. The `-test` flag makes PRISM parse and check the `// RESULT:` +comments, but first run **without** `-test` to capture the actual values: + +```bash +# From prism/ +./bin/prism ../prism-tests//.prism \ + ../prism-tests//.prism.props \ + +``` + +Note the printed results. If you already know the correct values (from a prior +run in the session, or from mathematical reasoning), skip this step. + +--- + +## Step 6 — Create the arguments file (`.prism.props.args`) + +List one set of engine flags per line. Each line becomes a separate test run. +Leave a blank line between logical groups if it helps readability (blank lines +are ignored by the runner). + +``` +-ex -lp +-ex -gs +-ex -politer +``` + +**Use abbreviated engine flags** — these are the conventional forms in prism-tests: + +| Abbreviation | Meaning | +|---|---| +| `-ex` | explicit engine (most actively developed) | +| `-s` | sparse engine | +| `-h` | hybrid engine | +| `-m` | MTBDD engine | +| `-lp` | LP solution method (explicit engine; selects it automatically) | +| `-gs` | Gauss-Seidel solver | +| `-politer` | policy iteration | +| `-valiter` | value iteration | +| `-ii` | interval iteration (combine with VI or GS: `-ex -ii`) | +| `-exact` | exact arithmetic | + +Do not use the long forms (`-explicit`, `-sparse`, `-hybrid`, `-mtbdd`) — +prism-tests convention is the short forms above. + +Decide how many engines the test is *meant* to cover. An LP-specific test only +needs `-ex -lp`. A general correctness test should cover several engines. +A bug-fix test should at minimum cover the engine where the bug appeared. + +--- + +## Step 7 — Verify with `-test` + +Run the test with PRISM's `-test` flag, which reads the `// RESULT:` comments +and reports PASS/FAIL: + +```bash +./bin/prism ../prism-tests//.prism \ + ../prism-tests//.prism.props \ + -test +``` + +Do this for each line of the `.args` file. Every result should print +`Testing result: PASS`. If any FAIL, adjust the `// RESULT:` annotations or +the model/property until all pass. + +Alternatively, use `prism-auto` to run all lines at once (from `prism/`): + +```bash +etc/scripts/prism-auto -t -m ../prism-tests//.prism -p ./bin/prism +``` + +--- + +## Step 8 — Confirm and report + +Tell the user: +- The three file paths created +- What each `.args` line tests and whether it passed +- Any non-obvious modelling choices (e.g. why a particular state has infinite + expected reward, why a certain result is exact) + +If you're amending an existing commit, stage and amend. If creating a new +commit, stage only the three test files (plus any source changes) and commit +with a descriptive message. diff --git a/prism/CLAUDE.md b/prism/CLAUDE.md new file mode 100644 index 000000000..b3d9bd435 --- /dev/null +++ b/prism/CLAUDE.md @@ -0,0 +1,163 @@ +# CLAUDE.md + +This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. + +## Repository Layout + +The working directory is `prism/` (one level below the repo root). Most build/test/run commands are executed from here. + +``` +repo-root/ + prism/ ← primary working directory (this file lives here) + prism-tests/ ← regression test suite + prism-examples/ ← example models and properties + cudd/ ← CUDD BDD library (C source) + manual/ ← HTML user manual +``` + +Inside `prism/`: +- `src/` — all Java and C++ source +- `unit-tests/` — JUnit 5 unit tests +- `bin/` — launch scripts (`prism`, `xprism`, `ngprism`) +- `etc/scripts/` — utilities including `prism-auto` (regression driver) +- `etc/tests/` — local smoke-test models/properties +- `ext/` — external library source (lpsolve) +- `lib/` — JAR dependencies and compiled native shared libraries +- `classes/` — compiled `.class` files (build output) +- `obj/` — compiled `.o`/`.so` files (build output) + +## Build Commands + +Run all of these from `prism/`. + +```bash +make # full build (CUDD + native C++ + Java) +make prism_java # Java-only recompile (fast after Java-only changes) +make parser # regenerate parser from src/parser/PrismParser.jj (JavaCC) +``` + +Java must target language level 11 (`javac --release 11`). Do not use Java 12+ language features. + +**Never run `make binary` (or otherwise create/update `lib/prism.jar`) during normal development.** That target packages a `lib/prism.jar` for binary releases only, and it is not part of the default `make`/`make prism_java` build. `bin/prism` puts `lib/prism.jar` *first* on the classpath, ahead of `classes/`, so if a stale jar is lying around it silently shadows freshly compiled classes and `./bin/prism` will run old code even after a successful `make prism_java`. If `lib/prism.jar` exists and isn't needed, remove it with `make clean_binary`. + +## Running PRISM + +Always use the local binary, never rely on a `prism` from `PATH` (a global install can cause misleading failures): + +```bash +# From prism/ +./bin/prism [options] + +# Example with explicit engine (-ex): +./bin/prism ../prism-tests/functionality/verify/dtmcs/dtmc_pctl.pm \ + ../prism-tests/functionality/verify/dtmcs/dtmc_pctl.pm.props -ex +``` + +Engine flags: `-mtbdd` (MTBDD/symbolic), `-sparse`, `-hybrid`, `-explicit` / `-ex` (most actively developed). + +## Testing + +From `prism/`: + +```bash +make test # smoke test (one DTMC PCTL check) +make unittests # compile and run JUnit unit tests +make tests # full regression suite (../prism-tests/), via Nailgun +make testsfull # all engines, all variants, with timeout +etc/tests/run.sh # alternative smoke-test runner +``` + +Extra `prism-auto` options can be passed to `make tests` via `TESTS_ARGS=...`. + +To run a single JUnit test class (after `make unittests` has compiled): + +```bash +java -jar lib/junit-platform-console-standalone-*.jar \ + -cp classes \ + --select-class \ + --details=summary +``` + +For regression tests, targeted reproduction is preferred over broad test suites — reproduce the failing case with a specific `./bin/prism` invocation first. + +For a scoped/custom regression run over part of `prism-tests/` (e.g. one subdirectory, or with extra flags like `--test-all`), run `etc/scripts/prism-auto` with the same core options the Makefile uses: + +```bash +# From prism/ +etc/scripts/prism-auto -t -m ../prism-tests/ -p ./bin/prism \ + --nailgun --ngprism ./bin/ngprism +``` + +- **`-m`/`--matching` is required alongside `-t`/`--test`.** Without it, `prism-auto` cross-tests every model against every properties file in a directory, producing spurious failures (e.g. "Undeclared label") from nonsensical file pairings that look like real regressions but aren't. +- **`-p ./bin/prism` is required.** `prism-auto` defaults to whatever `prism` is on `PATH`, so without it you may silently test a different install rather than your local build. (`etc/scripts/prism-test` is a shorthand for `prism-auto -m -t`, but it also relies on `PATH` for both `prism-auto` and `prism`, so still pass `-p ./bin/prism` to it.) +- **Use `--nailgun`** for any run of more than a handful of tests. It reuses one persistent JVM (`bin/ngprism`) across the whole run instead of starting a fresh one per invocation, which is far faster. It requires **JDK 23 or earlier**: for Java ≥ 19, `prism-auto` starts Nailgun with `-Djava.security.manager=allow`, which JDK 24 removed (JEP 486), so Nailgun mode cannot start under JDK 24+. Check with `java -version` and switch to an older JDK (e.g. 21) if needed. + +## Architecture + +### Computation Engines + +PRISM has four selectable engines defined as constants in `src/prism/Prism.java`: + +| Constant | Flag | Description | +|---|---|---| +| `MTBDD = 1` | `-mtbdd` | Symbolic, BDD-based (uses CUDD via JNI) | +| `SPARSE = 2` | `-sparse` | Explicit matrix via C++ sparse routines (JNI) | +| `HYBRID = 3` | `-hybrid` | Hybrid BDD + explicit (JNI) | +| `EXPLICIT = 4` | `-ex` | Pure Java explicit-state — most actively developed | + +### Key Source Packages (`src/`) + +| Package | Role | +|---|---| +| `prism/` | Core API: `Prism.java` (main API class), `PrismCL.java` (CLI entry point), model type enums, interfaces | +| `explicit/` | Explicit-state engine: model classes (`DTMCSimple`, `MDPSimple`, `CTMCSimple`, `POMDP`, `STPG`, …) and model checkers (`DTMCModelChecker`, `MDPModelChecker`, etc.) | +| `symbolic/` | Symbolic (MTBDD) engine: BDD-based model checkers | +| `hybrid/` | Hybrid engine: `PrismHybrid.java` + JNI C++ files | +| `sparse/` | Sparse engine: `PrismSparse.java` + JNI C++ files | +| `dd/`, `jdd/`, `odd/`, `dv/`, `mtbdd/` | BDD and decision diagram layers (C++ + Java JNI wrappers) | +| `parser/` | PRISM language parser (JavaCC grammar `PrismParser.jj`) and AST classes | +| `simulator/` | Statistical model checking / simulation engine | +| `param/` | Parametric model checking (rational functions) | +| `pta/` | Probabilistic timed automata (digital clocks translation) | +| `automata/` | LTL-to-automaton translation (Rabin, Büchi, WDBA, HOA) | +| `acceptance/` | Acceptance condition classes (Büchi, Rabin, Streett, etc.) | +| `strat/` | Strategy/policy computation and export | +| `io/` | Model import/export (DRN, DOT, UMB/PRISM explicit format, Matlab) | +| `settings/` | PRISM settings and preferences | +| `userinterface/` | Swing GUI — `GUIPrism` is the JAR manifest `Main-Class` | + +### Entry Points + +- **CLI:** `bin/prism` → `prism.PrismCL.main()` +- **GUI:** `bin/xprism` → `userinterface.GUIPrism` +- **Nailgun daemon:** `bin/ngprism` — persistent JVM for fast repeated CLI invocations + +### Parser + +The PRISM modelling language parser is generated by JavaCC from `src/parser/PrismParser.jj`. After editing the grammar, regenerate with `make parser`. The resulting AST classes live alongside the grammar in `src/parser/ast/`. + +### The umbj Library + +The general-purpose UMB import/export functionality forms a standalone library `umbj`. +But the code is also kept within PRISM, since most development happens there, +and is ported across. So code changes that involve UMB should if necessary be +split into commits that only touch `src/io/github/pmctools/umbj` (which should not use +any other classes from the PRISM codebase) and PRISM-specific code. The first line +of commit messages for the former type should be prefixed "umbj: ". + +## Coding Guidelines + +- Keep fixes minimal and localized; do not refactor unrelated code in the same change. +- Preserve existing style and naming conventions throughout. +- Add or adjust tests when behavior changes or bugs are fixed (see the `prism-add-test` skill in `.claude/skills/`). +- Don't add tests whose expected output pins one particular strategy/policy when several are equally optimal: PRISM does not specify which one is chosen. Only test a strategy when it is the unique valid one. +- Avoid introducing new dependencies unless explicitly requested. +- Java language level 11 is required — do not use features from Java 12+. + +## Bug Fix Workflow + +1. Reproduce the issue with an exact `./bin/prism` command. +2. Implement the smallest defensible fix. +3. Rebuild (`make` or `make prism_java` for Java-only changes). +4. Re-run the reproduction command (multiple times if nondeterministic). +5. Run nearby regression tests where feasible.