/nw-po-scenario-exploration

name: nw-po-scenario-exploration
description: Assess product values for Quint relevance and explore them through actual traces and mechanically rendered scenarios for human review.
user-invocable: false
disable-model-invocation: true

Product Scenario Exploration

**Kind**: PROCEDURE | **Job**: explore product behavior through actual Quint scenarios. **Trigger**: assess each DISCUSS value's relevance before constructing the brief/handoff.

Per-value relevance (single owner of this rule)

Does any value have a sad path: refusal, conflict, concurrency/race, stale or invalid input, or a missing operand? Then it is Quint-relevant by definition: prepare its product questions and actor observations for bounded exploration, even when the expected sad-path behavior is settled. Also explore unclear order, timing or state interactions, and human-requested model-generated alternatives. Only settled happy-path-only behavior may skip exploration without an availability or human-refusal reason. Supply each value's explicit relevance judgment and reason; one feature-level unavailability statement is not a per-value judgment.

For relevant values, run Quint inside the PO-human collaboration sequence, before settling product facts, not as an afterthought or separate offer. This introduces no wave, solver-owned route or formal-method gate.

Collaboration sequence (single owner of this policy)

| Mode | Sequence | |---|---| | Interactive | initial concrete examples -> model actual assumptions -> actual Quint traces -> deterministic domain rendering -> human judgment -> revise/regenerate changed choices/model -> settled product facts and brief | | Auto (delegated) | same steps without waiting; supply actual generated scenarios and assumptions or unresolved doubts for human reading and product authority. Silence or no human reply is never approval; keep it Open |

Question and value authority stay with the human unless explicitly delegated. The LLM orchestrates. Default documents are English; the human conversation uses the human's language (`nw-human-collaboration`). The modeler writes readable Quint; the PO never needs to read code.

Human authority

The human owns the intended behavior. The PO proposes contrasting scenarios and records the judgment, actor and conditions. A repeated choice supports those cases only; it does not prove general translation fidelity. Disagreement may expose an incorrect translation, ambiguity, changed intent or unclear rendering.

The LLM orchestrates tool use within the active roles' capabilities and requests model-capable help when needed. Product reasoning starts from the user's point of view; implementation code is unnecessary. The solver controls no delivery route. Installation still requires authorization.

Availability and installation

The execution owner probes `quint --version`, including a configured local binary when applicable. If unavailable, explain its purpose and offer a host-appropriate installation once, as for Agda. Install only with authorization; preserve an earlier acceptance or refusal. Check the host's Node/npm availability and the official Quint installation instructions before suggesting commands. On refusal or unsupported tooling, continue ordinary scenario discussion and mark formal exploration unavailable. Never present invented traces as tool output.

Model to human review

• Select a concrete operation pair and observation; where M2 is in use, identify

its candidate relation. One example pair does not establish a general law.

• Separate recorded human choices from modeler assumptions. Timing needs an

explicit clock/unit; simulation steps alone are not seconds. Name delivery, fairness and failure-detection assumptions rather than hiding them.

• Generate traces from the actual model. Retain model identity, tool version,

command, seed/bounds and raw trace. Simulation is not exhaustive verification; Quint exploration does not establish FRET realizability or conflict diagnosis.

• Use a verified deterministic renderer with explicit domain action templates.

Show actors, order, actual versus observed state, time and relevant conditions. Preserve trace indices and model identity; disclose any prefix or projection. Unsupported actions are reported, never filled in with invented narration. If no suitable renderer is available, report that integration gap.

• Let the human review the readable scenarios without reading Quint or formulas:

correct, incorrect, depends, unclear, or a proposed correction. Show assumptions and allow challenging the wording itself; do not preselect acceptance.

• Record the judgment against the exact model/scenario. An open question remains

open; silence is not approval. Revise the model after an actual decision, then generate fresh scenarios for review. Keep automated review distinct from the human's semantic judgment and respect explicitly delegated collaboration mode.

Tool reference: https://quint.sh/docs/quint

DISCUSS integration and HTML

For each relevant value, the PO returns product questions and actor observations to the host as an execution request rather than declaring exploration unrun. The host selects a model-capable helper for bounded Quint work within authorized tooling. The helper owns the model and raw trace evidence, not product intent. Return model assumptions and deterministically rendered scenarios to the PO before settling product authority.

Render trace events through domain templates, then share the readable scenario in the local nWave HTML view using `nw-doc-as-artifact`. This has two distinct transformations: trace-to-domain-scenario (must preserve events mechanically) and document-to-branded-HTML (the existing shared renderer). The HTML renderer alone does not implement the trace transformation. If that first component is absent, report it instead of writing an LLM paraphrase and calling it mechanical.

After actual feedback, supply revised scenari