False error: a known state 'a or b' is refused by a method allowed from a and from b (one @StateRefinement per state) #445

Impact: after any branch that leaves an object in one of two states (if, try/catch, try/finally), a method that is allowed in both states is refused, if its spec lists one @StateRefinement per state. The error message itself shows that the required state holds. This hits the most common resource idioms: close() in finally, and a timed-out accept() in try/catch.

Minimal reproducer

import liquidjava.specification.StateRefinement;
import liquidjava.specification.StateSet;

@StateSet({"open", "closed"})
class Res {
    @StateRefinement(to = "open(this)")
    public Res() {}

    @StateRefinement(from = "open(this)", to = "closed(this)")
    @StateRefinement(from = "closed(this)")
    public void close() {}
}

public class Repro {
    static void use(boolean early) {
        Res r = new Res();
        if (early) r.close();
        r.close();          // r is open or closed here; close() is allowed in both
    }
}

Expected: Correct! Passed Verification.

Actual (main @ f7f366c, and 1a506fe):

State Refinement Error: found early ? closed(r) : open(r) but expected open(r) || closed(r)

early ? closed(r) : open(r) implies open(r) || closed(r). It looks as if each from= alternative is checked on its own against the disjunction, and neither alone is implied.

Workaround (and a hint at the fix). Writing the same method as one from-less alternative, @StateRefinement(to = "closed(this)"), verifies. We now generate idempotent close() that way. But it only works when the method is allowed in every state. ServerSocket's accept() is allowed from bound and from accepted but not from unbound, and the same problem comes back with no workaround.

Real-world scenarios

1. close() on the normal path and again in finally (java.io.BufferedReader, where close() is idempotent), with close() specified per state:

   BufferedReader r = new BufferedReader(new StringReader("a\nb"));
   try {
       r.readLine();
       r.close();
   } finally {
       r.close();          // refused: open || closed
   }

2. An accept with a timeout (java.net.ServerSocket, with accept() allowed from="bound(this)", to="accepted(this)" and from="accepted(this)"). This is the standard way to accept with a timeout:

   ServerSocket s = new ServerSocket(0);
   s.setSoTimeout(50);
   try {
       s.accept();
   } catch (IOException timeout) {
       System.out.println("timed out");
   }
   s.close();              // refused: bound || accepted

   An earlier comparison on an older verifier (321a732 / 0.0.33) reported both programs as accepted with this spec. I haven't re-run that version. On 1a506fe and f7f366c both are refused. Rewriting accept() as one alternative from = "bound(this) || accepted(this)" moves the error to close(), which is also written one alternative per state.