290 lines
13 KiB
Markdown
290 lines
13 KiB
Markdown
# Paper Analyses For Simulation Architecture
|
|
|
|
This document extracts implementation-relevant lessons from the local paper corpus. The focus is opencode's proposed simulation system: real TUI-driven execution, narrow foundational layer replacement, WebSocket control, trace recording, model-based/property-based exploration, and generated deterministic tests.
|
|
|
|
## 2016: Mysteries of Dropbox
|
|
|
|
**Main idea:** stateful PBT can find bugs in real, black-box, nondeterministic distributed systems by generating action sequences, recording observations, and checking whether the observation trace has some valid explanation under a small model.
|
|
|
|
Useful techniques:
|
|
|
|
- Generate commands separately from observed effects.
|
|
- Model hidden nondeterministic events explicitly, even when the SUT does not expose them.
|
|
- Accept traces if there exists a sequence of hidden events that makes observations valid.
|
|
- Maintain possible model states, not a single expected state.
|
|
- Make quiescence explicit with a `STABILIZE` command.
|
|
- Re-run flaky failures during shrinking when nondeterminism cannot be fully controlled.
|
|
|
|
Pitfalls:
|
|
|
|
- Quiescence detection can lie.
|
|
- A model that is too permissive can explain away real bugs.
|
|
- Timing-dependent failures need either scheduler control or repeated validation.
|
|
- Raw happens-before modeling can become elegant but impractical.
|
|
|
|
Implications for opencode:
|
|
|
|
- Do not compare raw transcripts only. Compare observed behavior against allowed abstract outcomes.
|
|
- Represent hidden runtime transitions like prompt promotion, session wake, provider turn continuation, tool completion, retries, interrupt delivery, and event projection.
|
|
- Add a `drainUntilIdle` or `stabilize` simulation command with strict checks.
|
|
- Record all generated commands, UI actions, backend events, provider scripts, tool results, and snapshots in an append-only trace.
|
|
- Shrinking should preserve semantic validity and revalidate nondeterministic failures.
|
|
|
|
## 2019: Coverage Guided, Property Based Testing
|
|
|
|
**Main idea:** plain random generators often fail when valid inputs have sparse semantic preconditions. Coverage-guided PBT keeps interesting inputs and mutates structured values to explore deeper states.
|
|
|
|
Useful techniques:
|
|
|
|
- Maintain a corpus of inputs that improve coverage.
|
|
- Mutate typed structures rather than raw bytes.
|
|
- Keep both successful seeds and promising discarded seeds.
|
|
- Fall back to random generation when mutation stalls.
|
|
- Use coverage and progress counters, not only binary edge coverage.
|
|
|
|
Pitfalls:
|
|
|
|
- Instrumenting irrelevant framework code hurts performance.
|
|
- Generic mutators can explode in search space.
|
|
- Expert handwritten generators still outperform generic mutation but are expensive.
|
|
|
|
Implications for opencode:
|
|
|
|
- Preserve interesting `Scenario` and `Trace` seeds.
|
|
- Add structured mutators for prompts, tool calls, provider chunks, permission decisions, filesystems, config, interrupt timing, crash/restart points, and scheduler actions.
|
|
- Track semantic novelty: event types, session states, tool outcomes, permission branches, replay/recovery paths, and UI routes.
|
|
- Avoid byte fuzzing as the core; use it only inside fields that are naturally bytes/text.
|
|
|
|
## 2021: Model-Based Testing In Practice
|
|
|
|
**Main idea:** MBT works in industrial E2E systems when models are pragmatic, visible, and integrated into normal automation. Graph-like models are useful because actions and assertions are explicit and coverage is understandable.
|
|
|
|
Useful techniques:
|
|
|
|
- Model nodes as states/checkpoints and edges as actions.
|
|
- Split large systems into small composable models.
|
|
- Use traversal strategies, weights, and stop conditions.
|
|
- Report paths, coverage, and model transitions.
|
|
|
|
Pitfalls:
|
|
|
|
- Heavy formal models reduce adoption.
|
|
- Auto-inferred models can be noisy and costly to clean up.
|
|
- Coverage metrics must be live and inspectable.
|
|
|
|
Implications for opencode:
|
|
|
|
- Start with a small simulation DSL, not a complete formal model.
|
|
- Model domains separately: session lifecycle, prompt admission, queue/steer, tool execution, permissions, interrupts, compaction, crash/restart.
|
|
- Track command coverage, transition coverage, property coverage, and failure-mode coverage.
|
|
- Keep generated failure output readable: model path, user inputs, app observations, violated invariant.
|
|
|
|
## 2022: Property-Based Testing For Metamorphic Testing
|
|
|
|
**Main idea:** metamorphic testing helps when exact expected outputs are unavailable. It checks relations between multiple executions or transformed inputs.
|
|
|
|
Useful techniques:
|
|
|
|
- Generate source cases, derive follow-up cases, and compare related outputs.
|
|
- Use generators and shrinkers that preserve relation validity.
|
|
- Combine multiple metamorphic relations.
|
|
|
|
Pitfalls:
|
|
|
|
- Weak metamorphic relations miss real faults.
|
|
- Naive shrinkers can break validity.
|
|
- Reimplementing production logic in the oracle makes the test useless.
|
|
|
|
Implications for opencode:
|
|
|
|
- Use metamorphic relations for nondeterministic model behavior.
|
|
- Examples:
|
|
- Same prompt ID and same delivery mode should reconcile exactly on retry.
|
|
- Queueing independent prompts should preserve durable admission order.
|
|
- Interrupt/resume should not duplicate promoted user messages or orphan tool results.
|
|
- Crash after durable admission should not invent provider work unless recovery explicitly permits it.
|
|
- Fake renderer and visible renderer should agree on semantic action results.
|
|
- Two app versions should satisfy the same semantic invariants for the same trace.
|
|
|
|
## 2022: Climbing The Stairway To Verification
|
|
|
|
**Main idea:** PBT becomes stronger when it mirrors a refinement/specification structure. The test asks whether implementation behavior refines an executable abstract model.
|
|
|
|
Useful techniques:
|
|
|
|
- Generate one canonical test case and project it into abstract and concrete worlds.
|
|
- Compare implementation output to a finite set of model-allowed outcomes.
|
|
- Keep models abstract and observable.
|
|
- Use executable specs as cheaper, incremental versions of formal proofs.
|
|
|
|
Pitfalls:
|
|
|
|
- The model can become a second implementation.
|
|
- Strong preconditions plus random generation cause excessive discarded tests.
|
|
- Overly abstract nondeterminism can explode.
|
|
|
|
Implications for opencode:
|
|
|
|
- Build simulation around `scenario -> model outcomes -> real app run -> relation check`.
|
|
- The model should represent visible session, message, tool, provider, permission, event, status, and filesystem effects.
|
|
- The model must not reimplement `SessionRunner`, provider streaming, tool registry, or Effect scheduling.
|
|
- Generate concrete scenarios and derive abstract model inputs from them.
|
|
|
|
## 2023: QuickerCheck
|
|
|
|
**Main idea:** PBT and shrinking can be parallelized, especially for expensive properties, if workers have isolated state and reproducible seeds.
|
|
|
|
Useful techniques:
|
|
|
|
- Give each worker its own PRNG seed and size schedule.
|
|
- Stop all workers after the first counterexample.
|
|
- Run cleanup/finalizers for interrupted effectful properties.
|
|
- Use greedy parallel shrinking when deterministic minimality is less important than speed.
|
|
|
|
Pitfalls:
|
|
|
|
- Shared filesystem/global state breaks parallel PBT.
|
|
- Cancellation can leave processes, files, sockets, or locks behind.
|
|
- Parallel shrinking can be slower for cheap properties.
|
|
|
|
Implications for opencode:
|
|
|
|
- Design simulation workers as isolated from the start: workspace, DB, ports, fake providers, random seeds, trace buffers.
|
|
- Use `(campaignSeed, workerID, caseIndex)` for reproducibility.
|
|
- Separate fast local runs from long parallel campaigns.
|
|
- Add cleanup boundaries for every case.
|
|
|
|
## 2024: Can Large Language Models Write Good Property-Based Tests?
|
|
|
|
**Main idea:** LLMs can synthesize useful PBTs, but generated tests must be validated for validity, soundness, and property coverage. Two-stage prompting outperforms monolithic generation.
|
|
|
|
Useful techniques:
|
|
|
|
- First extract properties, then generate tests for one property at a time.
|
|
- Classify failures as invalid test, unsound property, weak property, or real bug.
|
|
- Use mutation/property coverage to check whether a property actually detects violations.
|
|
|
|
Pitfalls:
|
|
|
|
- Passing generated tests can be weak.
|
|
- LLMs overgeneralize documentation and miss implicit preconditions.
|
|
- Mutation coverage can be noisy if mutants are invalid or equivalent.
|
|
|
|
Implications for opencode:
|
|
|
|
- Treat model-generated simulation properties as candidates.
|
|
- Store property lifecycle: proposed, executable, validity-checked, soundness-checked, coverage-scored, accepted, rejected.
|
|
- Generate small focused properties, not one huge “test opencode” property.
|
|
- Expose enough observations for a model to validate its own property assumptions.
|
|
|
|
## 2024: Property-Based Testing In Practice
|
|
|
|
**Main idea:** experienced developers use PBT in a small number of high-leverage patterns. The hardest parts are writing useful properties, writing generators, shrinking, and knowing whether passing tests mean anything.
|
|
|
|
Useful techniques:
|
|
|
|
- High-leverage patterns include differential testing, model-based tests, round trips, catastrophic failure properties, and invariants.
|
|
- Developers validate PBT effectiveness through mutation testing, example inspection, code coverage, property coverage, and supplementary example tests.
|
|
- Passing tests need inspectable generated examples and distribution feedback.
|
|
|
|
Pitfalls:
|
|
|
|
- Derived generators can create false confidence.
|
|
- Shrinkers can violate invariants.
|
|
- Slow PBTs get removed.
|
|
|
|
Implications for opencode:
|
|
|
|
- Provide built-in property families instead of requiring every contributor to invent properties.
|
|
- Show generator stats: action distribution, trace length, discarded cases, transition coverage, example traces.
|
|
- Make failure output a concise, reviewable artifact.
|
|
- Support “promote minimized trace to normal test.”
|
|
|
|
## 2026: Agentic PBT
|
|
|
|
**Main idea:** an agentic loop can generate better PBTs than one-shot prompting by inspecting code/docs, proposing evidence-backed properties, running tests, triaging failures, refining false alarms, and reporting only reproducible bugs.
|
|
|
|
Useful techniques:
|
|
|
|
- Use a structured loop: inspect, propose, execute, triage, refine, report.
|
|
- Prefer high-value property patterns: invariants, round trips, inverse operations, multiple implementations, laws, confluence, metamorphic relations, and no-crash parser entrypoints.
|
|
- Keep an evidence chain for every property.
|
|
|
|
Pitfalls:
|
|
|
|
- Intent ambiguity is the main false-positive source.
|
|
- Internal helpers often have implicit preconditions.
|
|
- Extreme generated inputs can be unrealistic.
|
|
|
|
Implications for opencode:
|
|
|
|
- The simulation system should be friendly to model-driven exploration, not just batch tests.
|
|
- Store prompts, observations, selected actions, available actions, traces, refinements, and final classifications.
|
|
- Add a triage workflow before surfacing model-generated failures as bugs.
|
|
|
|
## 2026: Evolution Of Python Tests Into PBT
|
|
|
|
**Main idea:** existing example and parameterized tests often evolve naturally into PBTs. Generated deterministic tests and PBTs should be connected, not treated as separate worlds.
|
|
|
|
Useful techniques:
|
|
|
|
- Convert constants/parameter tables into generators.
|
|
- Keep explicit examples for known edge cases.
|
|
- Adjust generators/settings over time as tests mature.
|
|
|
|
Pitfalls:
|
|
|
|
- Coverage can be inflated by harness/generator code.
|
|
- PBTs can fail early and cover fewer later assertions.
|
|
- Slow PBTs are removed.
|
|
|
|
Implications for opencode:
|
|
|
|
- Use existing tests as simulation corpus seeds.
|
|
- Convert minimized simulation traces into normal deterministic tests.
|
|
- Keep SUT coverage separate from simulation harness coverage.
|
|
- Store generated regressions as explicit fixtures.
|
|
|
|
## 2026: Natural Language To Executable Properties For Mobile Apps
|
|
|
|
**Main idea:** natural-language app properties can become executable UI properties if the system first performs semantic grounding of UI elements.
|
|
|
|
Useful techniques:
|
|
|
|
- Decompose property synthesis into UI semantic grounding and executable property synthesis.
|
|
- Represent properties as precondition, interaction scenario, postcondition.
|
|
- Enrich each widget with text, ID, type, semantic label, functionality, screenshot/crop, and provenance.
|
|
|
|
Pitfalls:
|
|
|
|
- Similar widgets cause grounding errors.
|
|
- Free-form natural language is less reliable than structured Given/When/Then descriptions.
|
|
- Incorrect preconditions/postconditions are more common than incorrect interactions.
|
|
|
|
Implications for opencode:
|
|
|
|
- Expose semantic TUI state, not just screen text and coordinates.
|
|
- Elements/actions should have stable IDs, roles, labels, capabilities, focus/click/edit metadata, visibility, and provenance.
|
|
- Generated properties should use a precondition/action/postcondition structure.
|
|
|
|
## 2026: PropGen Mobile App Testing
|
|
|
|
**Main idea:** properties can be generated from runtime behavioral evidence. The loop is exploration, evidence collection, property synthesis, executable translation, testing, feedback, and refinement.
|
|
|
|
Useful techniques:
|
|
|
|
- Record condition-action-outcome traces.
|
|
- Use functionality-guided exploration plus random exploration fallback.
|
|
- Refine imprecise properties by classifying whether the problem is precondition, interaction, or postcondition.
|
|
|
|
Pitfalls:
|
|
|
|
- Single traces cause overfitting.
|
|
- Generated properties can assert incidental UI details.
|
|
- Refinement can overfit unless anchored to original evidence.
|
|
|
|
Implications for opencode:
|
|
|
|
- Record rich traces with before-state, action intent, concrete action, model/provider/tool effects, after-state, state diff, and outcome label.
|
|
- Let models derive properties from observed behavior, then validate and refine them.
|
|
- Use both model-guided goals and stochastic action exploration.
|