From c0488774bc99daae2aad2642e2a1d771b051395d Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Sun, 25 Oct 2026 00:48:30 +0100 Subject: [PATCH] Read old(this) in a precondition as the state before the call The state machine builder passed preconditions such as "closed(this) && connected(old(this))" to the solver with old() still in them, so building the machine failed and errors on such classes got no hints, category or state context. Replace old(this) with the state before the call, as the verifier does when it checks the call. Co-Authored-By: Claude Opus 5.5 --- .../ErrorStateHintOldInPrecondition.java | 22 +++++++++++++++++++ .../state_machine/StateMachineBuilder.java | 4 +++- .../liquidjava/api/tests/TestStateHints.java | 7 ++++++ 3 files changed, 32 insertions(+), 1 deletion(-) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorStateHintOldInPrecondition.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorStateHintOldInPrecondition.java b/liquidjava-example/src/main/java/testSuite/ErrorStateHintOldInPrecondition.java new file mode 100644 index 00000000..20d2c70c --- /dev/null +++ b/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 + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java index 3713e034..b99e65ee 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/state_machine/StateMachineBuilder.java @@ -145,7 +145,9 @@ private Optional> 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 next = statesAfter(change, state, current); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java index 8f5b4282..294841bc 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestStateHints.java +++ b/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,