State Machine view: show a multi-set state error in the set that is wrong #180

When a call needs states of two state sets, the State Machine view draws one diagram per set, but the error is about both together. Door example (d.lock(); d.open();, open needs doorState(this) == closed && lockState(this) == unlocked), screenshots in #178:

1. The red arrow is in the wrong diagram. open from closed is red in the doorState diagram, although closed is right for that set. What fails is the condition lockState(this) == unlocked, which nothing marks as unmet.
2. The diagram with the actual problem is below the fold. In focus mode lockState comes second and is cut off. It has the wrong state (locked) and the way out (unlock), which is not highlighted.
3. Self-loops that need a state and keep it (lock on closed, open on unlocked) are tiny curls; the open loop in lockState is the most relevant edge for this error.
4. Guards are raw spec text in mixed forms (lockState(this) != locked next to lockState(this) == unlocked), and their labels float away from their edges.
5. The summary line doesn't name the sets: "expected state closed and unlocked · actual state closed and locked".

Proposal

• Mark the failure where it is. In a set whose state is right, draw the call normally and show its unmet condition in red. In the wrong set's diagram, draw the call red.
• Focus on the wrong set. Put the diagram with the wrong state first and fit the view to it; highlight the ways to fix from the verifier's hints (here unlock).
• Make "needs and keeps" self-loops readable, especially the failing one.
• Write guards as conditions on the other set, e.g. [lockState: unlocked]; a != on a set with two states becomes the other state. Keep labels attached to their edges.
• Name the sets in the summary line: "expected doorState closed, lockState unlocked · actual lockState locked" (unnamed sets keep the current wording).

Not in scope: marking states that are current and fine (undecided).

Study exercises with the same two-set shape: A1_38 (stream, mark), A1_01 (tiling, compression), A1_56 (phase, undo, redo).