diff --git a/.gitignore b/.gitignore index 10d5d675..f82ce7b1 100644 --- a/.gitignore +++ b/.gitignore @@ -78,4 +78,7 @@ tests/Hedgehog.Tests/tests-js/ BenchmarkDotNet.Artifacts # docfx -_site/ \ No newline at end of file +_site/ + +# tests / verifier +*.received.* diff --git a/src/Hedgehog.Stateful/Hedgehog.Stateful.fsproj b/src/Hedgehog.Stateful/Hedgehog.Stateful.fsproj index 51061446..2454ff12 100644 --- a/src/Hedgehog.Stateful/Hedgehog.Stateful.fsproj +++ b/src/Hedgehog.Stateful/Hedgehog.Stateful.fsproj @@ -30,7 +30,6 @@ - diff --git a/src/Hedgehog.Stateful/Parallel.fs b/src/Hedgehog.Stateful/Parallel.fs index e7053554..b208bfef 100644 --- a/src/Hedgehog.Stateful/Parallel.fs +++ b/src/Hedgehog.Stateful/Parallel.fs @@ -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 @@ -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 @@ -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). @@ -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 @@ -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) @@ -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 @@ -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 -> @@ -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 @@ -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 diff --git a/src/Hedgehog.Stateful/Sequential.fs b/src/Hedgehog.Stateful/Sequential.fs index 5b734123..4750557a 100644 --- a/src/Hedgehog.Stateful/Sequential.fs +++ b/src/Hedgehog.Stateful/Sequential.fs @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 } diff --git a/src/Hedgehog.Stateful/Types.fs b/src/Hedgehog.Stateful/Types.fs index 0f44304d..84bc93d4 100644 --- a/src/Hedgehog.Stateful/Types.fs +++ b/src/Hedgehog.Stateful/Types.fs @@ -8,11 +8,12 @@ type Name = internal Name of int /// -/// 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. /// type Env = private { - values: Map nextId: int } @@ -20,123 +21,67 @@ type Env = private { /// /// 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). /// [] -type Var<'T> = private { +type Var<'T> = + internal /// - /// 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. /// - Name: int + | Symbolic of 'T option /// - /// Indicates if the variable is bound to a generated value. + /// Concrete variable with an actual runtime value from execution. /// - Bounded: bool - /// - /// The optional default value for the variable. - /// - Default: 'T option - /// - /// Transform function applied when resolving the variable from the environment. - /// Handles unboxing and any projections/mappings applied via Var.map. - /// - Transform: obj -> 'T - /// - /// 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. - /// - mutable ResolvedValue: 'T option -} + | Concrete of 'T with /// - /// Gets the unique integer name of the variable. + /// Gets whether the variable has been bound to a concrete execution value. /// - member this.VarName = this.Name - - /// - /// Gets whether the variable is bound to a generated value. - /// - 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 -> " (symbolic)" + match this with + | Concrete value -> $"%A{value}" + | Symbolic (Some defaultValue) -> $"%A{defaultValue}" + | Symbolic None -> "" /// - /// 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). /// - /// The environment to resolve the variable from. + /// The environment capability token. /// The resolved value of the variable. 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" /// - /// Resolve the variable with an explicit fallback value, overriding the variable's default. + /// Resolve the variable with an explicit fallback value. /// - /// The environment to resolve the variable from. - /// The fallback value to use if the variable is not found. - /// The resolved value or the fallback if not found. + /// The environment capability token. + /// The fallback value to use if the variable is symbolic without a default. + /// The resolved value or the fallback. 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 - - /// - /// Set the resolved value for display purposes during counterexample formatting. - /// This should only be called internally by StateFormatter during test failure formatting. - /// - /// The environment to resolve the variable from. - 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) diff --git a/src/Hedgehog.Stateful/Var.fs b/src/Hedgehog.Stateful/Var.fs index 56ff6c34..fff58523 100644 --- a/src/Hedgehog.Stateful/Var.fs +++ b/src/Hedgehog.Stateful/Var.fs @@ -13,7 +13,7 @@ module Var = /// A new symbolic (unbound) Var<T> with the given default value. [] let symbolic (defaultValue: 'T) : Var<'T> = - { Name = -1; Bounded = false; Default = Some defaultValue; Transform = unbox<'T>; ResolvedValue = None } + Symbolic (Some defaultValue) namespace Hedgehog.Stateful.FSharp @@ -23,43 +23,35 @@ open Hedgehog.Stateful [] module Var = /// - /// Resolve a variable using its default value if not found in the environment. + /// Resolve a variable using its default value if symbolic. /// - /// The environment to resolve the variable from. + /// The environment capability token. /// The variable to resolve. /// The resolved value of the variable. let resolve (env: Env) (v: Var<'T>) : 'T = v.Resolve(env) /// - /// Resolve a variable with an explicit fallback value, overriding the variable's default. + /// Resolve a variable with an explicit fallback value. /// - /// The fallback value to use if the variable is not found. - /// The environment to resolve the variable from. + /// The fallback value to use if the variable is symbolic without a default. + /// The environment capability token. /// The variable to resolve. /// The resolved value or the fallback if not found. let resolveOr (fallback: 'T) (env: Env) (v: Var<'T>) : 'T = v.ResolveOr(env, fallback) /// - /// Resolve a variable, returning Error if not found in the environment or if resolution fails. + /// Resolve a variable, returning Error if it's symbolic without a default value. /// /// The variable to resolve. - /// The environment to resolve the variable from. - /// The resolved value as Ok, or Error with failure reason if not found or transform fails. + /// The environment capability token. + /// The resolved value as Ok, or Error with failure reason if symbolic without default. let tryResolve<'T> (v: Var<'T>) (env: Env) : Result<'T, string> = - if not v.Bounded then - match v.Default with - | Some d -> Ok d - | None -> Error "Symbolic variable has no default value" - else - match env.values |> Map.tryFind (Name v.Name) with - | None -> Error $"Var_{v.Name} not found in environment" - | Some value -> - try - Ok (v.Transform value) - with ex -> - Error $"Transform failed: {ex.GetType().Name}" + match v with + | Concrete value -> Ok value + | Symbolic (Some defaultValue) -> Ok defaultValue + | Symbolic None -> Error "Symbolic variable has no default value" /// /// Map a function over a variable, creating a new variable that projects @@ -70,20 +62,18 @@ module Var = /// The variable to map over. /// A new variable with the projection applied. let map (f: 'T -> 'U) (v: Var<'T>) : Var<'U> = - { Name = v.Name - Bounded = v.Bounded - Default = v.Default |> Option.map f - Transform = v.Transform >> f - ResolvedValue = None } + match v with + | Symbolic (Some defaultValue) -> Symbolic (Some (f defaultValue)) + | Symbolic None -> Symbolic None + | Concrete value -> Concrete (f value) - /// Create a bounded var from a Name (used during generation) - let internal bound (name: Name) : Var<'T> = - let (Name n) = name - { Name = n; Bounded = true; Default = None; Transform = unbox<'T>; ResolvedValue = None } + /// Create a symbolic var placeholder (used during generation) + let internal symbolicEmpty () : Var<'T> = + Symbolic None + /// Convert from obj var to typed var (used internally) let internal convertFrom<'T> (v: Var) : Var<'T> = - { Name = v.Name - Bounded = v.Bounded - Default = v.Default |> Option.map unbox<'T> - Transform = unbox<'T> - ResolvedValue = None } + match v with + | Symbolic (Some value) -> Symbolic (Some (unbox<'T> value)) + | Symbolic None -> Symbolic None + | Concrete value -> Concrete (unbox<'T> value) diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/Hedgehog.Stateful.Tests.FSharp.fsproj b/tests/Hedgehog.Stateful.Tests.FSharp/Hedgehog.Stateful.Tests.FSharp.fsproj index 24cc0e7b..0819fec1 100644 --- a/tests/Hedgehog.Stateful.Tests.FSharp/Hedgehog.Stateful.Tests.FSharp.fsproj +++ b/tests/Hedgehog.Stateful.Tests.FSharp/Hedgehog.Stateful.Tests.FSharp.fsproj @@ -11,16 +11,18 @@ + + - + all runtime; build; native; contentfiles; analyzers; buildtransitive diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/Prelude.fs b/tests/Hedgehog.Stateful.Tests.FSharp/Prelude.fs new file mode 100644 index 00000000..8b3ec3aa --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/Prelude.fs @@ -0,0 +1,14 @@ +[] +module Hedgehog.Stateful.Tests.Prelude + +open VerifyTests +open VerifyXunit + +let settings = + let set = VerifySettings() + set.UseDirectory("__snapshots__") + set + +type Verifier with + static member VerifyFormatted<'T>(value: 'T) = + Verifier.Verify($"%A{value}", settings).ToTask() diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/StateFormatterSpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/StateFormatterSpec.fs deleted file mode 100644 index 1a8a2f09..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/StateFormatterSpec.fs +++ /dev/null @@ -1,206 +0,0 @@ -module Hedgehog.Stateful.Tests.StateFormatterSpec - -open Hedgehog.Stateful -open Hedgehog.Stateful.FSharp -open Xunit - -// Test types with various F# constructs -type MyUnion = - | CaseWithVar of Var - | CaseTwoVars of Var * Var - | CaseNoVars of int - -type NestedState = { - OptionalVar: Var option - ResultVar: Result, string> - UnionField: MyUnion - ListOfVars: Var list -} - -type SimpleRecord = { X: Var; Y: Var } - -type Node = { Value: Var; mutable Next: Node option } - -[] -let ``StateFormatter resolves vars inside Option`` () = - let var1 = Var.bound (Name 0) - let state = { - OptionalVar = Some var1 - ResultVar = Error "not used" - UnionField = CaseNoVars 123 - ListOfVars = [] - } - - let env = Env.empty |> Env.add var1 42 - - StateFormatter.formatForDisplay env state |> ignore - - Assert.Contains("42", $"%A{var1}") - -[] -let ``StateFormatter resolves vars inside Result Ok`` () = - let var2: Var = Var.bound (Name 0) - let state = { - OptionalVar = None - ResultVar = Ok var2 - UnionField = CaseNoVars 123 - ListOfVars = [] - } - - let env = Env.empty |> Env.add var2 "hello" - - StateFormatter.formatForDisplay env state |> ignore - - Assert.Contains("\"hello\"", $"%A{var2}") - -[] -let ``StateFormatter resolves vars inside custom union cases`` () = - let var1 = Var.bound (Name 0) - let var2: Var = Var.bound (Name 1) - let var3: Var = Var.bound (Name 2) - - let state = { - OptionalVar = None - ResultVar = Error "not used" - UnionField = CaseTwoVars(var2, var3) - ListOfVars = [var1] - } - - let env = - Env.empty - |> Env.add var1 42 - |> Env.add var2 "world" - |> Env.add var3 true - - StateFormatter.formatForDisplay env state |> ignore - - Assert.Contains("42", $"%A{var1}") - Assert.Contains("\"world\"", $"%A{var2}") - Assert.Contains("true", $"%A{var3}") - -[] -let ``StateFormatter handles nested Option Some Some`` () = - let var1: Var = Var.bound (Name 0) - let nestedOption = Some (Some var1) - - let env = - Env.empty - |> Env.add var1 "deeply nested" - - StateFormatter.formatForDisplay env nestedOption |> ignore - - Assert.Contains("\"deeply nested\"", sprintf "%A" var1) - -[] -let ``StateFormatter handles vars in lists`` () = - let var1 = Var.bound (Name 0) - let var2 = Var.bound (Name 1) - let var3 = Var.bound (Name 2) - - let state = { - OptionalVar = None - ResultVar = Error "not used" - UnionField = CaseNoVars 0 - ListOfVars = [var1; var2; var3] - } - - let env = - Env.empty - |> Env.add var1 10 - |> Env.add var2 20 - |> Env.add var3 30 - - StateFormatter.formatForDisplay env state |> ignore - - Assert.Contains("10", $"%A{var1}") - Assert.Contains("20", $"%A{var2}") - Assert.Contains("30", $"%A{var3}") - -[] -let ``StateFormatter preserves object identity`` () = - let var1 = Var.bound (Name 0) - let state = { - OptionalVar = Some var1 - ResultVar = Error "test" - UnionField = CaseNoVars 99 - ListOfVars = [] - } - - let env = Env.empty |> Env.add var1 42 - - let formatted = StateFormatter.formatForDisplay env state - - Assert.True(obj.ReferenceEquals(state, formatted)) - -[] -let ``StateFormatter handles Choice types`` () = - let var1 = Var.bound (Name 0) - let var2: Var = Var.bound (Name 1) - let var3: Var = Var.bound (Name 2) - - let choice1: Choice, string, bool> = Choice1Of3 var1 - let choice2: Choice, bool> = Choice2Of3 var2 - let choice3: Choice> = Choice3Of3 var3 - - let env = - Env.empty - |> Env.add var1 100 - |> Env.add var2 "choice" - |> Env.add var3 false - - StateFormatter.formatForDisplay env choice1 |> ignore - StateFormatter.formatForDisplay env choice2 |> ignore - StateFormatter.formatForDisplay env choice3 |> ignore - - Assert.Contains("100", $"%A{var1}") - Assert.Contains("\"choice\"", $"%A{var2}") - Assert.Contains("false", $"%A{var3}") - -[] -let ``StateFormatter handles vars in arrays`` () = - let var1 = Var.bound (Name 0) - let var2 = Var.bound (Name 1) - - let arr = [| var1; var2 |] - - let env = - Env.empty - |> Env.add var1 5 - |> Env.add var2 10 - - StateFormatter.formatForDisplay env arr |> ignore - - Assert.Contains("5", $"%A{var1}") - Assert.Contains("10", $"%A{var2}") - -[] -let ``StateFormatter handles vars in records`` () = - let var1 = Var.bound (Name 0) - let var2: Var = Var.bound (Name 1) - - let record = { X = var1; Y = var2 } - - let env = - Env.empty - |> Env.add var1 999 - |> Env.add var2 "record field" - - StateFormatter.formatForDisplay env record |> ignore - - Assert.Contains("999", $"%A{var1}") - Assert.Contains("\"record field\"", $"%A{var2}") - -[] -let ``StateFormatter handles circular references without infinite loop`` () = - let var1 = Var.bound (Name 0) - let node = { Value = var1; Next = None } - node.Next <- Some node // Create circular reference - - let env = - Env.empty - |> Env.add var1 42 - - let formatted = StateFormatter.formatForDisplay env node - - Assert.Contains("42", $"%A{var1}") - Assert.True(obj.ReferenceEquals(node, formatted)) diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/VarDisplaySpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/VarDisplaySpec.fs new file mode 100644 index 00000000..7778963f --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/VarDisplaySpec.fs @@ -0,0 +1,79 @@ +module Hedgehog.Stateful.Tests.VarDisplaySpec + +open Hedgehog.Stateful +open VerifyXunit +open Xunit + +// Test types with various F# constructs +type MyUnion = + | CaseWithVar of Var + | CaseTwoVars of Var * Var + | CaseNoVars of int + +type NestedState = { + OptionalVar: Var option + ResultVar: Result, string> + UnionField: MyUnion + ListOfVars: Var list +} + +type SimpleRecord = { X: Var; Y: Var } + +type Node = { Value: Var; mutable Next: Node option } + +[] +let ``Concrete vars display their values`` () = + Concrete 42 |> Verifier.VerifyFormatted + +[] +let ``Symbolic vars with default display the default`` () = + Symbolic (Some "hello") |> Verifier.VerifyFormatted + +[] +let ``Symbolic vars without default display as symbolic`` () = + Symbolic None |> Verifier.VerifyFormatted + +[] +let ``Vars in Option types display correctly`` () = + let concreteVar = Concrete 42 + let symbolicVar : Var = Symbolic (Some "test") + { + OptionalVar = Some concreteVar + ResultVar = Ok symbolicVar + UnionField = CaseNoVars 123 + ListOfVars = [] + } |> Verifier.VerifyFormatted + +[] +let ``Vars in union cases display correctly`` () = + let concreteInt = Concrete 42 + let concreteStr : Var = Concrete "world" + let concreteBool = Concrete true + + { + OptionalVar = None + ResultVar = Error "not used" + UnionField = CaseTwoVars(concreteStr, concreteBool) + ListOfVars = [concreteInt] + } |> Verifier.VerifyFormatted + +[] +let ``Vars in lists display correctly`` () = + let var1 = Concrete 10 + let var2 = Concrete 20 + let var3 = Symbolic (Some 30) + + { + OptionalVar = None + ResultVar = Error "not used" + UnionField = CaseNoVars 0 + ListOfVars = [var1; var2; var3] + } |> Verifier.VerifyFormatted + + +[] +let ``Vars in arrays display correctly`` () = + let var1 = Concrete 5 + let var2 = Symbolic (Some 10) + + [| var1; var2 |] |> Verifier.VerifyFormatted diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/VarMapSpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/VarMapSpec.fs index 55f22573..1cbd6292 100644 --- a/tests/Hedgehog.Stateful.Tests.FSharp/VarMapSpec.fs +++ b/tests/Hedgehog.Stateful.Tests.FSharp/VarMapSpec.fs @@ -48,8 +48,8 @@ type AddPersonCommand() = // Use Var.map to project individual fields from the Person result override _.Update(_, _, personVar) = - { LastPersonName = Var.map (fun p -> p.Name) personVar - LastPersonAge = Var.map (fun p -> p.Age) personVar } + { LastPersonName = Var.map _.Name personVar + LastPersonAge = Var.map _.Age personVar } override _.Ensure(_env, _oldState, _, (name, age), result) = // Verify the returned person has correct values @@ -107,17 +107,16 @@ let ``Var.map allows projecting fields from structured command outputs``() = VarMapSpec().ToProperty(sut).Check() [] -let ``Var.map preserves symbolic variable names``() = +let ``Var.map preserves symbolic status``() = // Create a symbolic var with a default person let personVar = Var.symbolic { Name = "Alice"; Age = 30 } // Map to get name - let nameVar = Var.map (fun p -> p.Name) personVar + let nameVar = Var.map _.Name personVar - // Both vars should have the same Name (symbolic vars have Name = -1) - Assert.Equal(-1, personVar.VarName) - Assert.Equal(-1, nameVar.VarName) - Assert.Equal(personVar.IsBounded, nameVar.IsBounded) + // Both vars should be symbolic (not bounded) + Assert.False(personVar.IsBounded) + Assert.False(nameVar.IsBounded) [] let ``Var.map chains multiple projections``() = @@ -127,6 +126,5 @@ let ``Var.map chains multiple projections``() = let nameVar = Var.map _.Name personVar let nameLengthVar = Var.map String.length nameVar - // All should share the same symbolic name - Assert.Equal(-1, nameLengthVar.VarName) + // All should remain symbolic Assert.False(nameLengthVar.IsBounded) diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Concrete vars display their values.verified.txt b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Concrete vars display their values.verified.txt new file mode 100644 index 00000000..68264e1a --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Concrete vars display their values.verified.txt @@ -0,0 +1 @@ +42 diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Symbolic vars with default display the default.verified.txt b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Symbolic vars with default display the default.verified.txt new file mode 100644 index 00000000..b2c58ec4 --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Symbolic vars with default display the default.verified.txt @@ -0,0 +1 @@ +"hello" diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Symbolic vars without default display as symbolic.verified.txt b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Symbolic vars without default display as symbolic.verified.txt new file mode 100644 index 00000000..9cbcc43d --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Symbolic vars without default display as symbolic.verified.txt @@ -0,0 +1 @@ + diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in Option types display correctly.verified.txt b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in Option types display correctly.verified.txt new file mode 100644 index 00000000..7aa32fbc --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in Option types display correctly.verified.txt @@ -0,0 +1,4 @@ +{ OptionalVar = Some 42 + ResultVar = Ok "test" + UnionField = CaseNoVars 123 + ListOfVars = [] } diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in arrays display correctly.verified.txt b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in arrays display correctly.verified.txt new file mode 100644 index 00000000..af2e8f97 --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in arrays display correctly.verified.txt @@ -0,0 +1 @@ +[|5; 10|] diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in lists display correctly.verified.txt b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in lists display correctly.verified.txt new file mode 100644 index 00000000..6236fe07 --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in lists display correctly.verified.txt @@ -0,0 +1,4 @@ +{ OptionalVar = None + ResultVar = Error "not used" + UnionField = CaseNoVars 0 + ListOfVars = [10; 20; 30] } diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in union cases display correctly.verified.txt b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in union cases display correctly.verified.txt new file mode 100644 index 00000000..0938d631 --- /dev/null +++ b/tests/Hedgehog.Stateful.Tests.FSharp/__snapshots__/VarDisplaySpec.Vars in union cases display correctly.verified.txt @@ -0,0 +1,4 @@ +{ OptionalVar = None + ResultVar = Error "not used" + UnionField = CaseTwoVars ("world", true) + ListOfVars = [42] }