Hacktoberfest 2026 : les issues que les mainteneurs ont marquées pour octobre, ouvertes et accessibles aux débutants. Parcourir les issues Hacktoberfest

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

Fermée
  • Quelque chose ne va pas ?
#402 0 commentaires 0 réactions 0 personnes assignées Voir sur GitHub

Les mainteneurs répondent en général sous 1 jour

Personne n'a encore pris cette issue.

Évaluation

Difficulté
5/5
Temps estimé
Plus d'une semaine
Accessibilité débutants
35/100
Type d'issue
Fonctionnalité
Clarté
Plutôt claire
Activité
Active
Stack technique
kotlin
Domaine
devtools, testing-qa

Piste de recherche

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.

Rédigé par le modèle d'indexation à partir du texte de l'issue.

Description

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.
Langage dominant
Kotlin
Étoiles
33
Forks
27
Merge moyen
3 j 21 h
PR mergées (30 j)
88

Préparer son environnement

Ce projet ne fournit ni conteneur de développement, ni Dockerfile, ni guide de contribution : l'installation est à votre charge. Commencez par son README, et consultez notre guide de la première contribution pour les étapes générales.

Par où commencer

  1. Lisez l'issue en entier, puis le guide de contribution du projet.
  2. Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
  3. Forkez le dépôt et travaillez sur une branche.
  4. Ouvrez une pull request qui référence le numéro de l'issue.

Autres issues de UnitTestBot/usvm

Toutes les issues de UnitTestBot/usvm

Issues similaires

Plus d'issues Kotlin

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.