Skip to content

Simplify vars and envs #474

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
AlexeyRaga merged 1 commit into from
Dec 24, 2025
Merged

Simplify vars and envs #474

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,4 +78,7 @@ tests/Hedgehog.Tests/tests-js/
BenchmarkDotNet.Artifacts

# docfx
_site/
_site/

# tests / verifier
*.received.*
1 change: 0 additions & 1 deletion src/Hedgehog.Stateful/Hedgehog.Stateful.fsproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,6 @@
<ItemGroup>
<Compile Include="Types.fs" />
<Compile Include="Var.fs" />
<Compile Include="StateFormatter.fs" />
<Compile Include="Action.fs" />
<Compile Include="ICommand.fs" />
<Compile Include="Command.fs" />
Expand Down
47 changes: 22 additions & 25 deletions src/Hedgehog.Stateful/Parallel.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,7 @@ module Parallel =
let stateAfterSetup =
setup.Steps
|> List.fold (fun s a ->
let name, _ = Env.freshName Env.empty
a.Update s (Var.bound name)
a.Update s (Var.symbolicEmpty())
) initial

// Generate prefix using state after setup
Expand All @@ -43,8 +42,7 @@ module Parallel =
let stateAfterPrefix =
prefix.Steps
|> List.fold (fun s a ->
let name, _ = Env.freshName Env.empty
a.Update s (Var.bound name)
a.Update s (Var.symbolicEmpty())
) stateAfterSetup

// Generate branches from state after prefix
Expand Down Expand Up @@ -85,11 +83,10 @@ module Parallel =
match Map.tryFind action.Id results with
| None -> None
| Some output ->
let name, env' = Env.freshName env
let outputVar = Var.bound name
let env'' = Env.add outputVar output env'
let _, env' = Env.freshName env
let outputVar = Concrete output
let state' = action.Update state outputVar
Some (state', env'')
Some (state', env')

/// Recursively search for a valid interleaving of the two branches.
/// Returns true as soon as a valid interleaving is found (early termination).
Expand Down Expand Up @@ -152,12 +149,12 @@ module Parallel =
match result with
| ActionResult.Failure ex ->
do! Property.counterexample (fun () -> formatActionName action)
do! Property.counterexample (fun () -> $"Final state: %A{StateFormatter.formatForDisplay env state}")
do! Property.counterexample (fun () -> $"Final state: %A{state}")
return! Property.exn ex
| ActionResult.Success output ->
let name, env' = Env.freshName env
let outputVar = Var.bound name
env <- Env.add outputVar output env'
let _, env' = Env.freshName env
let outputVar = Concrete output
env <- env'
state <- action.Update state outputVar

// Run prefix sequentially
Expand All @@ -169,13 +166,13 @@ module Parallel =
match result with
| ActionResult.Failure ex ->
do! Property.counterexample (fun () -> formatActionName action)
do! Property.counterexample (fun () -> $"Final state: %A{StateFormatter.formatForDisplay env state}")
do! Property.counterexample (fun () -> $"Final state: %A{state}")
return! Property.exn ex
| ActionResult.Success output ->
prefixResults.Add(action.Id, output)
let name, env' = Env.freshName env
let outputVar = Var.bound name
env <- Env.add outputVar output env'
let _, env' = Env.freshName env
let outputVar = Concrete output
env <- env'
state <- action.Update state outputVar

// Save state and env before parallel branches (which is also before cleanup)
Expand All @@ -193,11 +190,10 @@ module Parallel =
| ActionResult.Failure ex ->
return Error ex
| ActionResult.Success output ->
let name, env' = Env.freshName branchEnv
let outputVar = Var.bound name
let newEnv = Env.add outputVar output env'
let _, env' = Env.freshName branchEnv
let outputVar = Concrete output
let newState = action.Update branchState outputVar
return! loop ((action.Id, output) :: results) newEnv newState rest
return! loop ((action.Id, output) :: results) env' newState rest
}
loop [] env state branch

Expand All @@ -215,7 +211,7 @@ module Parallel =
| Error ex, _ | _, Error ex ->
// Branch failed - report state before branches
property {
do! Property.counterexample (fun () -> $"Final state: %A{StateFormatter.formatForDisplay envBeforeBranches stateBeforeBranches}")
do! Property.counterexample (fun () -> $"Final state: %A{stateBeforeBranches}")
return! Property.exn ex
}
| Ok results1, Ok results2 ->
Expand All @@ -229,7 +225,7 @@ module Parallel =
if not linearizable then
property {
do! Property.counterexample (fun () -> "No valid interleaving found")
do! Property.counterexample (fun () -> $"Final state: %A{StateFormatter.formatForDisplay envBeforeBranches stateBeforeBranches}")
do! Property.counterexample (fun () -> $"Final state: %A{stateBeforeBranches}")
return! Property.failure
}
else
Expand All @@ -249,9 +245,10 @@ module Parallel =
| ActionResult.Failure ex ->
cleanupError <- Some (formatActionName action, ex)
| ActionResult.Success output ->
let name, env' = Env.freshName env
let outputVar = Var.bound name
env <- Env.add outputVar output env'
let _, env' = Env.freshName env
let outputVar = Concrete output
env <- env'
state <- action.Update state outputVar

