Impact: there is no direct way to say "this call is never allowed". from = "false" should refuse the method in every state. Instead it makes the spec itself an error, even in programs that never call the method.

Minimal reproducer

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

@StateSet({"a", "b"})
class Res {
    @StateRefinement(to = "a(this)")
    public Res() {}

    @StateRefinement(from = "false")
    public void unsupported() {}

    public void fine() {}
}

public class Repro {
    public static void main(String[] args) {
        Res r = new Res();
        r.fine();          // unsupported() is never called
    }
}

Expected: Correct! Passed Verification. A call to unsupported() would then be refused.

Actual (main @ f7f366c, and 1a506fe):

State Conflict Error: Found multiple disjoint states in state transition: state transition can only go to one state of each state set
12 |     @StateRefinement(from = "false")

Real-world scenario. javax.management.modelmbean.RequiredModelMBean.load() and store() always throw MBeanException("Persistence not supported for this MBean") (RequiredModelMBean.java:372-378, 414-420), so a spec should refuse them everywhere. Barista's expert spec allows them, so the bug goes unreported.

Workaround: an int ghost that no call sets, with the constructor setting it to 0 (from = "supported(this) == 1"). It works, but it's an odd thing to have to write.