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

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

    @StateRefinement(from = "open(this)")
    public void read() {}

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

public class Repro {
    static void m() {
        Res a = new Res();
        Res b = a;
        b.close();
        a.read();           // a and b are the same object, now closed
    }
}

Correct! Passed Verification.

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

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

    @StateRefinement(from = "open(this)")
    public void read() {}

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

public class Control {
    static void m() {
        Res a = new Res();
        a.close();
        a.read();           // without the alias: reported
    }
}

State Refinement Error: found closed(a⁸) but expected open(a⁸)
18 |         Res a = new Res();
19 |         a.close();
20 |         a.read();           // without the alias: reported
   |         ^^^^^^^^^
21 |     }