Claude Code instructions & prism-add-test skill

.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/

CLAUDE.md

@@ -0,0 +1 @@
+@prism/CLAUDE.md

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 `<stem>.prism` (or historic aliases `.nm`/`.pm`/`.sm`), a properties file
+`<stem>.prism.props`, and an optional engine-arguments file `<stem>.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 `<stem>.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/<subdir>/`.
+
+---
+
+## Step 4 — Create the properties file (`<stem>.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/<subdir>/<stem>.prism \
+            ../prism-tests/<subdir>/<stem>.prism.props \
+            <engine-flags>
+```
+
+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 (`<stem>.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/<subdir>/<stem>.prism \
+            ../prism-tests/<subdir>/<stem>.prism.props \
+            <engine-flags> -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/<subdir>/<stem>.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.

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 <model-file> <props-file> [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 <fully.qualified.TestClassName> \
+  --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/<subdir> -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.