diff --git a/README.md b/README.md
index 4a8093e..44c6c8a 100644
--- a/README.md
+++ b/README.md
@@ -34,6 +34,8 @@ import liquidjava.fsm.StateMachine;
 import liquidjava.fsm.StateMachineParser;
 
 StateMachine stateMachine = StateMachineParser.parse(path.toUri().toString());
+// in a file with several classes, or for a verifier error's StateErrorContext#receiverClass
+StateMachine named = StateMachineParser.parse(path.toUri().toString(), "example.File");
 ```
 
 ### JSON Output
diff --git a/pom.xml b/pom.xml
index 5fd5be2..1c3befd 100644
--- a/pom.xml
+++ b/pom.xml
@@ -44,12 +44,12 @@
     <dependency>
       <groupId>io.github.liquid-java</groupId>
       <artifactId>liquidjava-verifier</artifactId>
-      <version>0.0.35</version>
+      <version>0.0.36</version>
     </dependency>
     <dependency>
       <groupId>fr.inria.gforge.spoon</groupId>
       <artifactId>spoon-core</artifactId>
-      <version>10.4.2</version>
+      <version>11.5.0</version>
     </dependency>
     <dependency>
       <groupId>org.junit.jupiter</groupId>
diff --git a/src/main/java/liquidjava/fsm/StateMachine.java b/src/main/java/liquidjava/fsm/StateMachine.java
index e2a7f60..055344e 100644
--- a/src/main/java/liquidjava/fsm/StateMachine.java
+++ b/src/main/java/liquidjava/fsm/StateMachine.java
@@ -9,6 +9,5 @@ public record StateMachine(
     String className,
     List<String> states,
     List<StateMachineTransition> transitions,
-    List<StateMachineInitialTransition> initialTransitions,
-    StateMachineErrorContext errorContext
+    List<StateMachineInitialTransition> initialTransitions
 ) {}
diff --git a/src/main/java/liquidjava/fsm/StateMachineErrorContext.java b/src/main/java/liquidjava/fsm/StateMachineErrorContext.java
deleted file mode 100644
index 6a76209..0000000
--- a/src/main/java/liquidjava/fsm/StateMachineErrorContext.java
+++ /dev/null
@@ -1,25 +0,0 @@
-package liquidjava.fsm;
-
-import java.util.List;
-
-/**
- * Describes the verification error overlaid on a state machine diagram.
- * @param calledMethod the method, constructor or static factory declared at the error's declaration position
- * @param actualStates the states mentioned by the found condition for the receiver
- * @param receiver the receiver of the failing call (e.g. root)
- * @param expectedStates the states accepted by the expected condition, in state set order
- * @param expectedCondition the expected condition as text
- * @param foundCondition the found condition for the receiver as text
- * @param definiteFoundState the single state the found condition establishes, or null if there is none
- * @param possibleStates the states the found condition allows for the receiver, in state set order
- */
-public record StateMachineErrorContext(
-    String calledMethod,
-    List<String> actualStates,
-    String receiver,
-    List<String> expectedStates,
-    String expectedCondition,
-    String foundCondition,
-    String definiteFoundState,
-    List<String> possibleStates
-) {}
diff --git a/src/main/java/liquidjava/fsm/StateMachineParser.java b/src/main/java/liquidjava/fsm/StateMachineParser.java
index 3b21f35..a9a77ad 100644
--- a/src/main/java/liquidjava/fsm/StateMachineParser.java
+++ b/src/main/java/liquidjava/fsm/StateMachineParser.java
@@ -4,25 +4,18 @@
 import java.nio.file.Paths;
 import java.util.ArrayList;
 import java.util.Collection;
-import java.util.Comparator;
 import java.util.List;
 
 import liquidjava.rj_language.ast.*;
 import liquidjava.rj_language.parsing.RefinementsParser;
-import liquidjava.processor.VCImplication;
-import liquidjava.rj_language.ast.formatter.ExpressionFormatter;
-import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.utils.Utils;
 import spoon.Launcher;
 import spoon.reflect.CtModel;
 import spoon.reflect.declaration.CtAnnotation;
 import spoon.reflect.declaration.CtClass;
-import spoon.reflect.declaration.CtConstructor;
-import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtExecutable;
 import spoon.reflect.declaration.CtMethod;
 import spoon.reflect.declaration.CtType;
-import spoon.reflect.cu.SourcePosition;
 
 public class StateMachineParser {
 
@@ -39,16 +32,16 @@ private record TransitionSource(String from, String cond) {}
      * @return StateMachine or null if none found
      */
     public static StateMachine parse(String uri) {
-        return parse(uri, null, null, null);
+        return parse(uri, null);
     }
 
-    public static StateMachine parseWithErrorContext(String uri, SourcePosition declarationPosition,
-            Expression expectedState, VCImplication foundState) {
-        return parse(uri, declarationPosition, expectedState, foundState);
-    }
-
-    private static StateMachine parse(String uri, SourcePosition declarationPosition,
-            Expression expectedState, VCImplication foundState) {
+    /**
+     * Parses the class or interface with the given name in the given uri, for files that declare several
+     * @param uri the document URI
+     * @param className the qualified class name, or the name given by ExternalRefinementsFor
+     * @return StateMachine or null if none found
+     */
+    public static StateMachine parse(String uri, String className) {
         try {
             String filePath = Paths.get(new URI(uri)).toString();
             Launcher launcher = new Launcher();
@@ -59,7 +52,7 @@ private static StateMachine parse(String uri, SourcePosition declarationPosition
             CtModel model = launcher.getModel();
 
             // get class or interface
-            CtType<?> ctType = getType(model);
+            CtType<?> ctType = getType(model, className);
             if (ctType == null)
                 return null; // no class or interface found
 
@@ -67,8 +60,8 @@ private static StateMachine parse(String uri, SourcePosition declarationPosition
             List<String> states = getStates(ctType);
             if (states == null || states.isEmpty())
                 return null; // no states found
-            String className = getClassName(ctType);
-            String simpleClassName = Utils.getSimpleName(className);
+            String qualifiedName = getClassName(ctType);
+            String simpleClassName = Utils.getSimpleName(qualifiedName);
 
             // get initial transitions and method transitions
             List<StateMachineInitialTransition> factoryTransitions = getFactoryTransitions(ctType, simpleClassName, states);
@@ -83,10 +76,7 @@ private static StateMachine parse(String uri, SourcePosition declarationPosition
             if (transitions.isEmpty())
                 return null; // no transitions found
 
-            StateMachineErrorContext errorContext = declarationPosition == null && expectedState == null
-                    && foundState == null ? null : getErrorContext(ctType, simpleClassName, states,
-                    declarationPosition, expectedState, foundState);
-            return new StateMachine(className, states, transitions, initialTransitions, errorContext);
+            return new StateMachine(qualifiedName, states, transitions, initialTransitions);
 
         } catch (Exception e) {
             e.printStackTrace();
@@ -94,194 +84,15 @@ private static StateMachine parse(String uri, SourcePosition declarationPosition
         }
     }
 
-    private static StateMachineErrorContext getErrorContext(CtType<?> ctType, String className, List<String> states,
-            SourcePosition declarationPosition, Expression expectedState, VCImplication foundState) {
-        String receiver = getStateReceiver(expectedState, states);
-        String receiverName = receiver == null ? null : VariableFormatter.withoutInstance(receiver);
-        List<Expression> foundPremises = getReceiverPremises(foundState, receiver);
-        return new StateMachineErrorContext(
-                getCalledMethod(ctType, className, declarationPosition),
-                getActualStates(expectedState, foundState, states),
-                receiverName,
-                getExpectedStates(expectedState, states, receiver),
-                expectedState == null ? null : formatCondition(expectedState, receiver, receiverName),
-                getFoundCondition(foundState, foundPremises, receiver, receiverName),
-                getDefiniteState(foundPremises, states, receiver),
-                getPossibleStates(foundPremises, states, receiver));
-    }
-
-    /**
-     * Gets the name of the method, constructor or static factory whose declaration contains the given position
-     * The verifier reports the position of the state refinement annotation value, so the position is matched by range
-     * Constructors are named after the class
-     */
-    private static String getCalledMethod(CtType<?> ctType, String className, SourcePosition declarationPosition) {
-        if (declarationPosition == null || !declarationPosition.isValidPosition()) return null;
-        List<CtExecutable<?>> executables = new ArrayList<>(ctType.getMethods());
-        if (ctType instanceof CtClass<?> ctClass) {
-            executables.addAll(ctClass.getConstructors());
-        }
-        return executables.stream()
-                .filter(executable -> contains(executable.getPosition(), declarationPosition))
-                .min(Comparator.comparingInt(executable -> executable.getPosition().getSourceEnd()
-                        - executable.getPosition().getSourceStart()))
-                .map(executable -> executable instanceof CtConstructor<?> ? className : executable.getSimpleName())
-                .orElse(null);
-    }
-
-    private static boolean contains(SourcePosition outer, SourcePosition inner) {
-        return outer.isValidPosition()
-                && outer.getFile() != null && inner.getFile() != null
-                && outer.getFile().toPath().toAbsolutePath().normalize()
-                        .equals(inner.getFile().toPath().toAbsolutePath().normalize())
-                && outer.getSourceStart() <= inner.getSourceStart()
-                && inner.getSourceEnd() <= outer.getSourceEnd();
-    }
-
-    private static List<String> getActualStates(Expression expectedState, VCImplication foundState,
-            List<String> states) {
-        String receiver = getStateReceiver(expectedState, states);
-        if (receiver == null || foundState == null) return List.of();
-
-        List<String> foundStates = new ArrayList<>();
-        for (VCImplication premise = foundState; premise != null; premise = premise.getNext()) {
-            if (premise.hasBinder() && receiver.equals(premise.getName()) && premise.getRefinement() != null) {
-                foundStates.addAll(getStateExpressions(premise.getRefinement().getExpression(), states, receiver));
-            }
-        }
-        return states.stream().filter(foundStates::contains).toList();
-    }
-
-    /**
-     * Gets the states accepted by the expected condition for the receiver, in state set order
-     */
-    private static List<String> getExpectedStates(Expression expectedState, List<String> states, String receiver) {
-        if (expectedState == null || receiver == null) return List.of();
-        List<String> expectedStates = getStateExpressions(expectedState, states, receiver);
-        return states.stream().filter(expectedStates::contains).toList();
-    }
-
-    /**
-     * Gets the found premises about the receiver: those bound to it and unbound ones that mention it
-     */
-    private static List<Expression> getReceiverPremises(VCImplication foundState, String receiver) {
-        List<Expression> premises = new ArrayList<>();
-        if (receiver == null) return premises;
-        for (VCImplication premise = foundState; premise != null; premise = premise.getNext()) {
-            if (premise.getRefinement() == null) continue;
-            Expression expr = premise.getRefinement().getExpression();
-            boolean bound = premise.hasBinder() && receiver.equals(premise.getName());
-            boolean mentioned = !premise.hasBinder() && premise.getRefinement().getVariableNames().contains(receiver);
-            if ((bound || mentioned) && !expr.isBooleanTrue()) {
-                premises.add(expr);
-            }
-        }
-        return premises;
-    }
-
-    private static String getFoundCondition(VCImplication foundState, List<Expression> foundPremises,
-            String receiver, String receiverName) {
-        if (foundState == null) return null;
-        if (receiver == null) return ExpressionFormatter.format(foundState.toPredicate().getExpression());
-        return formatCondition(joinConjunction(foundPremises), receiver, receiverName);
-    }
-
-    private static Expression joinConjunction(List<Expression> exprs) {
-        Expression conjunction = null;
-        for (Expression expr : exprs) {
-            conjunction = conjunction == null ? expr : new BinaryExpression(conjunction, "&&", expr);
-        }
-        return conjunction == null ? new LiteralBoolean(true) : conjunction;
-    }
-
     /**
-     * Formats a condition for display, showing the receiver by its source name (e.g. root instead of root¹⁷)
-     */
-    private static String formatCondition(Expression expr, String receiver, String receiverName) {
-        if (receiver != null && receiverName != null) {
-            expr = expr.substitute(new Var(receiver), new Var(receiverName));
-        }
-        return ExpressionFormatter.format(expr);
-    }
-
-    /**
-     * Gets the single state the found premises establish for the receiver, or null if there is none
-     * A state is established only when it is a top-level conjunct; any other conjunct about the receiver's
-     * states (disjunction, conditional, ...) makes the result null, except negations of other states.
-     * Negations alone never establish a state since the verifier does not bound the state set
-     */
-    private static String getDefiniteState(List<Expression> premises, List<String> states, String receiver) {
-        if (receiver == null) return null;
-        List<String> found = new ArrayList<>();
-        List<String> excluded = new ArrayList<>();
-        for (Expression premise : premises) {
-            for (Expression conjunct : premise.getConjuncts()) {
-                String state = getReceiverState(conjunct, states, receiver);
-                String negated = conjunct instanceof UnaryExpression unary && unary.getOp().equals("!")
-                        ? getReceiverState(unary.getExpression(), states, receiver) : null;
-                if (state != null) {
-                    if (!found.contains(state)) found.add(state);
-                } else if (negated != null) {
-                    excluded.add(negated);
-                } else if (mentionsReceiverState(conjunct, states, receiver)) {
-                    return null;
-                }
-            }
-        }
-        if (found.size() != 1 || excluded.contains(found.get(0))) return null;
-        return found.get(0);
-    }
-
-    /**
-     * Gets the states the found premises allow for the receiver, in state set order
-     * Each conjunct about the receiver's states is evaluated like the expected condition and the results are
-     * intersected; conjuncts that do not mention the receiver's states do not restrict it
-     */
-    private static List<String> getPossibleStates(List<Expression> premises, List<String> states, String receiver) {
-        if (receiver == null) return List.of();
-        List<String> possible = new ArrayList<>(states);
-        for (Expression premise : premises) {
-            for (Expression conjunct : premise.getConjuncts()) {
-                if (mentionsReceiverState(conjunct, states, receiver)) {
-                    possible.retainAll(getStateExpressions(conjunct, states, receiver));
-                }
-            }
-        }
-        return List.copyOf(possible);
-    }
-
-    private static String getReceiverState(Expression expr, List<String> states, String receiver) {
-        return expr instanceof FunctionInvocation ? getStateName(expr, states, receiver) : null;
-    }
-
-    private static boolean mentionsReceiverState(Expression expr, List<String> states, String receiver) {
-        if (getReceiverState(expr, states, receiver) != null) return true;
-        return expr.getChildren().stream().anyMatch(child -> mentionsReceiverState(child, states, receiver));
-    }
-
-    private static String getStateReceiver(Expression expr, List<String> states) {
-        if (expr == null) return null;
-        if (expr instanceof FunctionInvocation invocation
-                && findState(invocation.getName(), states) != null
-                && !invocation.getArgs().isEmpty()
-                && invocation.getArgs().get(0) instanceof Var receiver) {
-            return receiver.getName();
-        }
-        for (Expression child : expr.getChildren()) {
-            String receiver = getStateReceiver(child, states);
-            if (receiver != null) return receiver;
-        }
-        return null;
-    }
-
-    /**
-     * Finds the first class or interface in the model (we assume only one per file)
+     * Finds the class or interface in the model with the given name, or the first one if the name is null
      * @param model the CtModel
+     * @param className the qualified class name, or null
      * @return CtType or null if none found
      */
-    private static CtType<?> getType(CtModel model) {
+    private static CtType<?> getType(CtModel model, String className) {
         for (CtType<?> type : model.getAllTypes()) {
-            if (type.isClass() || type.isInterface())
+            if ((type.isClass() || type.isInterface()) && (className == null || className.equals(getClassName(type))))
                 return type;
         }
         return null;
@@ -625,21 +436,17 @@ private static List<TransitionSource> getStateSources(Expression expr, List<Stri
      * @return list of states
      */
     private static List<String> getStateExpressions(Expression expr, List<String> states) {
-        return getStateExpressions(expr, states, null);
-    }
-
-    private static List<String> getStateExpressions(Expression expr, List<String> states, String receiver) {
         List<String> stateExpressions = new ArrayList<>();
-        String state = getStateName(expr, states, receiver);
+        String state = getStateName(expr, states);
         if (state != null) {
             stateExpressions.add(state);
         } else if (expr instanceof BinaryExpression bin) {
-            stateExpressions.addAll(getStateExpressions(bin.getFirstOperand(), states, receiver));
-            stateExpressions.addAll(getStateExpressions(bin.getSecondOperand(), states, receiver));
+            stateExpressions.addAll(getStateExpressions(bin.getFirstOperand(), states));
+            stateExpressions.addAll(getStateExpressions(bin.getSecondOperand(), states));
         } else if (expr instanceof UnaryExpression unary) {
             if (unary.getOp().equals("!")) {
                 // all except those in the expression
-                List<String> negatedStates = getStateExpressions(unary.getExpression(), states, receiver);
+                List<String> negatedStates = getStateExpressions(unary.getExpression(), states);
                 if (!negatedStates.isEmpty()) {
                     for (String possibleState : states) {
                         if (!negatedStates.contains(possibleState)) {
@@ -650,27 +457,17 @@ private static List<String> getStateExpressions(Expression expr, List<String> st
             }
         } else if (expr instanceof Ite ite) {
             // combine states from then and else branches
-            stateExpressions.addAll(getStateExpressions(ite.getThen(), states, receiver));
-            stateExpressions.addAll(getStateExpressions(ite.getElse(), states, receiver));
+            stateExpressions.addAll(getStateExpressions(ite.getThen(), states));
+            stateExpressions.addAll(getStateExpressions(ite.getElse(), states));
         }
         return stateExpressions;
     }
 
     private static String getStateName(Expression expr, List<String> states) {
-        return getStateName(expr, states, null);
-    }
-
-    private static String getStateName(Expression expr, List<String> states, String receiver) {
         if (expr instanceof Var var) {
             return findState(var.getName(), states);
         } else if (expr instanceof FunctionInvocation func) {
-            String state = findState(func.getName(), states);
-            if (state == null || receiver == null) return state;
-            if (!func.getArgs().isEmpty()
-                    && func.getArgs().get(0) instanceof Var target
-                    && receiver.equals(target.getName())) {
-                return state;
-            }
+            return findState(func.getName(), states);
         }
         return null;
     }
diff --git a/src/test/java/liquidjava/fsm/StateMachineParserTests.java b/src/test/java/liquidjava/fsm/StateMachineParserTests.java
index 631eda8..c346dd1 100644
--- a/src/test/java/liquidjava/fsm/StateMachineParserTests.java
+++ b/src/test/java/liquidjava/fsm/StateMachineParserTests.java
@@ -1,27 +1,21 @@
 package liquidjava.fsm;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertNotNull;
 import static org.junit.jupiter.api.Assertions.assertNull;
+import static org.junit.jupiter.api.Assertions.assertTrue;
 
-import java.io.File;
 import java.nio.file.Path;
+import java.util.ArrayList;
 import java.util.List;
 
 import org.junit.jupiter.api.Test;
 
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.Diagnostics;
+import liquidjava.diagnostics.errors.StateErrorContext;
 import liquidjava.diagnostics.errors.StateRefinementError;
-import liquidjava.processor.VCImplication;
-import liquidjava.rj_language.Predicate;
-import liquidjava.rj_language.parsing.RefinementsParser;
-import spoon.Launcher;
-import spoon.reflect.cu.SourcePosition;
-import spoon.reflect.declaration.CtClass;
-import spoon.reflect.declaration.CtType;
-import spoon.reflect.reference.CtTypeReference;
-
-import static org.junit.jupiter.api.Assertions.assertNotNull;
 
 public class StateMachineParserTests {
 
@@ -39,17 +33,6 @@ public void testSimpleStateMachine() {
                         new StateMachineTransition("open", "open", "read")),
                 List.of(new StateMachineInitialTransition("open")));
         assertStateMachineEquals(expectedSm, sm);
-        assertNull(sm.errorContext(), "Plain state machines should not contain diagnostic context");
-    }
-
-    @Test
-    public void testStateMachineGroupsErrorContext() {
-        StateMachineErrorContext errorContext = new StateMachineErrorContext(
-                "read", List.of("closed"), "file", List.of("open"), "open(file)", "closed(file)", "closed",
-                List.of("closed"));
-        StateMachine sm = new StateMachine("Simple", List.of("open", "closed"), List.of(), List.of(), errorContext);
-
-        assertEquals(errorContext, sm.errorContext());
     }
 
     @Test
@@ -282,158 +265,36 @@ public void testExternalFactoryWithoutConstructorHasNoDefaultInitialState() {
     }
 
     @Test
-    public void testErrorContextForRejectedCall() {
-        // root.getFirstChild() after add and removeAllChildren
-        StateRefinementError error = verifyStateError("errors/tree", "root");
-        StateMachine sm = parseWithErrorContext(error);
-        assertNotNull(sm);
-        assertEquals(new StateMachineErrorContext("getFirstChild", List.of("childrenAllowed"), "root",
-                List.of("maybeHasChildren"), "maybeHasChildren(root)", "childrenAllowed(root)", "childrenAllowed",
-                List.of("childrenAllowed")),
-                sm.errorContext());
-    }
-
-    @Test
-    public void testErrorContextForPreconditionWithMultipleStates() {
-        StateRefinementError error = verifyStateError("errors/door", "twice");
-        assertEquals(new StateMachineErrorContext("lock", List.of("locked"), "twice", List.of("open", "closed"),
-                "open(twice) || closed(twice)", "locked(twice)", "locked", List.of("locked")),
-                parseWithErrorContext(error).errorContext());
-    }
-
-    @Test
-    public void testErrorContextForNegatedPrecondition() {
-        StateRefinementError error = verifyStateError("errors/door", "pushed");
-        assertEquals(new StateMachineErrorContext("push", List.of("locked"), "pushed", List.of("open", "closed"),
-                "!locked(pushed)", "locked(pushed)", "locked", List.of("locked")),
-                parseWithErrorContext(error).errorContext());
-    }
-
-    @Test
-    public void testErrorContextWithoutDefiniteFoundState() {
-        // found flag ? open(unknown) : closed(unknown) does not establish one state
-        StateRefinementError error = verifyStateError("errors/door", "unknown");
-        assertEquals(new StateMachineErrorContext("unlock", List.of("open", "closed"), "unknown",
-                List.of("locked"), "locked(unknown)", "flag ? open(unknown) : closed(unknown)", null,
-                List.of("open", "closed")),
-                parseWithErrorContext(error).errorContext());
-    }
-
-    @Test
-    public void testErrorContextForStateFromBranches() {
-        // socket.receive after closing the socket on one branch and sending on the other
-        StateRefinementError error = verifyStateError("errors/udp", "socket");
-        StateMachineErrorContext errorContext = parseWithErrorContext(error).errorContext();
-        assertEquals("receive", errorContext.calledMethod());
-        assertEquals("socket", errorContext.receiver());
-        assertEquals(List.of("unbound", "bound", "connected"), errorContext.expectedStates());
-        assertEquals(List.of("bound", "closed"), errorContext.possibleStates());
-        assertNull(errorContext.definiteFoundState());
-    }
-
-    @Test
-    public void testPossibleStates() {
-        String doorUri = uri("errors/door/Door.java");
-        assertEquals(List.of("open"), possibleStates(doorUri, "open(d)"));
-        assertEquals(List.of("open"), possibleStates(doorUri, "open(d) && !locked(d)"));
-        assertEquals(List.of("open"), possibleStates(doorUri, "open(d) && (closed(e) || locked(e))"));
-        assertEquals(List.of("open", "closed"), possibleStates(doorUri, "closed(d) || open(d)"));
-        assertEquals(List.of("open", "closed"), possibleStates(doorUri, "flag ? open(d) : closed(d)"));
-        assertEquals(List.of("open", "locked"), possibleStates(doorUri, "!closed(d)"));
-        assertEquals(List.of("closed"), possibleStates(doorUri, "!open(d) && !locked(d)"));
-        assertEquals(List.of("closed"), possibleStates(doorUri, "!(open(d) || locked(d))"));
-        assertEquals(List.of("open"), possibleStates(doorUri, "open(d) && (open(d) || closed(d))"));
-        assertEquals(List.of(), possibleStates(doorUri, "open(d) && closed(d)"));
-        assertEquals(List.of(), possibleStates(doorUri, "open(d) && !open(d)"));
-        assertEquals(List.of("open", "closed", "locked"), possibleStates(doorUri, "open(e)"));
-        assertEquals(List.of("open", "closed", "locked"), possibleStates(doorUri, "x > 0"));
-        assertEquals(List.of("open", "closed", "locked"), possibleStates(doorUri, "true"));
-    }
-
-    @Test
-    public void testNegatedFoundExcludesState() {
-        CtTypeReference<?> doorType = new Launcher().getFactory().Type().createReference("fsm.errors.door.Door");
-        VCImplication found = new VCImplication("#s_4", doorType, predicate("!closed(#s_4)"));
-        StateMachineErrorContext errorContext = StateMachineParser.parseWithErrorContext(
-                uri("errors/door/Door.java"), null, RefinementsParser.createAST("closed(#s_4)", ""), found)
-                .errorContext();
-        assertEquals(List.of("open", "locked"), errorContext.possibleStates());
-    }
-
-    @Test
-    public void testPossibleStatesWithoutReceiver() {
-        CtTypeReference<?> doorType = new Launcher().getFactory().Type().createReference("fsm.errors.door.Door");
-        VCImplication found = new VCImplication("d", doorType, predicate("open(d)"));
-        assertEquals(List.of(), StateMachineParser.parseWithErrorContext(uri("errors/door/Door.java"), null,
-                RefinementsParser.createAST("x > 0", ""), found).errorContext().possibleStates());
-    }
-
-    @Test
-    public void testPossibleStatesMatchDefiniteFoundState() {
-        String doorUri = uri("errors/door/Door.java");
-        for (String found : List.of("open(d)", "open(d) && !locked(d)", "open(d) && open(e)",
-                "open(d) && (closed(e) || locked(e))", "open(d) || closed(d)", "flag ? open(d) : closed(d)",
-                "!locked(d)", "!open(d) && !locked(d)", "!(open(d) || locked(d))", "open(d) && closed(d)",
-                "open(d) && !open(d)", "open(d) && (open(d) || closed(d))", "open(e)", "true")) {
-            StateMachineErrorContext errorContext = errorContext(doorUri, found);
-            if (errorContext.definiteFoundState() != null) {
-                assertEquals(List.of(errorContext.definiteFoundState()), errorContext.possibleStates(), found);
+    public void testClassSelectedByName() {
+        StateMachine sm = StateMachineParser.parse(uri("TwoStateClasses.java"), "fsm.Second");
+        assertStateMachineEquals(stateMachine("Second", List.of("idle", "busy"),
+                List.of(new StateMachineTransition("idle", "busy", "start")),
+                List.of(new StateMachineInitialTransition("idle"))), sm);
+        assertEquals("fsm.TwoStateClasses", StateMachineParser.parse(uri("TwoStateClasses.java")).className());
+        assertNull(StateMachineParser.parse(uri("TwoStateClasses.java"), "fsm.Missing"));
+    }
+
+    @Test
+    public void testVerifierStatesAreStatesOfTheDiagram() {
+        for (String directory : List.of("errors/door", "errors/tree", "errors/udp")) {
+            List<StateRefinementError> errors = stateErrors(directory);
+            assertFalse(errors.isEmpty(), "Expected state refinement errors in " + directory);
+            for (StateRefinementError error : errors) {
+                StateErrorContext context = error.getContext();
+                assertNotNull(context, "Expected the verifier's states for " + error.getMessage());
+                StateMachine sm = StateMachineParser.parse(error.getDeclarationPosition().getFile().toURI().toString(),
+                        context.receiverClass());
+                assertNotNull(sm, "Expected a diagram of " + context.receiverClass());
+                List<List<String>> verifierStates = new ArrayList<>(context.possibleStates());
+                if (context.acceptedStates() != null)
+                    verifierStates.addAll(context.acceptedStates());
+                // the diagram shows the first state set
+                for (List<String> state : verifierStates)
+                    assertTrue(sm.states().contains(state.get(0)), state.get(0) + " is not in " + sm.states());
             }
         }
     }
 
-    @Test
-    public void testDefiniteFoundState() {
-        String doorUri = uri("errors/door/Door.java");
-        assertEquals("open", definiteFoundState(doorUri, "open(d)"));
-        assertEquals("open", definiteFoundState(doorUri, "open(d) && !locked(d)"));
-        assertEquals("open", definiteFoundState(doorUri, "open(d) && open(e)"));
-        assertEquals("open", definiteFoundState(doorUri, "open(d) && (closed(e) || locked(e))"));
-        assertNull(definiteFoundState(doorUri, "open(d) || closed(d)"));
-        assertNull(definiteFoundState(doorUri, "flag ? open(d) : closed(d)"));
-        assertNull(definiteFoundState(doorUri, "!locked(d)"));
-        assertNull(definiteFoundState(doorUri, "!open(d) && !locked(d)"));
-        assertNull(definiteFoundState(doorUri, "!(open(d) || locked(d))"));
-        assertNull(definiteFoundState(doorUri, "open(d) && closed(d)"));
-        assertNull(definiteFoundState(doorUri, "open(d) && !open(d)"));
-        assertNull(definiteFoundState(doorUri, "open(d) && (open(d) || closed(d))"));
-        assertNull(definiteFoundState(doorUri, "open(e)"));
-        assertNull(definiteFoundState(doorUri, "true"));
-    }
-
-    @Test
-    public void testFoundConditionIsRestrictedToReceiver() {
-        CtTypeReference<?> doorType = new Launcher().getFactory().Type().createReference("fsm.errors.door.Door");
-        VCImplication other = new VCImplication("#e_2", doorType, predicate("closed(#e_2)"));
-        VCImplication receiver = new VCImplication("#d_3", doorType, predicate("open(#d_3) && x > 0"));
-        other.setNext(receiver);
-        StateMachineErrorContext errorContext = StateMachineParser.parseWithErrorContext(
-                uri("errors/door/Door.java"), null, RefinementsParser.createAST("locked(#d_3)", ""), other)
-                .errorContext();
-        assertEquals(new StateMachineErrorContext(null, List.of("open"), "d", List.of("locked"), "locked(d)",
-                "open(d) && x > 0", "open", List.of("open")), errorContext);
-    }
-
-    @Test
-    public void testCalledConstructorAndStaticFactory() {
-        CtClass<?> staticFactory = (CtClass<?>) buildType("StaticFactory.java");
-        assertEquals("StaticFactory", calledMethod("StaticFactory.java",
-                staticFactory.getConstructors().iterator().next().getPosition()));
-        assertEquals("of", calledMethod("StaticFactory.java",
-                staticFactory.getMethodsByName("of").get(0).getPosition()));
-        assertEquals("close", calledMethod("StaticFactory.java",
-                staticFactory.getMethodsByName("close").get(0).getPosition()));
-
-        // interfaces declare constructors as methods named after the class
-        CtType<?> refinements = buildType("errors/tree/DefaultMutableTreeNodeRefinements.java");
-        assertEquals("DefaultMutableTreeNode", calledMethod("errors/tree/DefaultMutableTreeNodeRefinements.java",
-                refinements.getMethodsByName("DefaultMutableTreeNode").get(0).getPosition()));
-
-        // positions outside the state machine's type resolve to no method
-        assertNull(calledMethod("errors/tree/DefaultMutableTreeNodeRefinements.java",
-                staticFactory.getMethodsByName("close").get(0).getPosition()));
-    }
-
     private static void assertStateMachineEquals(StateMachine expected, StateMachine actual) {
         assertNotNull(actual, "State machine should not be null");
         assertEquals(expected.className(), actual.className(), "Class names should match");
@@ -442,61 +303,19 @@ private static void assertStateMachineEquals(StateMachine expected, StateMachine
                 .toList(), "Initial transitions should match");
         assertEquals(expected.states(), actual.states(), "States should match");
         assertEquals(expected.transitions(), actual.transitions(), "State transitions should match");
-        assertEquals(expected.errorContext(), actual.errorContext(), "Error contexts should match");
     }
 
     private static StateMachine stateMachine(String className, List<String> states,
             List<StateMachineTransition> transitions, List<StateMachineInitialTransition> initialTransitions) {
         String qualifiedName = className.contains(".") ? className : "fsm." + className;
-        return new StateMachine(qualifiedName, states, transitions, initialTransitions, null);
+        return new StateMachine(qualifiedName, states, transitions, initialTransitions);
     }
 
-    private static StateRefinementError verifyStateError(String directory, String receiver) {
+    private static List<StateRefinementError> stateErrors(String directory) {
         CommandLineLauncher.launch(BASE_PATH.resolve(directory).toAbsolutePath().toString());
         return Diagnostics.getInstance().getErrors().stream()
                 .filter(StateRefinementError.class::isInstance)
                 .map(StateRefinementError.class::cast)
-                .filter(error -> error.getFound().toString().contains("#" + receiver + "_"))
-                .findFirst()
-                .orElseThrow(() -> new AssertionError("No state refinement error found for " + receiver));
-    }
-
-    // same arguments as the vscode-liquidjava server
-    private static StateMachine parseWithErrorContext(StateRefinementError error) {
-        return StateMachineParser.parseWithErrorContext(
-                new File(error.getDeclarationPosition().getFile().getPath()).toURI().toString(),
-                error.getDeclarationPosition(), error.getExpected().getExpression(), error.getFound());
-    }
-
-    private static StateMachineErrorContext errorContext(String uri, String found) {
-        CtTypeReference<?> doorType = new Launcher().getFactory().Type().createReference("fsm.errors.door.Door");
-        VCImplication foundState = new VCImplication("d", doorType, predicate(found));
-        return StateMachineParser.parseWithErrorContext(uri, null, RefinementsParser.createAST("locked(d)", ""),
-                foundState).errorContext();
-    }
-
-    private static String definiteFoundState(String uri, String found) {
-        return errorContext(uri, found).definiteFoundState();
-    }
-
-    private static List<String> possibleStates(String uri, String found) {
-        return errorContext(uri, found).possibleStates();
-    }
-
-    private static Predicate predicate(String expr) {
-        return new Predicate(RefinementsParser.createAST(expr, ""));
-    }
-
-    private static String calledMethod(String file, SourcePosition declarationPosition) {
-        return StateMachineParser.parseWithErrorContext(uri(file), declarationPosition, null, null)
-                .errorContext().calledMethod();
-    }
-
-    private static CtType<?> buildType(String file) {
-        Launcher launcher = new Launcher();
-        launcher.getEnvironment().setNoClasspath(true);
-        launcher.addInputResource(BASE_PATH.resolve(file).toAbsolutePath().toString());
-        launcher.buildModel();
-        return launcher.getModel().getAllTypes().iterator().next();
+                .toList();
     }
 }
diff --git a/src/test/resources/fsm/TwoStateClasses.java b/src/test/resources/fsm/TwoStateClasses.java
new file mode 100644
index 0000000..c83e93a
--- /dev/null
+++ b/src/test/resources/fsm/TwoStateClasses.java
@@ -0,0 +1,18 @@
+package fsm;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"open", "closed"})
+public class TwoStateClasses {
+
+    @StateRefinement(from="open(this)", to="closed(this)")
+    public void close() {}
+}
+
+@StateSet({"idle", "busy"})
+class Second {
+
+    @StateRefinement(from="idle(this)", to="busy(this)")
+    public void start() {}
+}
diff --git a/src/test/resources/fsm/errors/udp/DatagramSocketRefinementsExpert.java b/src/test/resources/fsm/errors/udp/DatagramSocketRefinementsExpert.java
index 64acf97..b9ed2ca 100644
--- a/src/test/resources/fsm/errors/udp/DatagramSocketRefinementsExpert.java
+++ b/src/test/resources/fsm/errors/udp/DatagramSocketRefinementsExpert.java
@@ -47,16 +47,13 @@ public interface DatagramSocketRefinementsExpert {
 	void disconnect();
 
 	@StateRefinement(from = "connected(this)")
-	@StateRefinement(from = "closed(this) && connected(old(this))")
 	InetAddress getInetAddress();
 
 	@StateRefinement(from = "connected(this)")
-	@StateRefinement(from = "closed(this) && connected(old(this))")
 	@Refinement("Port(_) || _ == -1")
 	int getPort();
 
 	@StateRefinement(from = "connected(this)")
-	@StateRefinement(from = "closed(this) && connected(old(this))")
 	SocketAddress getRemoteSocketAddress();
 
 	@StateRefinement(from = "bound(this)")