Read old(this) in a precondition as the state before the call

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

@@ -0,0 +1,22 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"created", "open"})
+public class ErrorStateHintOldInPrecondition {
+
+    @StateRefinement(to = "created(this)")
+    public ErrorStateHintOldInPrecondition() {}
+
+    @StateRefinement(from = "created(this)", to = "open(this)")
+    public void open() {}
+
+    @StateRefinement(from = "open(old(this))")
+    public void read() {}
+
+    public static void main(String[] args) {
+        ErrorStateHintOldInPrecondition f = new ErrorStateHintOldInPrecondition();
+        f.read(); // Expect: State Refinement Error
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java

@@ -145,7 +145,9 @@ private Optional<List<Transition>> transitionsOf(RefinedFunction method) throws
             for (ObjectState change : method.getAllStates()) {
                 if (!change.hasFrom())
                     continue;
-                Predicate from = change.getFrom().substituteVariable(Keys.THIS, BEFORE);
+                // like the verifier, old(this) in a precondition is the state before the call
+                Predicate from = change.getFrom().substituteVariable(Keys.THIS, BEFORE).changeOldMentions(BEFORE,
+                        BEFORE);
                 if (solver.implies(current, from)) {
                     // like the verifier, the first state change whose precondition holds is the one applied
                     Set<State> next = statesAfter(change, state, current);

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

@@ -40,6 +40,13 @@ void statesOfMultipleStateSetsAreCombined() {
                 new Hint(Kind.AVAILABLE_CALLS, "In state closed and locked, d can call: unlock()"));
     }
 
+    @Test
+    void oldInAPreconditionIsTheStateBeforeTheCall() {
+        assertHints("ErrorStateHintOldInPrecondition.java",
+                new Hint(Kind.CALL_SEQUENCE, "Call f.open() before this call to move f from created to open"),
+                new Hint(Kind.AVAILABLE_CALLS, "In state created, f can call: open()"));
+    }
+
     @Test
     void finalStateSuggestsCreatingANewObject() {
         assertHints("ErrorStateHintFinalState.java", new Hint(Kind.UNREACHABLE_STATE,