Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

[TS PBT] Reuse bounded command models and state invariants in hybrid search

Đang mở
  • Có gì không ổn?
#402 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Maintainer thường phản hồi trong vòng 1 ngày

Chưa có ai nhận issue này.

Đánh giá

Độ khó
5/5
Thời gian dự kiến
Hơn một tuần
Mức phù hợp với người mới
35/100
Loại issue
Tính năng
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Sôi nổi
Công nghệ
kotlin
Lĩnh vực
devtools, testing-qa

Hướng nghiên cứu

Read the core assessment in #405 and the related contracts in #395, #353/#354, #396/#398, and #384 before designing the extension; coordinate dependent sequence generation with #400. Run focused checks for reset, within-sequence mutation, guards, replay, and shrinking. Done means a bounded stateful model reproduces a sequence-dependent fault through the original command model and publishes its bounds, commands, and evaluation results.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

Part of the full #345 delivery. Builds on #395, #353/#354, and #396/#398. Coordinate with #400 for dependent sequence generation without making the two implementations cyclic.

Delivery stage

This is a stage-two extension of #345. Complete and record the core assessment in #405 before accepting this extension's end-to-end integration and results. Literature, interface design and focused experiments may start earlier; the extension never blocks #355 or #405.

Reuse the completed core contracts. This issue owns any extension-specific changes to observation, binding, scheduling, replay, shrinking and feedback integration, with focused follow-up PRs; do not retroactively broaden #351/#352 or require already completed core issues to reopen. A negative or inconclusive pilot is recorded honestly and informs design; it does not silently cancel this full-roadmap obligation.

Publish a separately identifiable extension configuration and evaluate it against the same original oracle with the extension disabled. Its final held-out evaluation belongs to #357 and is reported separately from the development pilot.

Goal

Reuse PBT model-based command sequences, guards and postconditions to find stateful faults across a bounded sequence of operations.

Scope

  • Support a bounded synchronous command model with an explicit initial model/SUT state, command identity/arguments, pure admissibility guard and concrete postcondition/invariant. The sequence is one property invocation.
  • Reset model/SUT state between samples, replay and shrink attempts; preserve intended state and aliases between commands in the same sequence. This extends #384 explicitly without introducing persistent cross-sample module state.
  • Begin with a concrete collection/cache-like model and bounded command count. Use supported primitive/tuple arguments and explicit lowering/unrolling rather than requiring arbitrary object graphs or concurrency.
  • Preserve the user's reference model and original command checks as the concrete oracle. Record per-step observations and hypothesis contexts keyed by command/state features.
  • Let USVM select arguments and/or a bounded continuation of a concrete prefix. Reconstruct/reexecute the prefix faithfully; do not assert a sampled heap as a universally reachable symbolic state.
  • Share the common total deadline and target/result/replay contracts. Track sequence bounds, unsupported commands, divergence and model errors separately.
  • Minimize command sequences and arguments with backend support, preserving executable guards and the same failure. Deleting a setup command must not turn a failure into an invalid sequence.
  • No async scheduling, distributed state, uncontrolled I/O or arbitrary environment snapshotting is required.

Definition of Done

  • A real or representative stateful API has a confirmed sequence-dependent fault that is not exposed by isolated calls from the initial state.
  • PBT state/command observations guide a bounded symbolic continuation, which reproduces through the full original command model.
  • Cross-sample reset, within-sequence mutation, invalid guards, prefix replay and sequence shrinking have focused tests.
  • The model, author effort, bounds and supported commands are published. #357 compares the same stateful oracle with and without feedback and with PBT-only generation.
Ngôn ngữ chính
Kotlin
Star
33
Fork
27
Merge trung bình
2 ngày 20 giờ
Pull request đã merge (30 ngày)
10

Chuẩn bị môi trường

Dự án này không cung cấp dev container, Dockerfile hay hướng dẫn đóng góp, nên bạn cần tự thiết lập môi trường: hãy bắt đầu từ README và xem hướng dẫn đóng góp lần đầu của chúng tôi để biết các bước chung.

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của UnitTestBot/usvm

Tất cả issue của UnitTestBot/usvm

Issue tương tự

Thêm issue về Kotlin

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.