Problem (soundness). getMissingStates keeps a state set of this unchanged only if to does not mention that set. A state counts as a mention whatever object it is applied to, so a method that changes another object's state forgets the receiver's state.

import liquidjava.specification.*;

@StateSet({"closed", "opened"})
public class FrameOther {
    @StateRefinement(to = "closed(this)")
    public FrameOther() {}

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

    @StateRefinement(to = "opened(other)")
    public void observe(FrameOther other) {}

    public static void main(String[] args) {
        FrameOther x = new FrameOther();
        FrameOther y = new FrameOther();
        x.observe(y);
        x.close(); // fine only if x is still closed is NOT required; close needs opened(x)
    }
}

This passes verification, but x is still closed when x.close() (from opened) is called. observe's to is opened(other). Because opened appears in it, state1(this) == state1(old(this)) is not added, so x's set is unconstrained after the call.

Fix. A set counts as mentioned only when to constrains it on the post-state receiver, this. That is a state or the set function applied to this, and not to old(this) or another object.

Found while designing #502.