Skip to content

Add the receiver's possible states to the error context - #11

Merged
CatarinaGamboa merged 1 commit into
mainfrom
feat/possible-states
Oct 24, 2026
Merged

Add the receiver's possible states to the error context#11
CatarinaGamboa merged 1 commit into
mainfrom
feat/possible-states

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Oct 24, 2026

Copy link
Copy Markdown
Contributor

Closes #10.

Summary

  • Adds possibleStates as the last field of StateMachineErrorContext. These are the states the Found premises allow for the receiver, in state set order. The VS Code State Machine view uses them to split the receiver's states into Valid (P ∩ A) and Invalid (P \ A), where A is expectedStates (Focus the state machine on the rejected call vscode-liquidjava#158).
  • Each conjunct of the receiver's premises that mentions its states is evaluated the same way as expectedStates (||, !, ternaries), and the results are intersected.
    • Conjuncts that do not mention the receiver's states do not restrict P.
    • No information about the receiver gives every state. No receiver gives an empty list. A contradiction gives an empty list.
  • When definiteFoundState is set, possibleStates is exactly that state.

Tests

New tests:

  • UDP chat client, from the study example, with the real verifier. The single error is on socket.receive(...):
    • Found #fresh ? closed(socket) : bound(socket)
    • possibleStates [bound, closed]
    • expectedStates [unbound, bound, connected]
    • calledMethod receive
    • receiver socket
    • definiteFoundState null
  • 14 Found shapes, constructed directly;
  • a negated Found (!closed) that excludes closed;
  • no receiver;
  • consistency with definiteFoundState.

Existing error-context tests now also assert possibleStates. mvn test: 35 tests, all pass.

🤖 Generated with Claude Code

@CatarinaGamboa @claude
Add the receiver's possible states to StateMachineErrorContext
d11acf0 
possibleStates lists, in state set order, the states the receiver's found
premises allow. Each conjunct about the receiver is evaluated like the
expected condition and the results are intersected; with nothing known
about the receiver every state is possible.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa
CatarinaGamboa merged commit 8b9d03e into main Oct 24, 2026
2 checks passed
@CatarinaGamboa CatarinaGamboa mentioned this pull request Oct 24, 2026
Merged
CatarinaGamboa added a commit to liquid-java/vscode-liquidjava that referenced this pull request Oct 24, 2026
@CatarinaGamboa @claude
Focus the state machine on the rejected call (#158)
34d7611 
## Description
Closes #117.

When the State Machine view is opened from a state refinement error, it
marks the rejected call on the full diagram. There are two sets of
states:
- **P**, the states the receiver can be in, from Found;
- **A**, the states the call accepts, from Expected.

The view marks:
- **Invalid, P \ A**: red outline and **✕**. The call fails from here.
- **Valid, P ∩ A**: green outline and **✓**. The call is fine from here.
- **Accepted but not possible here, A \ P**: a thin dashed yellow
outline and no text. It hints at where the object could be brought.
- **The failed method**: every arrow labelled with it gets a red label,
including inside merged labels. The rejected call is never drawn as a
new transition.

Red and green have a faint fill and yellow is outline only, so a large
machine stays calm.

The full diagram is always shown. Focus mode dims what does not help
with the error:
- states outside P ∪ A;
- constructors;
- every method name that is neither the failed method nor a transition
that moves the receiver out of a state in P to a different state. This
applies to each name inside merged labels: in `getOption / receive /
send / …` only `receive` stays bright.

An arrow's path is dimmed only when all of its names are. "Show all" and
"Focus on error" switch the dimming off and on and keep pan and zoom.
The label text is identical in both modes, so the layout does not move.

A one-line legend shows only the marks that are present: "✕ Call
rejected", "✓ Call allowed" and "Allowed, but not reachable here". In
light themes the dashed outline uses a darker warning colour.

One summary line sits above the diagram, e.g. "`socket.receive()` is
rejected when `socket` is in state `closed` · allowed in state `bound`".

**Edge cases**
- When the receiver's state is unknown (every state is possible), only A
is marked, and the summary says the state is unknown.
- With no known receiver or accepted states, or with an older server,
the view behaves as on `main`.

**Data**
- P is `possibleStates` (liquid-java/liquidjava-fsm#11). With an older
server, it falls back to `definiteFoundState` and then `actualStates`.
- A is `expectedStates`.
- **Dependency:** bumps `liquidjava-fsm` to 0.1.5.
- The call is matched by its exact method name from the error context,
not by label text.
- "Copy Mermaid Source" copies the plain diagram.

## Screenshots
These are real verifier output in headless VS Code.

**UDP chat client.** The study example `E_OSS_A1_22_UdpChatClient`:
`receive` after an `if` that may close the socket. In focus mode the
following stay bright:
- `receive`;
- `close` and `connect` out of `bound`;
- the accessors out of `closed`.

The accessors stay bright because the DatagramSocket spec writes `from =
"closed(this) && connected(old(this))"`, which is drawn as an arrow from
`closed` to `connected`. That `old(...)` in a `from` is a spec error,
not an extension issue.

<img width="720" alt="DatagramSocket focus: only receive, close and
connect stay bright"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/udp-focus-methods.png"
/>

<details><summary>Whole UDP machine: focus in dark and light, and Show
all</summary>

<img width="560" alt="UDP focus, dark"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/udp-dark.png"
/> <img width="560" alt="UDP focus, light"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/udp-light.png"
/>

<img width="560" alt="UDP Show all"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/udp-show-all.png"
/>
</details>

**DefaultMutableTreeNode** (the issue's example). `getFirstChild()`
after `removeAllChildren()`:
- `childrenAllowed` is invalid;
- `maybeHasChildren` is accepted;
- `add`, the way there, stays bright;
- `removeAllChildren` is dimmed.

<img width="560" alt="Tree focus, dark"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/tree-dark.png"
/> <img width="560" alt="Tree focus, light"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/tree-light.png"
/>

<details><summary>Dimmed unrelated state (simplified demo machine, not a
real class)</summary>

<img width="560" alt="Dimmed unrelated state"
src="https://raw.githubusercontent.com/liquid-java/vscode-liquidjava/pr-screenshots/158/dimming-demo.png"
/>
</details>

## Tests
Run against liquidjava-fsm 0.1.5 and verifier 0.0.35 from Maven Central:
- `npm run lint` and `npm run test:typecheck`: clean.
- `npm run test:unit`: 75 passed in 7 files.
- `npm test` (VS Code): 8 + 1 passing.
- Server `mvn test`: 24 passing.
- Local smoke test: passed.

The new tests cover:
- the split into Valid, Invalid and accepted states;
- the fallbacks and the unknown-state case;
- empty or unknown states;
- exact method matching (`receive` does not match `receiveAll`);
- red labels inside merged labels;
- dimming of rendered paths and labels, per-name dimming inside merged
labels, and the rule for which methods count as useful;
- the legend;
- dimmed constructors;
- diagram clipping below the summary when panned;
- the toggle keeping zoom;
- plain Mermaid copy;
- the computed outline styles.

Independently reviewed twice; all findings were fixed.

## Known limits
- Large machines such as DatagramSocket have long stacked self-loop
labels. This already happens on `main`.
- #159 touches the same webview files; whichever PR merges second will
be rebased.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Add the receiver's possible states to the error context

1 participant

@CatarinaGamboa