Write the state origin notes as Origin: line L, <call> <verb> <state>

- the call that last set the sets "makes" their state;
- a call the receiver was assigned "returns" it, or "says nothing
  about" the sets;
- the creation fact says the constructor "creates" the receiver with
  its state, not that it makes the current one.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/StateOrigin.java

@@ -237,8 +237,9 @@ private Optional<String> lastSetNote(StateChange change, VariableInstance after,
         Optional<Predicate> facts = foundAbout(after, shownFound, changed);
         if (facts.isEmpty() || !implies(after.getRefinement(), facts.get()))
             return Optional.empty();
-        return code(change.position()).map(code -> String.format("From: %s, last set at line %d: %s",
-                display(facts.get(), after.getName()), change.position().getLine(), code));
+        // the call last set these sets, so it is what makes them so
+        return code(change.position()).map(code -> String.format("Origin: line %d, %s makes %s",
+                change.position().getLine(), code, display(facts.get(), after.getName())));
     }
 
     /**
@@ -251,14 +252,13 @@ private Optional<String> returnedNote(CallResult call, VariableInstance assigned
         Optional<String> code = code(call.position());
         if (code.isEmpty())
             return Optional.empty();
-        String from = String.format("From: %s = %s, line %d, ", written, code.get(), call.position().getLine());
+        String origin = String.format("Origin: line %d, %s ", call.position().getLine(), code.get());
         Optional<Predicate> facts = factsOn(call.returned(), Keys.WILDCARD, shown);
         Optional<Predicate> found = foundAbout(assigned, shownFound, shown);
         if (facts.isPresent())
             return found.isPresent()
                     && implies(facts.get().substituteVariable(Keys.WILDCARD, assigned.getName()), found.get())
-                            ? Optional.of(from + "which returns " + display(facts.get(), Keys.WILDCARD))
-                            : Optional.empty();
+                            ? Optional.of(origin + "returns " + display(facts.get(), Keys.WILDCARD)) : Optional.empty();
         Predicate returned = call.returned();
         // a set declared without a name has a generated one, which the message does not otherwise show
         // a state refinement of the method may give the value its state, as `to = "running(_)"` does
@@ -269,7 +269,7 @@ && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains)
                 && !hasAlias(returned.getExpression());
         String sets = shown.stream().map(set -> Utils.getSimpleName(set.getName()) + "(" + written + ")").sorted()
                 .collect(Collectors.joining(", "));
-        return saysNothing ? Optional.of(from + "which says nothing about " + sets) : Optional.empty();
+        return saysNothing ? Optional.of(origin + "says nothing about " + sets) : Optional.empty();
     }
 
     /**
@@ -278,7 +278,7 @@ && setsOf(List.of(returned), ghostStates).stream().noneMatch(shown::contains)
      * constructor only, given when the walk back to the call that last set the state broke, e.g. at a join of branches
      */
     private Optional<String> creationNote(VariableInstance unknown, Predicate shownFound) throws LJError {
-        DebugLog.warn("From note: no known call gives " + unknown.getName() + " its state, e.g. a join of branches");
+        DebugLog.warn("Origin note: no known call gives " + unknown.getName() + " its state, e.g. a join of branches");
         if (!(invocation instanceof CtInvocation<?> call && call.getTarget()instanceof CtVariableRead<?> read
                 && read.getVariable().getDeclaration()instanceof CtLocalVariable<?> local
                 && local.getDefaultExpression()instanceof CtConstructorCall<?> constructor
@@ -292,8 +292,9 @@ private Optional<String> creationNote(VariableInstance unknown, Predicate shownF
         if (facts.isEmpty() || found.isEmpty() || code.isEmpty()
                 || !implies(found.get(), facts.get().substituteVariable(Keys.THIS, unknown.getName())))
             return Optional.empty();
-        return Optional.of(String.format("From: %s is created at line %d by %s, which makes it %s", written,
-                created.position().getLine(), code.get(), display(facts.get(), Keys.THIS)));
+        // not "makes": a later call may have set the state again, which found no longer tells
+        return Optional.of(String.format("Origin: line %d, %s creates %s with %s", created.position().getLine(),
+                code.get(), written, display(facts.get(), Keys.THIS)));
     }
 
     /**

liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java

@@ -24,13 +24,13 @@ void unrefinedParameterIsNamedWithItsMethod() {
 
     @Test
     void stateIsTracedToTheCallThatLastSetTheSetThatIsWrong() {
-        assertEquals(List.of("From: lockState(d) == locked, last set at line 27: d.lock()"),
+        assertEquals(List.of("Origin: line 27, d.lock() makes lockState(d) == locked"),
                 verify("ErrorStateHintMultipleSets.java").getMessageNotes());
     }
 
     @Test
     void stateIsTracedToTheReturnRefinementOfTheCallAssigned() {
-        assertEquals(List.of("From: task = FromReturnedTask.create(), line 27, which returns phase(task) == idle"),
+        assertEquals(List.of("Origin: line 27, FromReturnedTask.create() returns phase(task) == idle"),
                 verify("ErrorStateFromReturnedValue.java").getMessageNotes());
     }