@@ -18,6 +18,7 @@
 import liquidjava.processor.state_machine.DecidingArgument;
 import liquidjava.processor.state_machine.State;
 import liquidjava.processor.state_machine.StateMachine;
+import liquidjava.rj_language.Predicate;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Keys;
 import spoon.reflect.reference.CtExecutableReference;
@@ -141,7 +142,10 @@ private List<Hint> howToReach(Set<State> current, RefinedFunction call, String f
      */
     private List<Hint> guard(Set<State> current, RefinedFunction call) {
         List<CallVariant> guards = new ArrayList<>();
+        boolean anyCombination = anyCombination(current);
         for (CallVariant guard : machine.guards()) {
+            if (anyCombination && !namesCheckedState(guard.method()))
+                continue;
             if (!machine.allows(current, guard))
                 continue;
             Set<State> reached = machine.after(current, guard);
@@ -158,6 +162,33 @@ private List<Hint> guard(Set<State> current, RefinedFunction call) {
         return List.of(new Hint(Kind.GUARD, message));
     }
 
+    /**
+     * Whether the receiver can be in any combination of the states {@code current} has in each state set. Then a call
+     * that names no state of the sets the failing call checks leaves them as they were, whatever it returns, so the
+     * failing call stays disallowed after it
+     */
+    private boolean anyCombination(Set<State> current) {
+        long combinations = 1;
+        for (int set = 0; set < current.iterator().next().names().size(); set++) {
+            int index = set;
+            combinations *= current.stream().map(s -> s.names().get(index)).distinct().count();
+        }
+        return combinations == current.size();
+    }
+
+    /**
+     * Whether a state refinement or the return refinement of {@code method} names a state of a set the failing call
+     * checks, or an alias
+     */
+    private boolean namesCheckedState(RefinedFunction method) {
+        Set<String> checked = machine.states().stream().flatMap(s -> checkedSets.stream().map(s.names()::get))
+                .collect(Collectors.toSet());
+        Stream<Predicate> refinements = Stream.concat(
+                method.getAllStates().stream().flatMap(o -> Stream.of(o.getFrom(), o.getTo())),
+                Stream.ofNullable(method.getRefReturn()));
+        return refinements.anyMatch(p -> StateMachine.mayName(p, checked));
+    }
+
     private Hint callSequence(Set<State> current, List<CallVariant> sequence, String from) {
         Set<State> reached = current;
         for (CallVariant step : sequence)
 
@@ -2,6 +2,8 @@
 
 import java.util.ArrayList;
 import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Map;
 import java.util.Optional;
@@ -56,8 +58,14 @@ record Scope(TypeChecker tc, StateSolver solver, List<State> states, List<List<S
     /** The effects with any arguments, whose entries a condition on the result does not change, or null */
     private final CallVariant.Effects any;
 
-    private final Map<Integer, Map<State, CallVariant.Entry>> entries = new HashMap<>();
+    /** By state refinement, then by the states before the call in the state sets its {@code from} names */
+    private final Map<Integer, Map<List<String>, CallVariant.Entry>> entries = new HashMap<>();
     private final Map<Integer, Map<State, Optional<Set<State>>>> afters = new HashMap<>();
+    /**
+     * By state refinement, then by the states before the call in the sets its {@code to} names for {@code old(this)}:
+     * the states it can lead to in the sets it names
+     */
+    private final Map<Integer, Map<List<String>, Set<List<String>>>> reachedBefore = new HashMap<>();
 
     /**
      * @param changes
@@ -99,13 +107,17 @@ public CallVariant.Entry entry(int index, State state) {
             return CallVariant.Entry.HOLDS; // no state refinement: allowed in every state
         if (onResult && any != null)
             return any.entry(index, state); // the result is not known before the call
-        return entries.computeIfAbsent(index, i -> new HashMap<>()).computeIfAbsent(state, s -> {
+        // the states of the other sets are about other ghost functions, so they cannot change the answer
+        Predicate from = changes.get(index).getFrom();
+        List<String> named = namedSets(from).stream().map(state.names()::get).toList();
+        return entries.computeIfAbsent(index, i -> new HashMap<>()).computeIfAbsent(named, n -> {
             Optional<CallVariant.Entry> entry = withScope(() -> {
-                Predicate before = before(s);
-                Predicate from = changes.get(index).getFrom().substituteVariable(Keys.THIS, BEFORE);
-                if (scope.solver().implies(before, from))
+                Predicate before = before(state);
+                Predicate fromBefore = from.substituteVariable(Keys.THIS, BEFORE);
+                if (scope.solver().implies(before, fromBefore))
                     return CallVariant.Entry.HOLDS;
-                return scope.solver().compatible(before, from) ? CallVariant.Entry.UNDECIDED : CallVariant.Entry.FAILS;
+                return scope.solver().compatible(before, fromBefore) ? CallVariant.Entry.UNDECIDED
+                        : CallVariant.Entry.FAILS;
             });
             return entry.orElse(CallVariant.Entry.UNDECIDED);
         });
@@ -133,11 +145,23 @@ private Optional<Set<State>> computeAfter(int index, State state, Set<State> can
             ObjectState change = changes.get(index);
             if (!change.hasTo())
                 return Set.of(s);
-            Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER);
-            Predicate known = Predicate.createConjunction(before(s), to);
-            if (onResult)
-                known = Predicate.createConjunction(known, condition);
-            Set<State> next = possibleStates(candidates, known, AFTER);
+            List<Integer> named = namedSets(change.getTo()).stream().sorted().toList();
+            Set<State> kept = Set.copyOf(StateMachine.keeping(candidates, s, Set.copyOf(named)));
+            // where it leads in the sets it names depends only on the state before in those it names for old(this)
+            List<String> before = StateMachine.namedSetsBefore(change.getTo(), scope.stateSets()).stream().sorted()
+                    .map(s.names()::get).toList();
+            Map<List<String>, Set<List<String>>> reached = reachedBefore.computeIfAbsent(index, i -> new HashMap<>());
+            if (!reached.containsKey(before)) {
+                Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER);
+                Predicate known = Predicate.createConjunction(before(s), to);
+                if (onResult)
+                    known = Predicate.createConjunction(known, condition);
+                reached.put(before, possibleStates(kept, known, AFTER).stream()
+                        .map(c -> named.stream().map(c.names()::get).toList()).collect(Collectors.toSet()));
+            }
+            Set<State> next = scope.states().stream().filter(kept::contains)
+                    .filter(c -> reached.get(before).contains(named.stream().map(c.names()::get).toList()))
+                    .collect(Collectors.toCollection(LinkedHashSet::new));
             // no state at all: the condition contradicts the refinement here, so nothing can be claimed
             return next.isEmpty() && !onResult ? null : next;
         });
@@ -171,6 +195,13 @@ private Set<State> possibleStates(Set<State> candidates, Predicate known, String
         return scope.solver().possibleStates(combined, known, variable);
     }
 
+    /** The state sets that {@code predicate} or this variant's condition may name a state of */
+    private Set<Integer> namedSets(Predicate predicate) {
+        Set<Integer> named = new HashSet<>(StateMachine.namedSets(predicate, scope.stateSets()));
+        named.addAll(StateMachine.namedSets(condition, scope.stateSets()));
+        return named;
+    }
+
     /** What is known before the call in {@code state} */
     private Predicate before(State state) {
         Predicate before = state.predicate().substituteVariable(Keys.THIS, BEFORE);
 
@@ -11,10 +11,16 @@
 import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
+import java.util.stream.IntStream;
 
 import liquidjava.processor.context.ObjectState;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.AliasInvocation;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.utils.Utils;
+import liquidjava.utils.constants.Keys;
 
 /**
  * The typestate of a class as a finite state machine, built by {@link StateMachineBuilder}
@@ -256,6 +262,60 @@ public Set<State> ordered(Collection<State> subset) {
         return states.stream().filter(subset::contains).collect(Collectors.toCollection(LinkedHashSet::new));
     }
 
+    /**
+     * Whether {@code predicate} names one of {@code states}, by its simple name, or calls an alias, which may name one
+     * that cannot be seen without expanding it
+     */
+    public static boolean mayName(Predicate predicate, Set<String> states) {
+        return mayName(predicate.getExpression(), states, false);
+    }
+
+    /**
+     * The state sets, as indexes into {@link State#names()}, that {@code predicate} {@link #mayName may name} a state
+     * of
+     *
+     * @param stateSets
+     *            the states of each state set on its own, in the order the sets are declared
+     */
+    static Set<Integer> namedSets(Predicate predicate, List<List<State>> stateSets) {
+        return namedSets(predicate, stateSets, false);
+    }
+
+    /** Like {@link #namedSets}, but only the sets it may name a state of for {@code old(this)} */
+    static Set<Integer> namedSetsBefore(Predicate predicate, List<List<State>> stateSets) {
+        return namedSets(predicate, stateSets, true);
+    }
+
+    private static Set<Integer> namedSets(Predicate predicate, List<List<State>> stateSets, boolean onOld) {
+        return IntStream.range(0, stateSets.size())
+                .filter(k -> mayName(predicate.getExpression(),
+                        stateSets.get(k).stream().map(s -> s.names().get(0)).collect(Collectors.toSet()), onOld))
+                .boxed().collect(Collectors.toSet());
+    }
+
+    /**
+     * The {@code candidates} in the same state as {@code before} in every state set but those in {@code changed}: the
+     * verifier keeps the state of a set that a state refinement's {@code to} does not name
+     */
+    static List<State> keeping(Collection<State> candidates, State before, Set<Integer> changed) {
+        return candidates.stream().filter(c -> IntStream.range(0, before.names().size())
+                .allMatch(k -> changed.contains(k) || c.names().get(k).equals(before.names().get(k)))).toList();
+    }
+
+    private static boolean mayName(Expression expression, Set<String> states, boolean onOld) {
+        if (expression instanceof AliasInvocation)
+            return true;
+        if (expression instanceof FunctionInvocation f && states.contains(Utils.getSimpleName(f.getName()))
+                && (!onOld || invokesOld(f)))
+            return true;
+        return expression.getChildren().stream().anyMatch(e -> mayName(e, states, onOld));
+    }
+
+    private static boolean invokesOld(Expression expression) {
+        return expression instanceof FunctionInvocation f && Keys.OLD.equals(f.getName())
+                || expression.getChildren().stream().anyMatch(StateMachine::invokesOld);
+    }
+
     private Optional<Transition> transition(State from, RefinedFunction method) {
         return transitions.stream().filter(t -> t.from().equals(from) && t.method().equals(method)).findFirst();
     }
 
@@ -3,8 +3,10 @@
 import java.util.ArrayDeque;
 import java.util.ArrayList;
 import java.util.Deque;
+import java.util.HashMap;
 import java.util.HashSet;
 import java.util.LinkedHashMap;
+import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Map;
 import java.util.Objects;
@@ -509,32 +511,68 @@ private Optional<List<Transition>> transitionsOf(RefinedFunction method) throws
         if (!canModel(method))
             return Optional.empty();
         List<Transition> transitions = new ArrayList<>();
+        List<List<State>> sets = stateSets();
+        List<ObjectState> changes = method.getAllStates();
+        // whether a from holds depends only on the state sets it names: the others are other ghost functions
+        List<Map<List<String>, CallVariant.Entry>> entries = changes.stream()
+                .map(c -> new HashMap<List<String>, CallVariant.Entry>()).collect(Collectors.toList());
+        List<Map<List<String>, Set<List<String>>>> afters = changes.stream()
+                .map(c -> new HashMap<List<String>, Set<List<String>>>()).collect(Collectors.toList());
         for (State state : states) {
             Predicate current = state.predicate().substituteVariable(Keys.THIS, BEFORE);
-            for (ObjectState change : method.getAllStates()) {
+            for (int i = 0; i < changes.size(); i++) {
+                ObjectState change = changes.get(i);
                 if (!change.hasFrom())
                     continue;
-                Predicate from = change.getFrom().substituteVariable(Keys.THIS, BEFORE);
-                if (solver.implies(current, from)) {
+                List<String> named = StateMachine.namedSets(change.getFrom(), sets).stream().map(state.names()::get)
+                        .toList();
+                CallVariant.Entry entry = entries.get(i).get(named);
+                if (entry == null) {
+                    entry = entry(current, change.getFrom().substituteVariable(Keys.THIS, BEFORE));
+                    entries.get(i).put(named, entry);
+                }
+                if (entry == CallVariant.Entry.HOLDS) {
                     // like the verifier, the first state change whose precondition holds is the one applied
-                    Set<State> next = statesAfter(change, state, current);
+                    Set<State> next = statesAfter(change, state, current, sets, afters.get(i));
                     if (next.isEmpty())
                         return Optional.empty();
                     transitions.add(new Transition(state, method, change, next));
                     break;
                 }
-                if (solver.compatible(current, from))
+                if (entry == CallVariant.Entry.UNDECIDED)
                     return Optional.empty(); // allowed only sometimes in this state
             }
         }
         return Optional.of(transitions);
     }
 
-    private Set<State> statesAfter(ObjectState change, State state, Predicate current) throws LJError {
+    private CallVariant.Entry entry(Predicate current, Predicate from) throws LJError {
+        if (solver.implies(current, from))
+            return CallVariant.Entry.HOLDS;
+        return solver.compatible(current, from) ? CallVariant.Entry.UNDECIDED : CallVariant.Entry.FAILS;
+    }
+
+    /**
+     * The states {@code change} can lead to from {@code state}. The verifier keeps the state of the sets its {@code to}
+     * does not name, and the states it can lead to in the others depend only on the state before in the sets it names
+     * for {@code old(this)}, so they are asked once for each and kept in {@code known}
+     */
+    private Set<State> statesAfter(ObjectState change, State state, Predicate current, List<List<State>> sets,
+            Map<List<String>, Set<List<String>>> known) throws LJError {
         if (!change.hasTo())
             return Set.of(state);
-        Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER);
-        return solver.possibleStates(states, Predicate.createConjunction(current, to), AFTER);
+        List<Integer> named = StateMachine.namedSets(change.getTo(), sets).stream().sorted().toList();
+        List<State> candidates = StateMachine.keeping(states, state, Set.copyOf(named));
+        List<String> before = StateMachine.namedSetsBefore(change.getTo(), sets).stream().sorted()
+                .map(state.names()::get).toList();
+        if (!known.containsKey(before)) {
+            Predicate to = change.getTo().substituteVariable(Keys.THIS, AFTER).changeOldMentions(BEFORE, AFTER);
+            known.put(before, solver.possibleStates(candidates, Predicate.createConjunction(current, to), AFTER)
+                    .stream().map(s -> named.stream().map(s.names()::get).toList()).collect(Collectors.toSet()));
+        }
+        Set<List<String>> after = known.get(before);
+        return candidates.stream().filter(c -> after.contains(named.stream().map(c.names()::get).toList()))
+                .collect(Collectors.toCollection(LinkedHashSet::new));
     }
 
     /** The states {@code constructor} can create the object in, or nothing if they depend on its arguments */
 
@@ -15,6 +15,8 @@
 
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.AliasInvocation;
+import liquidjava.utils.constants.Keys;
 
 class StateMachineTest {
 
@@ -23,6 +25,9 @@ class StateMachineTest {
     private static final State OPEN_UNLOCKED = state("open", "unlocked");
     private static final State CLOSED_LOCKED = state("closed", "locked");
     private static final State CLOSED_UNLOCKED = state("closed", "unlocked");
+    private static final List<List<State>> SETS = List.of(List.of(state("open"), state("closed")),
+            List.of(state("locked"), state("unlocked")));
+    private static final Predicate THIS = Predicate.createVar(Keys.THIS);
     private static final StateMachine MACHINE = machine(
             List.of(OPEN_LOCKED, OPEN_UNLOCKED, CLOSED_LOCKED, CLOSED_UNLOCKED));
 
@@ -139,6 +144,41 @@ void callWhoseStatesAfterAreUnknownIsNotAllowed() {
         assertFalse(machine(ABC, call).allows(Set.of(A), call));
     }
 
+    @Test
+    void setsNamedAreThoseWithAStateInThePredicate() {
+        Predicate openAndPositive = Predicate.createConjunction(inState("open", THIS),
+                Predicate.createInvocation("size", THIS));
+        assertEquals(Set.of(0), StateMachine.namedSets(openAndPositive, SETS));
+        assertEquals(Set.of(), StateMachine.namedSets(new Predicate(), SETS));
+    }
+
+    @Test
+    void aliasMayNameEverySet() {
+        Predicate alias = new Predicate(new AliasInvocation("Ready", List.of(THIS.getExpression())));
+        assertEquals(Set.of(0, 1), StateMachine.namedSets(alias, SETS));
+        assertEquals(Set.of(0, 1), StateMachine.namedSetsBefore(alias, SETS));
+    }
+
+    @Test
+    void setsNamedBeforeAreThoseNamedForOld() {
+        // locked(this) && open(old(this))
+        Predicate to = Predicate.createConjunction(inState("locked", THIS),
+                inState("open", Predicate.createInvocation(Keys.OLD, THIS)));
+        assertEquals(Set.of(0, 1), StateMachine.namedSets(to, SETS));
+        assertEquals(Set.of(0), StateMachine.namedSetsBefore(to, SETS));
+    }
+
+    @Test
+    void candidatesKeepTheStateOfSetsNotChanged() {
+        assertEquals(List.of(OPEN_LOCKED, OPEN_UNLOCKED),
+                StateMachine.keeping(MACHINE.states(), OPEN_LOCKED, Set.of(1)));
+        assertEquals(List.of(OPEN_LOCKED), StateMachine.keeping(MACHINE.states(), OPEN_LOCKED, Set.of()));
+    }
+
+    private static Predicate inState(String state, Predicate object) {
+        return Predicate.createInvocation(state, object);
+    }
+
     /** Effects given by hand: the states where each refinement's from holds, and the states after the call from each */
     private record Effects(boolean changesState, Map<State, Set<State>> after, Set<State> undecided) {
         Effects(boolean changesState, Map<State, Set<State>> after) {