[CatarinaGamboa]

Follows the verifier's named state sets (liquid-java/liquidjava#498) and states written as values of their sets (liquid-java/liquidjava#510, design in liquid-java/liquidjava#502).

Problem

With the verifier on main, a spec can write

@StateSet(name = "phase", value = {"open", "closed", "broken"})
...
@StateRefinement(from = "open == this.phase()", to = "closed(this)")

The parser took open == phase(this) for a condition that holds in any state, so close was drawn from open, closed and broken, each with the condition open == phase(this). phase(this) != open went the same way, and a value of another set in a to was kept instead of being left out.

Change

• getStateName also reads set(x) == state and state == set(x) (a one-argument function compared with a state) as the state, and getNegated reads a != b as the negation of a == b, like !. This is the verifier's reading (StateValues.toShorthand), and it applies wherever the shorthand is read: from, to, constructors and factories, this.phase(), phase(), old(this), and generated names such as state2(this) == unlocked.
• Conditions keep the form the spec wrote, e.g. phase(this) != broken.
• StateMachine gets stateSetName: the name of its @StateSet, or null when it has none. Generated names (state1, ...) are not exposed, since the verifier does not show them in messages either. The old six-argument constructor is kept, as vscode-liquidjava uses it.
• README: the new field and the value form.

Unchanged: the parser stays as lax as for the shorthand (it does not check that the function is a state set of the class, nor that a parameter is named like a state); a spec where that matters is rejected by the verifier.

Tests

One fixture, StateValues.java (a named and an unnamed set, == in both orders, !=, this.phase(), phase(), a generated name, mixed with the shorthand), and one test that fails without the change. mvn test passes locally (33 tests).

Screenshots of the diagrams before and after, in VS Code: liquid-java/vscode-liquidjava#178.

A release is needed before vscode-liquidjava can use stateSetName (PR to follow there).

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

codex exec review --base origin/main:

• [P2] Recognize zero-argument state-set comparisons (StateMachineParser.java:796-799): when a refinement uses phase() == open, getStateValue rejects the zero-argument call, even though the new test fixture uses phase() != broken. An equality in to then produces no destination state, while one in from becomes a guard on every state rather than selecting open.
• [P2] Check which state set the comparison calls (StateMachineParser.java:796-799): with several state sets, any one-argument function compared with a state name is taken as a value of the current set. phase(this) == unlocked is parsed as an unlocked transition for the unlocked/locked set, although phase names the open/closed/broken set.

Response

Both declined:

1. Zero arguments: the refinements parser already reads phase() as phase(this), and this.phase() too (checked on verifier 0.0.36: phase() == open gives a FunctionInvocation phase with the argument this). The fixture's phase() != broken is covered by the test and gives open and closed, not a guard.
2. Wrong set: phase(this) == unlocked is rejected by the verifier (State 'unlocked' is not a state of 'phase' (its states are ...)), so the diagram never has to draw it. The parser is equally lax for the shorthand: it does not check that unlocked(other) is about this either. Checking the set name would mean passing the state set names through every helper for a spec the verifier rejects.

No changes in this round.

[CatarinaGamboa]

Codex review, round 2

codex exec on git diff origin/main...HEAD, told the reasons for the two findings declined in round 1:

StateMachineParser.java:810: getNegated treats every != involving a state as the complement of that state. The verifier accepts from = "open(this) != false", but the parser draws close from closed instead of open.

Response

Fixed in b5a1061: getNegatedStates now reads a != b as a negation only when a == b is itself a state written as a value of its set. open(this) != false is parsed as on main again (a condition), so no new test: it behaves as before this PR.

[CatarinaGamboa]

Codex review, round 3

codex exec on git diff origin/main...HEAD, with the round 1 and 2 outcomes: No findings. The loop ends here.

[CatarinaGamboa]

Clean-code review

Audit of this PR's diff against the clean-code-principles checklist (file:line - [principle] issue):

• StateMachineParser.java:615-623 and :756-761 - [core-dry] the complement of the negated states is built twice, once as TransitionSources and once as names. Declined: the duplication was already on main (the two ! branches); this PR only changes where the negated states come from, and the PM prefers small PRs over refactors.
• StateMachineParser.java:753 - [core-kiss] getStateExpressions computes getNegatedStates even when the expression is already a state. Declined: one extra walk of a small refinement; computing it inside the branch would need the else-chain split up.
• StateMachineParser.java:807 - [core-dry] getNegatedStates builds a == b to reuse getStateName, rather than repeating the two operand orders. Kept on purpose.
• StateMachine.java:20 - [core-yagni] the old six-argument constructor is kept. Kept: it is the public constructor vscode-liquidjava's tests and the shorter constructors use; removing it would break callers for no gain.
• Naming (StateSet, getStateSetName, getStateValue, getNegatedStates) and function size follow the file's existing style. No findings on SOLID.

No changes.