Point out the argument that decided a state a call does not allow (#419)

## Description
Adds the **Argument picks the state** category (codebook C3.1) and a
hint for it. These errors had no useful hint before: a transition that
depends on an argument isn't part of the state machine, so the existing
hints can't explain it.

- Each object instance now records the last call that changed its state
(`StateChange`). Method calls and constructors record their own call,
and state-preserving calls keep the previous record. A join of branches
records nothing, which ends the search below.
- `DecidingArgument` follows that chain back to the last call that
changed a state set the failing call checks. If that call's transition
depends on its arguments or result, the SMT solver looks for values that
would have allowed the failing call: the state before the call, the
call's `to` with its parameters left free, and the failing call's
`from`. The model gives the values for the hint.
- When such values exist, the category comes before the other state
categories. The error then gets only the deciding hint. If none exist,
the error keeps its other category (for example
`ErrorArgumentCannotPickTheState`).

## Example
```
State Refinement Error: found empty(buffer) but expected filled(buffer)

Hints:
  - buffer.reset(boolean) on line 20 decides the state of buffer: with keep == true, this call would be allowed
```
Category: Argument picks the state (C3.1).

## Measured against the codebook
Same runs as #418:
- **Corpus:** 94 of 99 right (91 before), 1 wrong, 4 with no category.
- **Exercises:** 42 of 52 right (34 before), 6 wrong, 4 with no
category.

The category now finds 12 of the 15 C3.1 cases. The ones it misses:
- a guard in `from` that changes no state;
- an earlier value that is the real cause;
- a returned value at a join.

## Type of change
- [x] New feature

## Checklist
- [x] Added tests:
- `ErrorArgumentPicksTheState`, `ErrorConstructorArgumentPicksTheState`
and `ErrorArgumentPicksTheStateEarlier` (the decider is found past a
call on another state set);
- `ErrorArgumentCannotPickTheState` (no value helps, so no category
change);
  - cases in `TestErrorCategories` and `TestStateHints`.
- [x] `mvn test` passes locally

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/ErrorArgumentCannotPickTheState.java

@@ -0,0 +1,24 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "filled", "closed"})
+public class ErrorArgumentCannotPickTheState {
+
+    @StateRefinement(to = "empty(this)")
+    public ErrorArgumentCannotPickTheState() {}
+
+    @StateRefinement(from = "!closed(this)", to = "keep ? filled(this) : empty(this)")
+    public void reset(boolean keep) {}
+
+    @StateRefinement(from = "closed(this)")
+    public void reopen() {}
+
+    // no value of keep closes the object, so the argument is not what went wrong
+    public static void use() {
+        ErrorArgumentCannotPickTheState buffer = new ErrorArgumentCannotPickTheState();
+        buffer.reset(true);
+        buffer.reopen(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheState.java

@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "filled", "closed"})
+public class ErrorArgumentPicksTheState {
+
+    @StateRefinement(to = "empty(this)")
+    public ErrorArgumentPicksTheState() {}
+
+    @StateRefinement(from = "!closed(this)", to = "keep ? filled(this) : empty(this)")
+    public void reset(boolean keep) {}
+
+    @StateRefinement(from = "filled(this)")
+    public void read() {}
+
+    public static void use() {
+        ErrorArgumentPicksTheState buffer = new ErrorArgumentPicksTheState();
+        buffer.reset(false);
+        buffer.read(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorArgumentPicksTheStateEarlier.java

@@ -0,0 +1,29 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"tilingOff", "tilingOn"})
+@StateSet({"uncompressed", "compressed"})
+public class ErrorArgumentPicksTheStateEarlier {
+
+    @StateRefinement(to = "tilingOff(this) && uncompressed(this)")
+    public ErrorArgumentPicksTheStateEarlier() {}
+
+    @StateRefinement(to = "mode == 2 ? tilingOn(this) : tilingOff(this)")
+    public void setTilingMode(int mode) {}
+
+    @StateRefinement(from = "uncompressed(this)", to = "compressed(this)")
+    public void compress() {}
+
+    @StateRefinement(from = "tilingOn(this)")
+    public void setTiling() {}
+
+    // compress() changes another state set, so the tiling mode is what decided the state
+    public static void use() {
+        ErrorArgumentPicksTheStateEarlier param = new ErrorArgumentPicksTheStateEarlier();
+        param.setTilingMode(1);
+        param.compress();
+        param.setTiling(); // Expect: State Refinement Error
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorConstructorArgumentPicksTheState.java

@@ -0,0 +1,19 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"readOnly", "writable"})
+public class ErrorConstructorArgumentPicksTheState {
+
+    @StateRefinement(to = "write ? writable(this) : readOnly(this)")
+    public ErrorConstructorArgumentPicksTheState(boolean write) {}
+
+    @StateRefinement(from = "writable(this)")
+    public void append() {}
+
+    public static void use() {
+        ErrorConstructorArgumentPicksTheState file = new ErrorConstructorArgumentPicksTheState(false);
+        file.append(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/categories/ErrorCategory.java

@@ -8,6 +8,7 @@ public enum ErrorCategory {
 
     OUT_OF_ORDER("A1", "Out of order: the operation is legal for this object, but not right now"),
     OUT_OF_DOMAIN("A2", "Out of domain: the value is outside what is accepted"),
+    ARGUMENT_PICKS_THE_STATE("C3.1", "Argument picks the state: the value passed decides where the object lands"),
     PATH_DEPENDENT_STATE("C4.1", "Path-dependent state: the state differs depending on which branch ran"),
     UNPROVABLE("C4.2", "Unprovable: nothing is known that could prove the requirement");
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/Hint.java

@@ -13,6 +13,8 @@ public record Hint(Kind kind, String message) {
     public enum Kind {
         /** A suggestion that does not come from a specific analysis */
         GENERAL,
+        /** An earlier call whose arguments decided the state, and values that would allow the failing call */
+        DECIDING_ARGUMENT,
         /** Calls to add before the failing call so the object reaches a state that allows it */
         CALL_SEQUENCE,
         /** The calls allowed in the object's current state */

liquidjava-verifier/src/main/java/liquidjava/diagnostics/hints/StateHints.java

@@ -14,10 +14,12 @@
 import liquidjava.diagnostics.hints.Hint.Kind;
 import liquidjava.processor.context.RefinedFunction;
 import liquidjava.processor.context.Variable;
+import liquidjava.processor.state_machine.DecidingArgument;
 import liquidjava.processor.state_machine.State;
 import liquidjava.processor.state_machine.StateMachine;
 import liquidjava.processor.state_machine.Transition;
 import liquidjava.utils.Utils;
+import spoon.reflect.reference.CtExecutableReference;
 import spoon.reflect.reference.CtTypeReference;
 
 /**
@@ -65,6 +67,18 @@ public static List<Hint> forCall(StateMachine machine, RefinedFunction call, Set
                 hints.allowedCalls(current).stream()).toList();
     }
 
+    /** The earlier call whose arguments decided the receiver's state, and values that would allow the call */
+    public static Hint decidingArgument(DecidingArgument deciding, String receiver) {
+        RefinedFunction function = deciding.call().function();
+        String call = CtExecutableReference.CONSTRUCTOR_NAME.equals(function.getName()) ? constructor(function)
+                : receiver + "." + signature(function);
+        String values = deciding.values().isEmpty() ? "other arguments" : deciding.values().entrySet().stream()
+                .map(e -> e.getKey() + " == " + e.getValue()).collect(Collectors.joining(" and "));
+        return new Hint(Kind.DECIDING_ARGUMENT,
+                String.format("%s on line %d decides the state of %s: with %s, this call would be allowed", call,
+                        deciding.call().position().getLine(), receiver, values));
+    }
+
     /** Nothing is known about the receiver's state: list what leads to a state where {@code call} is allowed */
     private List<Hint> reachingCalls(RefinedFunction call, Set<State> goal) {
         Map<RefinedFunction, List<State>> sources = new LinkedHashMap<>();

liquidjava-verifier/src/main/java/liquidjava/processor/context/StateChange.java

@@ -0,0 +1,25 @@
+package liquidjava.processor.context;
+
+import java.util.Optional;
+
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * The call that put an object in its current state
+ *
+ * @param function
+ *            the method or constructor called
+ * @param change
+ *            the state refinement of {@code function} that applied
+ * @param before
+ *            the object before the call, or {@code null} for a constructor
+ * @param position
+ *            where the call is
+ */
+public record StateChange(RefinedFunction function, ObjectState change, VariableInstance before,
+        SourcePosition position) {
+
+    public Optional<VariableInstance> previous() {
+        return Optional.ofNullable(before);
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/VariableInstance.java

@@ -7,6 +7,7 @@
 public class VariableInstance extends RefinedVariable {
 
     private Variable parent;
+    private StateChange stateChange;
 
     public VariableInstance(String name, CtTypeReference<?> type, Predicate c) {
         super(name, type, c);
@@ -33,6 +34,15 @@ public void setParent(Variable p) {
         parent = p;
     }
 
+    /** The last call that changed the state of this object, if it is known */
+    public Optional<StateChange> getStateChange() {
+        return Optional.ofNullable(stateChange);
+    }
+
+    public void setStateChange(StateChange stateChange) {
+        this.stateChange = stateChange;
+    }
+
     public Optional<Variable> getParent() {
         return parent == null ? Optional.empty() : Optional.of(parent);
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

@@ -414,9 +414,13 @@ public boolean checkStateSMT(Predicate prevState, Predicate expectedState, Sourc
 
     public boolean checkStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent)
             throws LJError {
-        SMTResult result = vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p,
-                factory, silent);
-        return result.isOk();
+        return verifyStateSMT(prevState, expectedState, p, silent).isOk();
+    }
+
+    /** Checks that {@code prevState} implies {@code expectedState}, with a counterexample when it does not */
+    public SMTResult verifyStateSMT(Predicate prevState, Predicate expectedState, SourcePosition p, boolean silent)
+            throws LJError {
+        return vcChecker.verifySMTSubtypeStates(prevState, expectedState, context.getGhostStates(), p, factory, silent);
     }
 
     public void throwRefinementError(SourcePosition position, SourcePosition declarationPosition,