Skip to content

Allow Generate return symbolic variables as input - #475

Merged
AlexeyRaga merged 4 commits into
masterfrom
correlation-rebased
Dec 29, 2025
Merged

Allow Generate return symbolic variables as input#475
AlexeyRaga merged 4 commits into
masterfrom
correlation-rebased

Conversation

@AlexeyRaga

Copy link
Copy Markdown
Collaborator

Support Symbolic Variables in Command Inputs

Motivation

Commands often need to reference outputs from previous commands (e.g., looking up a user ID that was returned by a prior registration). Previously, Var<T> could only be used as command outputs. Using them as inputs was not supported, making it difficult when commands need to randomly select from collections of symbolic references stored in the state, especially when shrinking can leave variables unbound.

The Solution

Commands can now accept Var<T> as input parameters:

  1. Generate returns Var<T> when picking from state (e.g., randomly selecting from List<Var<int>>)
  2. Require checks if symbolic variables can be resolved before execution (handles shrinking safely)
  3. Execute resolves symbolic variables to concrete values at runtime

Key Changes

  • Resolution API: Resolve, ResolveOr, and TryResolve methods for safe variable resolution
  • Default Values: Symbolic variables can carry defaults for initial state or fallback scenarios
  • Projection: Var.map to extract fields from command outputs
  • Runtime Checks: Require method receives environment to verify variable resolvability, preventing crashes during shrinking

Example

type RegistryState = {
    RegisteredIds: Var<int> list  // Store symbolic references
}

type LookupCommand() =
    inherit Command<Registry, RegistryState, Var<int>, User option>()
    
    override _.Generate(state) = Gen.item state.RegisteredIds
    override _.Require(env, _, idVar) = idVar |> Var.tryResolve env |> Result.isOk
    override _.Execute(sut, env, _, idVar) = 
        let id = idVar.Resolve(env)
        Task.FromResult(sut.Lookup(id))

Commands can now naturally work with symbolic variables as inputs, while Require ensures safe shrinking by skipping commands when referenced variables are unbound.

@AlexeyRaga
AlexeyRaga merged commit 943435e into master Dec 29, 2025
2 checks passed
@AlexeyRaga
AlexeyRaga deleted the correlation-rebased branch December 29, 2025 05:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant