Hacktoberfest 2026: die Issues, die Maintainer für den Oktober markiert haben – offen und einsteigerfreundlich. Hacktoberfest-Issues durchsuchen

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

Geschlossen
  • Stimmt etwas nicht?
#402 0 Kommentare 0 Reaktionen 0 zugewiesene Personen Auf GitHub ansehen

Maintainer antworten meist innerhalb von 1 Tag

Dieses Issue hat noch niemand übernommen.

Bewertung

Schwierigkeit
5/5
Geschätzter Aufwand
Über eine Woche
Anfängerfreundlichkeit
35/100
Issue-Typ
Feature
Klarheit
Größtenteils klar
Aktivitätsstatus
Aktiv
Tech-Stack
kotlin
Bereich
devtools, testing-qa

Rechercherichtung

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.

Vom Indexierungsmodell aus dem Issue-Text verfasst.

Beschreibung

Current state (2026-10-14)

Audited against usvm main at 19866c959d.

Stateless property definitions, joint input support and bounded scalar/array observations exist. No command-model sequence search/reduction implementation was identified.

Remaining acceptance boundary

Implement bounded command sequences with guards, model/state invariants, execution provenance and validity-preserving reduction. Reuse existing codecs/oracles/budgets; do not relabel repeated stateless samples as model-based stateful testing.

Original report and acceptance context, retained for traceability

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.
Vorherrschende Sprache
Kotlin
Sterne
33
Forks
27
Ø Merge
3 T. 21 Std.
Gemergte PRs (30 T.)
88

Entwicklungsumgebung

Dieses Projekt bietet weder Dev-Container noch Dockerfile noch Beitragsleitfaden – die Einrichtung liegt bei Ihnen. Beginnen Sie mit der README; die allgemeinen Schritte stehen in unserem Leitfaden für den ersten Beitrag.

Erste Schritte

  1. Lesen Sie das ganze Issue und danach den Beitragsleitfaden des Projekts.
  2. Schreiben Sie ins Issue, dass Sie es übernehmen — das erspart doppelte Arbeit.
  3. Forken Sie das Repository und arbeiten Sie in einem Branch.
  4. Öffnen Sie einen Pull Request, der die Issue-Nummer nennt.

Mehr aus UnitTestBot/usvm

Alle Issues in UnitTestBot/usvm

Ähnliche Issues

Weitere Issues zu Kotlin

Neue Issues direkt in Ihr Postfach

Eine kurze Übersicht über anfängerfreundliche GitHub-Issues.