GV

GeezerVison

The World Wide Web, restored to 800 pixels of glory.

Home|About|Gaming cabinet|Archives|How it works|Starter sites

On this site

  • Sign in
  • ActionsCI/CD and automation
  • CodespacesCloud development environments
  • All Features
  • Documentation
  • Training
  • Certifications
  • Build with Copilot
  • Customize Copilot
  • Integrations
  • Trending repos
  • GitHub Sponsors
  • Developer articles
  • Enterprises

This view

  • Original page
  • New address

GeezerVison is showing github.com — Read old(this) in a precondition as the state before the call by CatarinaGamboa · Pull Request #422 · liquid-java/liquidjava

Conversation

@CatarinaGamboa

@CatarinaGamboa CatarinaGamboa commented Oct 24, 2026

Copy link
Copy Markdown
Collaborator

Why

The state machine builder sent preconditions that mention old(this) to the solver without replacing old. One example is the expert DatagramSocket spec's from = "closed(this) && connected(old(this))". The solver failed with Ghost 'old' could not be found, and since the analysis is best effort, every state error on such a class lost its hints, its category and (since #421) its StateErrorContext.

The liquidjava-fsm test that checks the verifier's states against the diagram found this.

What

In StateMachineBuilder.transitionsOf, old(this) in a precondition now means the state before the call, which is how AuxStateHandler.changeState reads it (changeOldMentions(name, name)).

Tests

ErrorStateHintOldInPrecondition with TestStateHints#oldInAPreconditionIsTheStateBeforeTheCall. It fails without the fix and passes with it. On the fsm DatagramSocket client, the error now gets the path-dependent hint. mvn test: 494 tests pass.

🤖 Generated with Claude Code

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.
All reactions
@CatarinaGamboa @claude
Read old(this) in a precondition as the state before the call
c048877 
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 <[email protected]>
rcosta358
rcosta358 approved these changes Oct 25, 2026
View reviewed changes
@CatarinaGamboa
CatarinaGamboa marked this pull request as draft October 26, 2026 11:32
@CatarinaGamboa

CatarinaGamboa commented Nov 4, 2026

Copy link
Copy Markdown
Collaborator Author

Review by Codex (codex-cli 0.164.0, gpt-6-sol), run from Claude Code on the PR diff and the full StateMachineBuilder.java:

I found no concrete correctness issue in the change. Replacing old(this) with the before-call state is consistent with how the builder evaluates preconditions.

The new test covers the basic behavior: a precondition containing old(this) produces state hints. It does not directly cover the DatagramSocket precondition, which combines this and old(this).

Suggested follow-up from that: a test case whose precondition uses both this and old(this), as in the DatagramSocket spec.

🤖 Generated with Claude Code
All reactions

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@rcosta358 rcosta358 rcosta358 approved these changes

Uh oh!

There was an error while loading. Please reload this page.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Uh oh!

There was an error while loading. Please reload this page.

2 participants

@CatarinaGamboa @rcosta358
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
You are visitor 01402503 — GeezerVison does not store the pages you look up.
Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.