// Check linearizability first
do! linearizabilityCheck
Expand Down
29 changes: 14 additions & 15 deletions src/Hedgehog.Stateful/Sequential.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,8 @@ module Sequential =

// Use outcome to compute next state for subsequent actions
let outcomeAction, outcomeEnv = Tree.outcome actionAndEnvTree
let name, nextEnv = Env.freshName outcomeEnv
let outputVar = Var.bound name
let _, nextEnv = Env.freshName outcomeEnv
let outputVar = Var.symbolicEmpty()
let nextState = outcomeAction.Update currentState outputVar

// Recursively generate rest with updated state
Expand Down Expand Up @@ -94,8 +94,8 @@ module Sequential =

// Extract outcome for state evolution
let action, env' = Tree.outcome actionAndEnvTreeResult
let name = fst (Env.freshName env)
let outputVar = Var.bound name
let _, _ = Env.freshName env
let outputVar = Var.symbolicEmpty()
let state' = action.Update state outputVar

// Recurse with split seed
Expand All @@ -112,7 +112,7 @@ module Sequential =
| [] -> true
| action :: rest ->
if action.Require env state then
let state' = action.Update state (Var.bound (Name counter))
let state' = action.Update state (Var.symbolicEmpty())
validateSequence env state' (counter + 1) rest
else false

Expand All @@ -121,8 +121,8 @@ module Sequential =
let allActions = setupActions @ testActions
allActions
|> List.indexed
|> List.fold (fun state (counter, action) ->
action.Update state (Var.bound (Name counter))
|> List.fold (fun state (_counter, action) ->
action.Update state (Var.symbolicEmpty())
) initial

// Main generator
Expand Down Expand Up @@ -201,13 +201,12 @@ module Sequential =
// Add counterexample for the failing action before propagating the exception
do! Property.counterexample (fun () -> formatActionName action)
if action.Category <> ActionCategory.Cleanup then
do! Property.counterexample (fun () -> $"Failed at state: %A{StateFormatter.formatForDisplay env state}")
do! Property.counterexample (fun () -> $"Failed at state: %A{state}")
do! Property.exn ex

| ActionResult.Success output ->
let name, env' = Env.freshName env
let outputVar = Var.bound name
let env'' = Env.add outputVar output env'
let _, env' = Env.freshName env
let outputVar = Concrete output
let state0 = state
let state1 = action.Update state outputVar

Expand All @@ -216,19 +215,19 @@ module Sequential =
// If ensure fails, add final state before propagating
do!
try
action.Ensure env'' state0 state1 output |> Property.ofBool
action.Ensure env' state0 state1 output |> Property.ofBool
with ex ->
if action.Category <> ActionCategory.Cleanup then
property {
do! Property.counterexample (fun () -> $"Failed at state: %A{StateFormatter.formatForDisplay env'' state1}")
do! Property.counterexample (fun () -> $"Failed at state: %A{state1}")
do! Property.exn ex
}
else
Property.exn ex
do! loop state1 env'' rest
do! loop state1 env' rest
}

property {
do! Property.counterexample (fun () -> $"Initial state: %A{StateFormatter.formatForDisplay Env.empty actions.Initial}")
do! Property.counterexample (fun () -> $"Initial state: %A{actions.Initial}")
do! loop actions.Initial Env.empty actions.Steps
}
135 changes: 40 additions & 95 deletions src/Hedgehog.Stateful/Types.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,135 +8,80 @@ type Name = internal Name of int


/// <summary>
/// Environment mapping symbolic variable names to concrete values.
/// Environment used for generating unique action IDs and as a capability token
/// to enforce compile-time safety. The presence of an Env parameter indicates
/// the execution phase, where symbolic variables can be resolved.
/// The SUT is passed separately to Execute, not stored in Env.
/// </summary>
type Env = private {
values: Map<Name, obj>
nextId: int
}


