State hints: name only the state the call leads to #519

Since #517 the hints write named-set states in value form, which keeps them close to the spec. But each hint now repeats the "from" side, which the Found already shows, and lists every state of a set. The hints are about twice as long:

Call host.dispose() before this call to move host from display(host) == notDisplayable or display(host) == displayable to display(host) == notDisplayable

In A1_09, "from notDisplayable or displayable" lists every state of the set, so it reads like a contradiction. It comes from a closed-world projection (StateSolver.possibleStates).

Proposal

Keep the value form, but write at most one state per hint, the one the call leads to:

• CALL_SEQUENCE: Call buffered.mark(int) before this call; afterwards markState(buffered) == marked. No "from" part. afterwards is the machine's after state.
• Arguments: write a deciding argument mode == ImageWriteParam.MODE_EXPLICIT as the call itself: Call wParam.setCompressionMode(ImageWriteParam.MODE_EXPLICIT) before this call; afterwards ....
• AVAILABLE_CALLS: drop the "can call" hint when any other hint exists.

Lengths (characters):

Soundness: the hint states only what the verifier computes after the call, so it never writes != as ==.