Repository navigation
Commit 34d7611
Focus the state machine on the rejected call (#158)
## 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>1 parent 6b10158 commit 34d7611
11 files changed
Lines changed: 900 additions & 21 deletions
File tree
- client/src
- types
- webview
- views/fsm
- server
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
11 | 11 | | |
12 | 12 | | |
13 | 13 | | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
14 | 20 | | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
| 70 | + | |
| 71 | + | |
| 72 | + | |
| 73 | + | |
| 74 | + | |
| 75 | + | |
| 76 | + | |
| 77 | + | |
| 78 | + | |
| 79 | + | |
| 80 | + | |
| 81 | + | |
| 82 | + | |
| 83 | + | |
| 84 | + | |
| 85 | + | |
| 86 | + | |
| 87 | + | |
| 88 | + | |
| 89 | + | |
| 90 | + | |
| 91 | + | |
| 92 | + | |
| 93 | + | |
| 94 | + | |
| 95 | + | |
| 96 | + | |
| 97 | + | |
| 98 | + | |
| 99 | + | |
| 100 | + | |
| 101 | + | |
| 102 | + | |
| 103 | + | |
| 104 | + | |
| 105 | + | |
| 106 | + | |
| 107 | + | |
| 108 | + | |
| 109 | + | |
| 110 | + | |
| 111 | + | |
| 112 | + | |
| 113 | + | |
| 114 | + | |
| 115 | + | |
| 116 | + | |
| 117 | + | |
| 118 | + | |
| 119 | + | |
| 120 | + | |
| 121 | + | |
| 122 | + | |
| 123 | + | |
| 124 | + | |
| 125 | + | |
| 126 | + | |
| 127 | + | |
| 128 | + | |
| 129 | + | |
| 130 | + | |
| 131 | + | |
| 132 | + | |
| 133 | + | |
| 134 | + | |
| 135 | + | |
| 136 | + | |
| 137 | + | |
| 138 | + | |
| 139 | + | |
| 140 | + | |
| 141 | + | |
| 142 | + | |
| 143 | + | |
| 144 | + | |
| 145 | + | |
| 146 | + | |
| 147 | + | |
| 148 | + | |
| 149 | + | |
| 150 | + | |
| 151 | + | |
| 152 | + | |
| 153 | + | |
| 154 | + | |
| 155 | + | |
| 156 | + | |
| 157 | + | |
| 158 | + | |
| 159 | + | |
| 160 | + | |
| 161 | + | |
| 162 | + | |
| 163 | + | |
| 164 | + | |
| 165 | + | |
| 166 | + | |
| 167 | + | |
| 168 | + | |
| 169 | + | |
| 170 | + | |
| 171 | + | |
| 172 | + | |
| 173 | + | |
| 174 | + | |
| 175 | + | |
| 176 | + | |
| 177 | + | |
| 178 | + | |
| 179 | + | |
| 180 | + | |
| 181 | + | |
| 182 | + | |
| 183 | + | |
| 184 | + | |
| 185 | + | |
| 186 | + | |
| 187 | + | |
| 188 | + | |
| 189 | + | |
| 190 | + | |
| 191 | + | |
| 192 | + | |
| 193 | + | |
| 194 | + | |
| 195 | + | |
| 196 | + | |
| 197 | + | |
| 198 | + | |
| 199 | + | |
| 200 | + | |
| 201 | + | |
| 202 | + | |
| 203 | + | |
| 204 | + | |
| 205 | + | |
| 206 | + | |
| 207 | + | |
| 208 | + | |
| 209 | + | |
| 210 | + | |
| 211 | + | |
| 212 | + | |
| 213 | + | |
| 214 | + | |
| 215 | + | |
| 216 | + | |
| 217 | + | |
| 218 | + | |
| 219 | + | |
| 220 | + | |
| 221 | + | |
| 222 | + | |
| 223 | + | |
| 224 | + | |
| 225 | + | |
| 226 | + | |
| 227 | + | |
| 228 | + | |
| 229 | + | |
| 230 | + | |
| 231 | + | |
| 232 | + | |
| 233 | + | |
| 234 | + | |
| 235 | + | |
| 236 | + | |
| 237 | + | |
| 238 | + | |
| 239 | + | |
| 240 | + | |
| 241 | + | |
| 242 | + | |
| 243 | + | |
| 244 | + | |
| 245 | + | |
| 246 | + | |
| 247 | + | |
| 248 | + | |
| 249 | + | |
| 250 | + | |
| 251 | + | |
| 252 | + | |
| 253 | + | |
| 254 | + | |
| 255 | + | |
| 256 | + | |
| 257 | + | |
| 258 | + | |
| 259 | + | |
| 260 | + | |
| 261 | + | |
| 262 | + | |
| 263 | + | |
| 264 | + | |
| 265 | + | |
| 266 | + | |
| 267 | + | |
| 268 | + | |
| 269 | + | |
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
| 1 | + | |
| 2 | + | |
| 3 | + | |
| 4 | + | |
| 5 | + | |
| 6 | + | |
| 7 | + | |
| 8 | + | |
| 9 | + | |
| 10 | + | |
| 11 | + | |
| 12 | + | |
| 13 | + | |
| 14 | + | |
| 15 | + | |
| 16 | + | |
| 17 | + | |
| 18 | + | |
| 19 | + | |
| 20 | + | |
| 21 | + | |
| 22 | + | |
| 23 | + | |
| 24 | + | |
| 25 | + | |
| 26 | + | |
| 27 | + | |
| 28 | + | |
| 29 | + | |
| 30 | + | |
| 31 | + | |
| 32 | + | |
| 33 | + | |
| 34 | + | |
| 35 | + | |
| 36 | + | |
| 37 | + | |
| 38 | + | |
| 39 | + | |
| 40 | + | |
| 41 | + | |
| 42 | + | |
| 43 | + | |
| 44 | + | |
| 45 | + | |
| 46 | + | |
| 47 | + | |
| 48 | + | |
| 49 | + | |
| 50 | + | |
| 51 | + | |
| 52 | + | |
| 53 | + | |
| 54 | + | |
| 55 | + | |
| 56 | + | |
| 57 | + | |
| 58 | + | |
| 59 | + | |
| 60 | + | |
| 61 | + | |
| 62 | + | |
| 63 | + | |
| 64 | + | |
| 65 | + | |
| 66 | + | |
| 67 | + | |
| 68 | + | |
| 69 | + | |
0 commit comments