/// <summary>
/// Symbolic variable referencing a command's output. Symbolic variables are placeholders
/// that let us chain commands by using one command's result as input to another, even before execution.
/// A symbolic variable is not yet bound to a generated value and is used to represent a value in the model before binding occurs.
/// Variables can be either Symbolic (during generation, with optional default values) or
/// Concrete (during execution, with actual runtime values).
/// </summary>
[<StructuredFormatDisplay("{DisplayText}")>]
type Var<'T> = private {
type Var<'T> =
internal
/// <summary>
/// The unique integer name of the variable.
/// Symbolic variable with an optional default value.
/// None indicates a placeholder created during generation (not yet executed).
/// Some indicates an initial state default value.
/// </summary>
Name: int
| Symbolic of 'T option
/// <summary>
/// Indicates if the variable is bound to a generated value.
/// Concrete variable with an actual runtime value from execution.
/// </summary>
Bounded: bool
/// <summary>
/// The optional default value for the variable.
/// </summary>
Default: 'T option
/// <summary>
/// Transform function applied when resolving the variable from the environment.
/// Handles unboxing and any projections/mappings applied via Var.map.
/// </summary>
Transform: obj -> 'T
/// <summary>
/// Mutable field used internally for displaying resolved values in counterexamples.
/// Only mutated during test failure formatting, not during normal test execution.
///
/// The purpose is to report failure with the concrete state values,
/// to make dev experience better when debugging failed tests.
///
/// NOT INTENDED TO BE USED FOR ANY OTHER PURPOSE.
/// </summary>
mutable ResolvedValue: 'T option
}
| Concrete of 'T
with
/// <summary>
/// Gets the unique integer name of the variable.
/// Gets whether the variable has been bound to a concrete execution value.
/// </summary>
member this.VarName = this.Name

/// <summary>
/// Gets whether the variable is bound to a generated value.
/// </summary>
member this.IsBounded = this.Bounded
member this.IsBounded =
match this with
| Concrete _ -> true
| Symbolic _ -> false

member private this.DisplayText =
// If resolved for display (during counterexample formatting), show the resolved value
match this.ResolvedValue with
| Some resolved -> $"%A{resolved}"
| None ->
if this.Bounded then
match this.Default with
| Some d -> $"%A{d}"
| None -> $"Var_%d{this.Name}"
else
match this.Default with
| Some d -> $"%A{d}"
| None -> "<no value> (symbolic)"
match this with
| Concrete value -> $"%A{value}"
| Symbolic (Some defaultValue) -> $"%A{defaultValue}"
| Symbolic None -> "<symbolic>"

/// <summary>
/// Resolve the variable using its default if not found in the environment.
/// Resolve the variable to its value.
/// Requires Env parameter as a capability token to enforce that resolution
/// only happens during execution phase (Execute, Require, Ensure methods).
/// </summary>
/// <param name="env">The environment to resolve the variable from.</param>
/// <param name="env">The environment capability token.</param>
/// <returns>The resolved value of the variable.</returns>
member this.Resolve(env: Env) : 'T =
if not this.Bounded then
match this.Default with
| Some d -> d
| None -> failwithf "Symbolic var must have a default value"
else
match Map.tryFind (Name this.Name) env.values with
| Some v -> this.Transform v
| None ->
match this.Default with
| Some d -> d
| None -> failwithf $"Var %A{Name this.Name} not bound in environment and no default provided"
match this with
| Concrete value -> value
| Symbolic (Some defaultValue) -> defaultValue
| Symbolic None -> failwith "Cannot resolve symbolic variable without a default value"

/// <summary>
/// Resolve the variable with an explicit fallback value, overriding the variable's default.
/// Resolve the variable with an explicit fallback value.
/// </summary>
/// <param name="env">The environment to resolve the variable from.</param>
/// <param name="fallback">The fallback value to use if the variable is not found.</param>
/// <returns>The resolved value or the fallback if not found.</returns>
/// <param name="env">The environment capability token.</param>
/// <param name="fallback">The fallback value to use if the variable is symbolic without a default.</param>
/// <returns>The resolved value or the fallback.</returns>
member this.ResolveOr(env: Env, fallback: 'T) : 'T =
if not this.Bounded then
fallback // Override default for unbounded
else
match Map.tryFind (Name this.Name) env.values with
| Some v -> this.Transform v
| None -> fallback

/// <summary>
/// Set the resolved value for display purposes during counterexample formatting.
/// This should only be called internally by StateFormatter during test failure formatting.
/// </summary>
/// <param name="env">The environment to resolve the variable from.</param>
member internal this.SetResolvedValue(env: Env) : unit =
try
let resolved = this.Resolve(env)
this.ResolvedValue <- Some resolved
with
| _ -> () // If resolution fails, leave ResolvedForDisplay as None

static member internal CreateSymbolic(value: 'T) : Var<'T> =
{ Name = -1; Bounded = false; Default = Some value; Transform = unbox<'T>; ResolvedValue = Some value }
match this with
| Concrete value -> value
| Symbolic (Some defaultValue) -> defaultValue
| Symbolic None -> fallback


module internal Env =
/// Empty environment
let empty : Env = { values = Map.empty; nextId = 0 }
let empty : Env = { nextId = 0 }

/// Generate a fresh variable name
/// Generate a fresh action ID
let freshName (env: Env) : Name * Env =
Name env.nextId, { env with nextId = env.nextId + 1 }

/// Store a concrete value for a variable
let add (v: Var<'a>) (value: 'a) (env: Env) : Env =
{ env with values = Map.add (Name v.Name) (box value) env.values }

/// Resolve a variable to its concrete value
let resolve<'T> (v: Var<'T>) (env: Env) : 'T =
v.Resolve(env)
Loading
Loading