Skip to content

[TS] Preserve analysis work across bounded phases - #546

Closed
CaelmBleidd wants to merge 1 commit into
mainfrom
caelmbleidd/ts-resumable-analysis
Closed

CaelmBleidd wants to merge 1 commit into
mainfrom
caelmbleidd/ts-resumable-analysis

Conversation

@CaelmBleidd

Copy link
Copy Markdown
Member

Pausing TypeScript analysis previously left no supported way to continue its pending queue. Add TsMachine.openAnalysis(...).advance(maxSteps = ...) so one property can yield between feedback rounds while retaining its states, solver models, coverage, collectors and cumulative limits. Existing analysis entry points execute one uninterrupted advance through the same implementation.

Bounded phases currently support one runnable entry point. Multi-entry analysis remains available without phase yields; its existing time-based fairness is not advertised as resumable. One session owns the machine at a time, including preparation callbacks. Closing the session discards pending work, closing the machine invalidates the session, and an exceptional advance cannot be resumed. Completed analyses return their previous snapshot without executing again.

Validation on Java 11 / Node 22:

  • Nine new session tests cover phased versus uninterrupted outcomes and solver-query counts, native witness replay, cumulative step/timeout limits, stable result snapshots, ownership, failure and closure.
  • All 21 focused session, suspended-state and startup-input tests pass.
  • Strict TypeScript main/test Detekt passes with no findings; git diff --check is clean.
  • Full TypeScript suite on 25f663469ad27929f41fe55146b8736762465210: 1,739 tests, 1,600 passed, 139 existing skips, no failures or errors.

Refs #481. This is the reusable execution primitive. PBT evidence admission, changes to pending target selection and the repeated generation/search loop are separate integrations; this PR does not complete #481 or establish experimental benefit. Benchmark campaigns remain paused.

@CaelmBleidd

Copy link
Copy Markdown
Member Author

Closing as not planned after the two-phase scope agreed in #345: one PBT generation phase followed by one uninterrupted USVM search needs no resumable core session. The only identified product consumer was #549, which is already closed; no open PR currently depends on this branch or references an independent consumer. This does not mark #481 complete. The branch and commits are preserved, as are the historical experimental checkouts.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant