Focus the state machine on the rejected call and relevant states

[CatarinaGamboa]

Problem

Opening a state machine from a state refinement error can show an overwhelming full diagram. The view currently highlights some found states and method labels, but it does not clearly show the required states or focus the viewport on the failure. In a diagram with many transitions, such as Socket, the relevant part is hard to find.

A highlighted transition can also imply that the rejected call took place successfully.

Example

Consider these state rules for DefaultMutableTreeNode:

@StateSet({"childrenAllowed", "maybeHasChildren"})
interface NodeStates {
    @StateRefinement(to="childrenAllowed(this)")
    void DefaultMutableTreeNode(Object value);

    @StateRefinement(from="childrenAllowed(this)",
                     to="maybeHasChildren(this)")
    void add(MutableTreeNode child);

    @StateRefinement(from="maybeHasChildren(this)",
                     to="childrenAllowed(this)")
    void removeAllChildren();

    @StateRefinement(from="maybeHasChildren(this)")
    TreeNode getFirstChild();
}

And this call sequence:

DefaultMutableTreeNode root = new DefaultMutableTreeNode("outline");
root.add(new DefaultMutableTreeNode("section"));
root.removeAllChildren();
TreeNode landing = root.getFirstChild(); // state error

At the last call, Found is childrenAllowed(root) and Expected is maybeHasChildren(root).

Proposed behavior

When opened from a selected state error, start with a focused view that:

• Centers and fits the found state, the rejected call, and all states accepted by the call's precondition. Keep their labels readable.
• Marks the found state in red: “Found for this receiver at the call.”
• Shows a separate red marker: “Call rejected from this state.” Show it even if the method is absent from the general diagram or buried in a merged label.
• Marks each required state in green: “Required for this call.”
• Reduces unrelated diagram content in the initial view so large machines do not overwhelm the error. Provide “Show full diagram” and “Focus on error” controls, while retaining pan and zoom.

The rejected-call marker must not be drawn as a successful state transition. In the example, getFirstChild() does not move root to maybeHasChildren.

Accuracy and accessibility

• Use the verifier's method, receiver, Found condition, and required condition; do not identify a call by transition label text alone.
• If Found does not establish one definite state, display the condition without selecting a single red node.
• Include text or icons so the overlay is understandable without color.
• Keep the general diagram available when no error is selected.
• Coordinate with #116 to focus the correct diagram when there are multiple @StateSet groups.

Acceptance criteria

• The example opens focused on childrenAllowed(root), the rejected getFirstChild() call, and the required maybeHasChildren state.
• The initial view of a large machine such as Socket makes the relevant error area readable without manually searching the full graph.
• The user can switch to the full diagram and return to error focus.