[CatarinaGamboa]

Closes #14

What changes

The verifier tries a method's @StateRefinements in declaration order and uses the first one whose from matches (AuxStateHandler.changeState). A @StateRefinement without from has from = true, so:

• Edges — it now only goes from the states that the earlier from= alternatives of the same method do not cover. A state counts as covered when an earlier from names it without a condition.
• Entry transitions — when it sits beside from= alternatives, it also becomes a StateMachineEntryTransition(to, label, toCondition) in the new StateMachine.entryTransitions list: how an object whose state is unknown (a field, a parameter, a getter result) enters the protocol. Clients can draw it as [*] --> to: label.
• A from-less @StateRefinement with no alternatives keeps its edges from every state and gets no entry transition (it really applies in every known state, see ToOnlyTransition).

For the UndoManager canUndo() in the issue, the four canUndo [return] → endDone edges are gone; instead there is one entry transition [*] → endDone: canUndo [return], plus the self-loops from the from= alternatives.

Compatibility

StateMachine gets a new component entryTransitions. The existing 4- and 5-argument constructors are kept and default it to an empty list. The MCP's get_state_machine and the VS Code extension will need a follow-up to render the new list.

Tests

• EntryTransition.java fixture: the canUndo spec from the issue, plus a reset() whose from-less alternative still goes from the uncovered states.
• testToOnlyTransitionHasNoEntryTransition: a from-less refinement alone adds no entry transition.
• mvn test: 27 tests, 0 failures.

🤖 Generated with Claude Code