Hacktoberfest 2026：メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

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

オープン
  • 何か問題がありますか？
#402 コメント 0 件 リアクション 0 件 担当者 0 名 GitHub で見る

メンテナーはふだん 3 日以内に返信

まだ誰も着手していません。

評価

難易度
5/5
見積もり時間
1週間以上
初心者へのやさしさ
35/100
issue の種類
機能追加
明瞭さ
おおむね明確
活発さ
活発
技術スタック
kotlin
領域
devtools, testing-qa

調査の方向性

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.

索引モデルが issue の本文から書いたものです。

説明

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.
主要言語
Kotlin
スター
33
フォーク
27
平均マージ
4日 8時間
マージ済み PR（30日）
19

環境構築

このプロジェクトには開発コンテナ、Dockerfile、コントリビューションガイドがありません。まず README を読み、一般的な手順ははじめてのコントリビューションガイドを参照してください。

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

UnitTestBot/usvm のほかの issue

UnitTestBot/usvm の issue をすべて見る

似ている issue

Kotlin の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。