Skip to content

[TS PBT] Add direct campaign controls under a shared deadline - #540

Open
CaelmBleidd wants to merge 1 commit into
caelmbleidd/ts-pbt-external-witness-replayfrom
caelmbleidd/pbt-direct-campaign-controls
Open

CaelmBleidd wants to merge 1 commit into
caelmbleidd/ts-pbt-external-witness-replayfrom
caelmbleidd/pbt-direct-campaign-controls

Conversation

@CaelmBleidd

@CaelmBleidd CaelmBleidd commented Oct 15, 2026 •

Copy link
Copy Markdown
Member

Concrete PBT, original-predicate symbolic search, and native candidate confirmation currently require separate calls with independent time budgets. This change adds PropertyCampaignRunner for an ordinary PropertyDefinition, with PBT_ONLY, SYMBOLIC_ONLY, and SEQUENTIAL controls sharing one monotonic deadline.

SYMBOLIC_ONLY confirms and reduces the actual USVM candidate through the existing external-witness implementation from #506. SEQUENTIAL returns a demonstrated concrete violation immediately. Completed concrete results and unresolved symbolic candidates remain available when preparation, confirmation, or the remaining allocation cannot finish. Requested concrete coverage is retained; collection timeouts produce an explicit diagnostic artifact without discarding an already demonstrated violation.

The existing two-argument FastCheckBackend.run keeps its contract. A deadline-aware overload bounds its coverage preparation and supervised process. The TypeScript machine receives the same optional caller deadline callback already used by #524, so machine preparation cannot silently reset the search allocation. Frontend generation reuses the existing JacoDB timeout with the convenience loader's provider, entrypoint and inference settings; failed partial output is discarded and successful temporary IR is cleaned up. JSON loading, mapping, and individual solver calls remain cooperative boundaries; their elapsed time is charged before subsequent work begins.

This is a bounded first implementation slice of #354, stacked on #506 at 0715401d5d973479bc677072322925c47a501c77. It does not close #354 or #353. Concrete named checks work; symbolic named/DSL candidates retain an explicit UNSUPPORTED_REPLAY outcome until the separate executable binding integration exists. CLI wiring, a common serialized campaign artifact, and repeated session/feedback integration remain outside this change. No README changes or benchmark campaigns.

Validation on Java 11 / Node 22: after inheriting the shared transport repair, the complete integration check with #542 passed 195 PBT Kotlin tests, 138 FastCheck Kotlin tests and 186 Node tests, without failures or skips. It includes all 13 direct-campaign scenarios and 18 symbolic-search regressions. The shared timeout class also passes directly on #506. Strict Detekt for the changed sets and git diff --check passed.

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