diff --git a/Hedgehog.sln b/Hedgehog.sln index b9e4426c..25b8b5a7 100644 --- a/Hedgehog.sln +++ b/Hedgehog.sln @@ -31,12 +31,6 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Hedgehog.Xunit.Tests.CSharp EndProject Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Hedgehog.Xunit.Tests.FSharp", "tests\Hedgehog.Xunit.Tests.FSharp\Hedgehog.Xunit.Tests.FSharp.fsproj", "{856960BF-6CD8-4BBB-949F-02A47BCF8EC7}" EndProject -Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Hedgehog.Stateful", "src\Hedgehog.Stateful\Hedgehog.Stateful.fsproj", "{E4A2FE8F-65E7-4553-A295-E201908C893D}" -EndProject -Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "Hedgehog.Stateful.Tests.FSharp", "tests\Hedgehog.Stateful.Tests.FSharp\Hedgehog.Stateful.Tests.FSharp.fsproj", "{0B5554AB-C67A-4C1E-AFC7-BFF7DC7DE51E}" -EndProject -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Hedgehog.Stateful.Tests.CSharp", "tests\Hedgehog.Stateful.Tests.CSharp\Hedgehog.Stateful.Tests.CSharp.csproj", "{8303DF19-1DE2-4826-A394-4C74E968EEAC}" -EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU @@ -83,18 +77,6 @@ Global {856960BF-6CD8-4BBB-949F-02A47BCF8EC7}.Debug|Any CPU.Build.0 = Debug|Any CPU {856960BF-6CD8-4BBB-949F-02A47BCF8EC7}.Release|Any CPU.ActiveCfg = Release|Any CPU {856960BF-6CD8-4BBB-949F-02A47BCF8EC7}.Release|Any CPU.Build.0 = Release|Any CPU - {E4A2FE8F-65E7-4553-A295-E201908C893D}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {E4A2FE8F-65E7-4553-A295-E201908C893D}.Debug|Any CPU.Build.0 = Debug|Any CPU - {E4A2FE8F-65E7-4553-A295-E201908C893D}.Release|Any CPU.ActiveCfg = Release|Any CPU - {E4A2FE8F-65E7-4553-A295-E201908C893D}.Release|Any CPU.Build.0 = Release|Any CPU - {0B5554AB-C67A-4C1E-AFC7-BFF7DC7DE51E}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {0B5554AB-C67A-4C1E-AFC7-BFF7DC7DE51E}.Debug|Any CPU.Build.0 = Debug|Any CPU - {0B5554AB-C67A-4C1E-AFC7-BFF7DC7DE51E}.Release|Any CPU.ActiveCfg = Release|Any CPU - {0B5554AB-C67A-4C1E-AFC7-BFF7DC7DE51E}.Release|Any CPU.Build.0 = Release|Any CPU - {8303DF19-1DE2-4826-A394-4C74E968EEAC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {8303DF19-1DE2-4826-A394-4C74E968EEAC}.Debug|Any CPU.Build.0 = Debug|Any CPU - {8303DF19-1DE2-4826-A394-4C74E968EEAC}.Release|Any CPU.ActiveCfg = Release|Any CPU - {8303DF19-1DE2-4826-A394-4C74E968EEAC}.Release|Any CPU.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE @@ -113,8 +95,5 @@ Global {C7D1E5C7-0281-4752-A7C7-E0C2CB2EF13D} = {3C2CF07C-905B-4162-BE81-46060153841B} {1E243C1E-563C-4D59-A270-9CB68B578540} = {ED87B4D7-BBFF-4B2A-A924-91939E5C3F00} {856960BF-6CD8-4BBB-949F-02A47BCF8EC7} = {ED87B4D7-BBFF-4B2A-A924-91939E5C3F00} - {E4A2FE8F-65E7-4553-A295-E201908C893D} = {3C2CF07C-905B-4162-BE81-46060153841B} - {0B5554AB-C67A-4C1E-AFC7-BFF7DC7DE51E} = {ED87B4D7-BBFF-4B2A-A924-91939E5C3F00} - {8303DF19-1DE2-4826-A394-4C74E968EEAC} = {ED87B4D7-BBFF-4B2A-A924-91939E5C3F00} EndGlobalSection EndGlobal diff --git a/docs/stateful/commands.md b/docs/stateful/commands.md deleted file mode 100644 index f57bc7ba..00000000 --- a/docs/stateful/commands.md +++ /dev/null @@ -1,544 +0,0 @@ -# Commands - -Commands are the heart of stateful testing. Each command represents a single operation you can perform on your system - like opening a door, adding an item to a cart, or incrementing a counter. - -Hedgehog then uses these individual actions (commands) to build up valid sequences that simulate client's behaviour. - -This page dives deep into the `Command` interface, explaining how commands work, when they execute, and how to use state to chain operations together. - -## Understanding State - -Before diving into commands, you need to understand how state works in stateful testing. - -State is shared throughout the lifecycle of testing: first during **sequence generation** (when Hedgehog builds up a series of commands to execute), and then during **sequence execution** (when those commands actually run against your system). - -The key insight is that some parts of the state can be known during generation, while others only become known during execution: - -- **Known at generation time**: When generating a sequence that includes `LockDoorCommand`, we know the door will be "Locked" for the next action in the sequence - even before executing anything. This is **concrete state**. - -- **Known only at execution time**: If the system returns a lock code when the door is locked, we know *that a code exists* during generation, but the actual value is only available after execution. This is **symbolic state**. - -We represent concrete state using regular properties (like `bool IsLocked`), and symbolic state using the `Var` type (like `Var LockCode`). - -Here's an example of a door state that combines both: - -# [F#](#tab/fsharp) - -```fsharp -type DoorState = { - IsLocked: bool // Concrete: we know immediately after LockDoor - LockCode: Var // Symbolic: actual code only known after execution -} -``` - -# [C#](#tab/csharp) - -```csharp -public record DoorState -{ - public bool IsLocked { get; init; } // Concrete: we know immediately after LockDoor - public Var LockCode { get; init; } // Symbolic: actual code only known after execution -} -``` - ---- - -**The key rule:** At generation time, you can only access the **concrete parts** of the state. You cannot resolve symbolic variables because execution hasn't happened yet! - -## The Command Interface - -Every command inherits from `Command` and implements these methods: - -# [F#](#tab/fsharp) - -```fsharp -type MyCommand() = - inherit Command() - - // 1. Name for reporting - override _.Name = "MyCommand" - - // 2. Should this command be generated in this state? - override _.Precondition(state) = true - - // 3. Generate input for this command - override _.Generate(state) = - Gen.int32 (Range.linear 0 100) - - // 4. Should we execute this command with these inputs? - override _.Require(env, state, input) = true - - // 5. Execute the real operation - override _.Execute(sut, env, state, input) = - let result = sut.DoSomething(input) - Task.FromResult(result) - - // 6. Update the model state - override _.Update(state, input, outputVar) = - { state with Value = outputVar } - - // 7. Verify the result is correct - override _.Ensure(env, oldState, newState, input, output) = - // Check output matches expectations - true -``` - -# [C#](#tab/csharp) - -```csharp -public class MyCommand : Command -{ - // 1. Name for reporting - public override string Name => "MyCommand"; - - // 2. Should this command be generated in this state? - public override bool Precondition(MyState state) => true; - - // 3. Generate input for this command - public override Gen Generate(MyState state) => - Gen.Int32(Range.LinearInt32(0, 100)); - - // 4. Should we execute this command with these inputs? - public override bool Require(Env env, MyState state, MyInput input) => true; - - // 5. Execute the real operation - public override Task Execute(MySystem sut, Env env, MyState state, MyInput input) - { - var result = sut.DoSomething(input); - return Task.FromResult(result); - } - - // 6. Update the model state - public override MyState Update(MyState state, MyInput input, Var outputVar) => - state with { Value = outputVar }; - - // 7. Verify the result is correct - public override bool Ensure(Env env, MyState oldState, MyState newState, MyInput input, MyOutput output) => - // Check output matches expectations - true; -} -``` - ---- - -Let's understand each piece and how they work together. - -### Understanding Env - -The `Env` (environment) is a key concept that allows you to resolve symbolic state values into concrete values, giving you access to the real execution-time values. - -**Methods with Env** (can resolve symbolic values): -- `Require` - Check preconditions using actual runtime values -- `Execute` - Perform operations using resolved values -- `Ensure` - Verify results using actual values - -**Methods without Env** (can only access concrete state): -- `Generate` - Only has access to structural/concrete state -- `Update` - Works with symbolic variables, doesn't resolve them - -During sequence generation, symbolic values don't have concrete runtime values yet, so `Generate` and `Update` cannot receive an `Env`. However, during execution, `Require`, `Execute`, and `Ensure` all receive an `Env` that lets you resolve any `Var` to its actual runtime value. - -## The Command Lifecycle - -When Hedgehog builds and executes a test sequence, each command goes through these stages: - -**During Generation:** -```text -1. Precondition → Should we include this command? (check concrete state only - no Env) -2. Generate → Generate input for this command (only called if Precondition returns true) -3. Update → Update model state symbolically (enables next command's Precondition check) -``` - -**During Execution:** -```text -1. Require → Can we execute it now? (has Env - can resolve symbolic values) -2. Execute → Run the operation on the real system -3. Update → Update model state symbolically (same call as generation, now env has real values) -4. Ensure → Verify the result matches our expectations -``` - -### 1. Precondition: Deciding Whether to Generate - -**When it runs:** During test *generation*, before execution - -**Purpose:** Decide whether this command makes sense based on the **concrete structure** of the state - -**Returns:** `true` to include the command (and call `Generate`), `false` to skip this command - -**Critical:** You can only access concrete parts of the state here. No `Env` means no resolving symbolic variables! - -For example, checking a simple boolean: - -# [F#](#tab/fsharp) - -```fsharp -type DoorState = { - IsLocked: bool // Concrete value we can check -} - -type KnockKnockDoorCommand() = - inherit Command() - - override _.Name = "KnockKnock" - - override _.Precondition(state) = - // Check concrete state directly - no Env needed! - state.IsLocked // Only generate when door is locked - - override _.Generate(state) = - // Generate the number of knocks - Gen.int32 (Range.linear 1 5) -``` - -# [C#](#tab/csharp) - -```csharp -public record DoorState -{ - public bool IsLocked { get; init; } // Concrete value we can check -} - -public class KnockKnockDoorCommand : Command -{ - public override string Name => "KnockKnock"; - - public override bool Precondition(DoorState state) - { - // Check concrete state directly - no Env needed! - return state.IsLocked; // Only generate when door is locked - } - - public override Gen Generate(DoorState state) - { - // Generate the number of knocks - return Gen.Int32(Range.LinearInt32(1, 5)); - } -} -``` - ---- - -**Key insight:** At generation time, you only know the *structure* - "the door is locked", "the stack has 3 items" - but not the actual values like "the lock code is 1234" or "the top item is 42". Those require execution. - -### 2. Generate: Creating Command Input - -**When it runs:** During test *generation*, after `Precondition` returns `true` - -**Purpose:** Generate random input for this command - -**Returns:** A `Gen` generator that produces input values - -**Important:** This is only called when `Precondition` returns `true`, so you can assume the structural preconditions are already satisfied. - -### 3. Require: Runtime Precondition Check - -**When it runs:** Just before execution, after the sequence is generated - -**Purpose:** Verify that the command can still be executed with these specific inputs. - -**Returns:** `true` to proceed with execution, `false` to skip this command (the test continues with remaining commands) - -**Important:** Returning `false` does NOT fail the test - it simply skips the command. This is different from `Ensure`, which validates correctness. - -**Key difference from Precondition:** `Require` DOES receive an `Env` parameter, so it CAN resolve symbolic variables! This is where you check concrete runtime values that weren't known during generation. - -**When you need it:** The most common case is when your `Generate` method returns `Var` as part of the input (e.g., picking from a list of symbolic IDs). Since previous commands can be skipped, those symbolic variables might not be bound at execution time. Override `Require` to check if such variables can actually be resolved before attempting to use them. - -> **💡 Tip:** For a detailed explanation of when and how to use `Require`, including complete examples with symbolic variables in inputs, see [Runtime Preconditions](require.md). - -**In practice:** The default `Require` implementation returns `true`, which works for most commands that don't use symbolic variables as input. - -### 4. Execute: Running the Real Operation - -**When it runs:** During test execution - -**Purpose:** Perform the actual operation on your system under test - -**Returns:** A `Task` with the result - -This is straightforward - call your system's method and return the result: - -# [F#](#tab/fsharp) - -```fsharp -override _.Execute(sut, env, state, input) = - let result = sut.IncrementCounter() - Task.FromResult(result) -``` - -# [C#](#tab/csharp) - -```csharp -public override Task Execute(Counter sut, Env env, CounterState state, bool input) -{ - var result = sut.Increment(); - return Task.FromResult(result); -} -``` - ---- - -**Important:** The `Execute` method receives: -- `sut`: Your system under test (the real object) -- `env`: The environment with resolved values from previous commands -- `state`: The current model state -- `input`: The generated input for this command - -Use `env` to resolve any symbolic variables you need from the state: - -# [F#](#tab/fsharp) - -```fsharp -override _.Execute(sut, env, state, input) = - let code = state.LockCode.Resolve(env) - sut.UnlockDoorAsync(code, input) -``` - -# [C#](#tab/csharp) - -```csharp -public override Task Execute(DoorState sut, Env env, CartState state, string input) -{ - var code = state.LockCode.Resolve(env); - return sut.UnlockDoorAsync(code, input); -} -``` - ---- - -### 5. Update: Tracking Symbolic State - -**When it runs:** During *both* generation **and** execution phases - after each command in the sequence - -**Purpose:** Update your model state with the new symbolic output to evolve the structural state - -**Returns:** The new state - -**Critical insight:** `Update` is called during *generation* (before any real execution happens) to maintain the structural state. -This allows subsequent commands in the sequence to evaluate their `Precondition` based on the evolved state. -During *execution*, these variables are bound to actual runtime values in the `Env`. - -This is where you store the command's output as a **symbolic variable** (`Var`) that future commands can reference: - -# [F#](#tab/fsharp) - -```fsharp -override _.Update(state, input, outputVar) = - { state with CurrentCount = outputVar } -``` - -# [C#](#tab/csharp) - -```csharp -public override CounterState Update(CounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; -``` - ---- - -The `outputVar` is a symbolic reference to this command's output. Later commands can resolve it to get the actual value. - -#### Projecting Fields from Structured Outputs - -When a command returns a structured type (like a record or class), you often want to store individual fields in your state rather than the entire object. Use `Var.map` (F#) or `.Select()` (C#) to project fields from the output: - -# [F#](#tab/fsharp) - -```fsharp -// Command that returns a structured Person type -type Person = { - Name: string - Age: int -} - -type RegistryState = { - LastPersonName: Var - LastPersonAge: Var -} - -type AddPersonCommand() = - inherit Command() - - override _.Execute(sut, env, state, (name, age)) = - let person = sut.AddPerson(name, age) - Task.FromResult(person) - - // Project individual fields from the Person output - override _.Update(state, input, personVar) = - { LastPersonName = Var.map (fun p -> p.Name) personVar - LastPersonAge = Var.map (fun p -> p.Age) personVar } -``` - -# [C#](#tab/csharp) - -```csharp -// Command that returns a structured Person type -public record Person(string Name, int Age); - -public record RegistryState -{ - public Var LastPersonName { get; init; } - public Var LastPersonAge { get; init; } -} - -public class AddPersonCommand : Command -{ - public override Task Execute(PersonRegistry sut, Env env, RegistryState state, (string, int) input) - { - var (name, age) = input; - var person = sut.AddPerson(name, age); - return Task.FromResult(person); - } - - // Project individual fields from the Person output - public override RegistryState Update(RegistryState state, (string, int) input, Var personVar) => - state with - { - LastPersonName = personVar.Select(p => p.Name), - LastPersonAge = personVar.Select(p => p.Age) - }; -} -``` - ---- - -**How it works:** Both projected variables (`LastPersonName` and `LastPersonAge`) share the same underlying variable name - they point to the same `Person` object in the environment. When you resolve them, the projection function is applied to extract the specific field. - -**You can chain projections:** - -# [F#](#tab/fsharp) - -```fsharp -override _.Update(state, input, personVar) = - let nameVar = Var.map (fun p -> p.Name) personVar - let nameLengthVar = Var.map String.length nameVar - { state with NameLength = nameLengthVar } -``` - -# [C#](#tab/csharp) - -```csharp -public override RegistryState Update(RegistryState state, (string, int) input, Var personVar) -{ - var nameVar = personVar.Select(p => p.Name); - var nameLengthVar = nameVar.Select(name => name.Length); - return state with { NameLength = nameLengthVar }; -} -``` - ---- - -This is particularly useful when you need to pass different parts of a command's output to different subsequent commands. - -### 6. Ensure: Verifying Correctness - -**When it runs:** After execution and state update - -**Purpose:** Assert that the output matches expectations - -**Returns:** `true` if the assertion passes, `false` or throw an exception if it fails - -This is your postcondition check: - -# [F#](#tab/fsharp) - -```fsharp -override _.Ensure(env, oldState, newState, input, output) = - let oldCount = oldState.CurrentCount.Resolve(env) - output = oldCount + 1 // Increment should increase by exactly 1 -``` - -# [C#](#tab/csharp) - -```csharp -public override bool Ensure(Env env, CounterState oldState, CounterState newState, bool input, int output) -{ - var oldCount = oldState.CurrentCount.Resolve(env); - return output == oldCount + 1; // Increment should increase by exactly 1 -} -``` - ---- - -You can also throw exceptions for more detailed error messages: - -# [F#](#tab/fsharp) - -```fsharp -override _.Ensure(env, oldState, newState, input, output) = - let oldCount = oldState.CurrentCount.Resolve(env) - if output <> oldCount + 1 then - failwith $"Expected {oldCount + 1}, got {output}" - true -``` - -# [C#](#tab/csharp) - -```csharp -public override bool Ensure(Env env, CounterState oldState, CounterState newState, bool input, int output) -{ - var oldCount = oldState.CurrentCount.Resolve(env); - Assert.Equal(output, oldCount + 1); - return true; -} -``` - ---- - - -## Commands Without Outputs - -Sometimes operations don't return meaningful values - they just perform side effects. For these, use `ActionCommand`: - -# [F#](#tab/fsharp) - -```fsharp -type CloseConnectionCommand() = - inherit ActionCommand() - - override _.Name = "CloseConnection" - - override _.Precondition(state) = true - - override _.Generate(state) = - Gen.constant () - - override _.Execute(sut, env, state, input) = - sut.CloseConnection() - Task.CompletedTask // No return value - - override _.Update(state, input) = - { state with IsConnected = false } // No output var - - override _.Ensure(env, oldState, newState, input) = - // Verify side effect without checking output - true -``` - -# [C#](#tab/csharp) - -```csharp -public class CloseConnectionCommand : ActionCommand -{ - public override string Name => "CloseConnection"; - - public override bool Precondition(DbState state) => true; - - public override Gen Generate(DbState state) => - Gen.Constant(NoInput.Value); - - public override Task Execute(Database sut, Env env, DbState state, NoInput input) - { - sut.CloseConnection(); - return Task.CompletedTask; // No return value - } - - public override DbState Update(DbState state, NoInput input) => - state with { IsConnected = false }; // No output var - - public override bool Ensure(Env env, DbState oldState, DbState newState, NoInput input) => - true; -} -``` - ---- diff --git a/docs/stateful/complete-example.md b/docs/stateful/complete-example.md deleted file mode 100644 index e6cc7908..00000000 --- a/docs/stateful/complete-example.md +++ /dev/null @@ -1,597 +0,0 @@ -# Complete Example: Testing a Counter - -This walkthrough will guide you through building a complete stateful test from scratch. We'll test a simple `Counter` class with increment, decrement, and reset operations. - -## The System Under Test (SUT) - -Let's start with a simple counter implementation: - -# [F#](#tab/fsharp) - -```fsharp -type Counter() = - let mutable value = 0 - - member _.Increment() = value <- value + 1 - member _.Decrement() = value <- value - 1 - member _.Reset() = value <- 0 - member _.Get() = value -``` - -# [C#](#tab/csharp) - -```csharp -public sealed class Counter -{ - private int _value; - - public void Increment() => _value++; - public void Decrement() => _value--; - public void Reset() => _value = 0; - public int Get() => _value; -} -``` - ---- - -This is our **System Under Test** (SUT). It maintains state (the current count) and provides operations that modify that state. - -## The Model State - -To test our counter, we need a model that represents what we *expect* the counter's state to be. Since our counter has a single integer value, our model is simple: - -# [F#](#tab/fsharp) - -```fsharp -type CounterState = { - CurrentCount: Var // Symbolic reference to the counter's value -} -``` - -# [C#](#tab/csharp) - -```csharp -public record CounterState -{ - public required Var CurrentCount { get; init; } -} -``` - ---- - -The `Var` is a **symbolic variable**—it represents "the value that operation X returned." This lets us track relationships between operations even before we know their concrete values. - -## Defining Commands - -Now we'll define each operation as a **Command**. - -Each command inherits from `Command` where: -- `TSystem` is our system under test type (`Counter`) -- `TState` is our model state type (`CounterState`) -- `TInput` is the input parameter type for this command -- `TOutput` is what the command returns - -### The Increment Command - -# [F#](#tab/fsharp) - -```fsharp -type IncrementCommand() = - inherit Command() - - // Name for debugging/shrinking output - override _.Name = "Increment" - - // Always allow this command - override _.Precondition(state) = true - - // Execute the real operation on the SUT - override _.Execute(counter, env, state, input) = - counter.Increment() - let result = counter.Get() - Task.FromResult(result) - - // Generate inputs (none needed for increment) - override _.Gen(state) = Gen.constant () - - // Update our model state with the new value - override _.Update(state, input, outputVar) = { CurrentCount = outputVar } - - // Assert the result is correct - override _.Ensure(env, oldState, newState, input, result) = - let oldCount = oldState.CurrentCount.Resolve(env) - result = oldCount + 1 -``` - -# [C#](#tab/csharp) - -```csharp -public class IncrementCommand : Command -{ - // Name for debugging/shrinking output - public override string Name => "Increment"; - - // Always allow this command - public override bool Precondition(CounterState state) => true; - - // Execute the real operation on the SUT - public override Task Execute(Counter sut, Env env, CounterState state, NoInput input) - { - sut.Increment(); - var result = sut.Get(); - return Task.FromResult(result); - } - - // Generate inputs (none needed for increment) - public override Gen Generate(CounterState state) => - Gen.Constant(NoInput.Value); - - // Update our model state with the new value - public override CounterState Update(CounterState state, NoInput input, Var outputVar) => - state with { CurrentCount = outputVar }; - - // Assert the result is correct - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoInput input, int result) - { - var oldCount = oldState.CurrentCount.Resolve(env); - return result == oldCount + 1; - } -} -``` - ---- - -Let's break down each method: - -1. **Name**: Used in test output to show which command failed -2. **Precondition**: Determines if this command can be generated in the current state (always `true` for simple commands) -3. **Execute**: Runs the actual operation and returns the new count -4. **Gen**: Generates random inputs (we use `unit` in F# or `NoInput` in C# since increment needs no meaningful input) -5. **Update**: Takes the output and creates the new model state -6. **Ensure**: Verifies the result is what we expected (old count + 1) - -### The Decrement Command - -The decrement command is almost identical: - -# [F#](#tab/fsharp) - -```fsharp -type DecrementCommand() = - inherit Command() - - override _.Name = "Decrement" - - override _.Precondition(state) = true - - override _.Execute(counter, env, state, input) = - counter.Decrement() - let result = counter.Get() - Task.FromResult(result) - - override _.Gen _ = Gen.constant () - - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(env, oldState, newState, input, result) = - let oldCount = oldState.CurrentCount.Resolve(env) - result = oldCount - 1 // Should decrease by 1 -``` - -# [C#](#tab/csharp) - -```csharp -public class DecrementCommand : Command -{ - public override string Name => "Decrement"; - - public override bool Precondition(CounterState state) => true; - - public override Task Execute(Counter sut, Env env, CounterState state, NoInput input) - { - sut.Decrement(); - var result = sut.Get(); - return Task.FromResult(result); - } - - public override Gen Generate(CounterState state) => - Gen.Constant(NoInput.Value); - - public override CounterState Update(CounterState state, NoInput input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoInput input, int result) - { - var oldCount = oldState.CurrentCount.Resolve(env); - return result == oldCount - 1; // Should decrease by 1 - } -} -``` - ---- - -### The Reset Command - -Reset is interesting because it doesn't depend on the previous state: - -# [F#](#tab/fsharp) - -```fsharp -type ResetCommand() = - inherit Command() - - override _.Name = "Reset" - - override _.Precondition(state) = true - - override _.Execute(counter, env, state, input) = - counter.Reset() - let result = counter.Get() - Task.FromResult(result) - - override _.Gen(state) = Gen.constant () - override _.Update(state, input, outputVar) = { CurrentCount = outputVar } - override _.Ensure(env, oldState, newState, input, result) = result = 0 -``` - -# [C#](#tab/csharp) - -```csharp -public class ResetCommand : Command -{ - public override string Name => "Reset"; - - public override bool Precondition(CounterState state) => true; - - public override Task Execute(Counter sut, Env env, CounterState state, NoInput input) - { - sut.Reset(); - var result = sut.Get(); - return Task.FromResult(result); - } - - public override Gen Generate(CounterState state) => - Gen.Constant(NoInput.Value); - - public override CounterState Update(CounterState state, NoInput input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoInput input, int result) => - result == 0; // Reset always returns 0 -} -``` - ---- - -### A Get Command (for completeness) - -Let's add a read-only operation to verify our model stays in sync: - -# [F#](#tab/fsharp) - -```fsharp -type GetCommand() = - inherit Command() - - override _.Name = "Get" - - override _.Precondition(state) = true - - override _.Execute(counter, env, state, input) = - Task.FromResult(counter.Get()) - - override _.Gen(state) = Gen.constant () - - override _.Update(state, input, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(env, oldState, newState, input, result) = - // Get should return exactly what's in our model - result = oldState.CurrentCount.Resolve(env) -``` - -# [C#](#tab/csharp) - -```csharp -public class GetCommand : Command -{ - public override string Name => "Get"; - - public override bool Precondition(CounterState state) => true; - - public override Task Execute(Counter sut, Env env, CounterState state, NoInput input) => - Task.FromResult(sut.Get()); - - public override Gen Generate(CounterState state) => - Gen.Constant(NoInput.Value); - - public override CounterState Update(CounterState state, NoInput input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoInput input, int result) - { - // Get should return exactly what's in our model - return result == oldState.CurrentCount.Resolve(env); - } -} -``` - ---- - -## Creating the Specification - -Now we tie it all together with a `SequentialSpecification`: - -# [F#](#tab/fsharp) - -```fsharp -type CounterSpec() = - inherit SequentialSpecification() - - // Start each test from 0 - override _.SetupCommands = [| ResetCommand() |] - - // The initial model state - override _.InitialState = { CurrentCount = Var.symbolic 0 } - - // How many commands to generate (1-50) - override _.Range = Range.linear 1 50 - - // All available commands - override _.Commands = [| - IncrementCommand() - DecrementCommand() - ResetCommand() - GetCommand() - |] -``` - -# [C#](#tab/csharp) - -```csharp -public class CounterSpec : SequentialSpecification -{ - // Start each test from 0 - public override ICommand[] SetupCommands => - [new ResetCommand()]; - - // The initial model state - public override CounterState InitialState => - new() { CurrentCount = Var.Symbolic(0) }; - - // How many commands to generate (1-50) - public override Range Range => - Hedgehog.Linq.Range.LinearInt32(1, 50); - - // All available commands - public override ICommand[] Commands => - [ - new IncrementCommand(), - new DecrementCommand(), - new ResetCommand(), - new GetCommand() - ]; -} -``` - ---- - -## Running the Test - -Finally, we write our test: - -# [F#](#tab/fsharp) - -```fsharp -[] -let ``Counter behaves correctly under random operations``() = - let sut = Counter() - CounterSpec().ToProperty(sut).Check() -``` - -# [C#](#tab/csharp) - -```csharp -[Fact] -public void CounterBehavesCorrectlyUnderRandomOperations() -{ - var sut = new Counter(); - new CounterSpec().ToProperty(sut).Check(); -} -``` - ---- - -That's it! When you run this test, Hedgehog will: - -1. Generate random sequences of commands (e.g., "Increment, Increment, Reset, Decrement, Get") -2. Execute each sequence against your actual counter -3. Verify each operation produces the expected result -4. If any assertion fails, shrink the sequence to find the minimal failing case - -### Example Test Scenarios - -Here are some sequences Hedgehog might generate: - -**Simple sequence:** -``` -1. Reset → expect 0 -2. Increment → expect 1 -3. Increment → expect 2 -4. Get → expect 2 -``` - -**Edge case:** -``` -1. Reset → expect 0 -2. Decrement → expect -1 -3. Decrement → expect -2 -4. Reset → expect 0 -5. Get → expect 0 -``` - -**Complex sequence:** -``` -1. Increment → expect 1 -2. Increment → expect 2 -3. Decrement → expect 1 -4. Increment → expect 2 -5. Reset → expect 0 -6. Increment → expect 1 -``` - -If any command returns an unexpected value, Hedgehog will report exactly which sequence caused the failure and shrink it to the smallest reproduction case. - -## Testing new behaviours - -Let's assume that now `Counter` adds a new API method `Set`: - -# [F#](#tab/fsharp) - -```fsharp -type Counter() = - member _.Set(n: int) = value <- n - // the rest of the members -``` - -# [C#](#tab/csharp) - -```csharp -public sealed class Counter -{ - public void Set(int n) => _value = n; - // the rest of the members -} - -``` - ---- - -To test it we need to define some `SetCommand`: - -# [F#](#tab/fsharp) - -```fsharp -type SetCommand() = - inherit Command() - - override _.Name = "Set" - - override _.Precondition(state) = true - - override _.Execute(counter, _, value) = - counter.Set(value) - let result = counter.Get() - Task.FromResult(result) - - // Generate random integers between -10 and 100 - override _.Gen _ = Gen.int32 (Range.linearFrom 0 -10 100) - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - override _.Ensure(_, _, _, input, result) = result = input -``` - -# [C#](#tab/csharp) - -```csharp -public class SetCommand : Command -{ - public override string Name => "Set"; - - public override bool Precondition(CounterState state) => true; - - public override Task Execute(Counter sut, Env env, int value) - { - sut.Set(value); - var result = sut.Get(); - return Task.FromResult(result); - } - - // Generate random integers between -10 and 100 - public override Gen Generate(CounterState state) => - Hedgehog.Linq.Gen.Int32(Range.LinearFromInt32(0, -10, 100)); - - public override CounterState Update(CounterState state, int input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, int input, int result) - { - return result == input; // Set should set the exact value - } -} -``` - ---- - -Then add `SetCommand()` to your `Commands` array in the specification. - -Now Hedgehog will use it in generating sequence and will generate sequences like: -``` -1. Set(42) → expect 42 -2. Increment → expect 43 -3. Set(-5) → expect -5 -4. Get → expect -5 -``` - -## What About Bugs? - -Let's introduce a bug in our counter to see what happens: - -# [F#](#tab/fsharp) - -```fsharp -member _.Decrement() = - if value > 10 then value <- value - 1 - else value <- value - 2 // SIMULATE BUG: decrements by 2 when <= 10 -``` - -# [C#](#tab/csharp) - -```csharp -public void Decrement() -{ - if (_value > 10) _value--; - else _value -= 2; // SIMULATE BUG: decrements by 2 when <= 10 -} -``` - ---- - -When you run the test, Hedgehog will find this bug and report something like: - -``` -*** Failed! Falsifiable (after 8 tests and 1 shrink): - -You can reproduce this failure with the following Recheck Seed: - "7_13402950062986702852_14277380902303697685_0" - -Generated values: - { Initial = CounterState { CurrentCount = 0 (symbolic) } - Steps = [Reset ; Decrement ] } - -Counterexamples: - Final state: CounterState { CurrentCount = 0 (symbolic) } - + Reset - Decrement -``` - -Hedgehog automatically found the minimal reproduction case: decrement once -(you can see "`+ Reset`" in the list because `Reset` is defined as a Setup step and is always executed first). - - - -## Summary - -You've learned how to: - -1. **Define a model state** that represents what you expect -2. **Create commands** for each operation on your SUT -3. **Implement the key methods** for each command: - - `Name`: for debugging - - `Precondition`: to control when the command can be generated - - `Gen`: to generate inputs - - `Execute`: to run the real operation - - `Update`: to update the model state - - `Ensure`: to verify correctness -4. **Create a specification** that ties everything together -5. **Run the test** and let Hedgehog find bugs automatically - -The beauty of this approach is that Hedgehog explores hundreds or thousands of different sequences automatically, finding edge cases you might never think to test manually. diff --git a/docs/stateful/index.md b/docs/stateful/index.md deleted file mode 100644 index a91b2262..00000000 --- a/docs/stateful/index.md +++ /dev/null @@ -1,122 +0,0 @@ -# What is stateful testing? - -Most property-based tests check individual operations in isolation: "if I sort this list, is it actually sorted?" But real systems have state that changes over time. A user logs in, makes changes, logs out. A door locks and unlocks. A shopping cart adds and removes items. - -**Stateful testing** lets you test sequences of actions on systems that maintain state. - -Instead of testing one operation at a time, you define each possible action as a **Command**. Hedgehog then generates random sequences of these commands - essentially, complete scenarios of how your system might be used. When something goes wrong, Hedgehog automatically shrinks both the sequence of actions *and* their parameters to find you the minimal failing case. - -Imagine testing a login system. Instead of manually writing test cases like "login, then logout" or "login, change password, logout," Hedgehog generates hundreds of different sequences and finds edge cases you never thought of—like what happens when you try to change a password twice in a row, or logout when already logged out. - -## Building blocks: Commands - -Let's build up the idea step by step. We'll use pseudocode to focus on concepts rather than specific syntax. - -#### Step 1: Naming your command - -Every command needs a name for clarity: - -```javascript -Command { - Name: "LogIn" -} -``` - -#### Step 2: Defining preconditions - -Here's where stateful testing gets interesting. Not all commands make sense at all times. You can't log out if you're not logged in. You can't lock a door that's already locked. - -We track this with a **model state**—a simple state representing what we know from interacting with the system. Commands can check this state and decide whether they're allowed to run: - -```javascript -Command { - Name: "LogOut" - - Precondition(currentState): - currentState.isLoggedIn // Only generate when logged in -} -``` - -This way, Hedgehog only generates valid sequences. The `LogOut` command appears only when the user is logged in (when `Precondition` returns true). The `LockDoor` command appears only when the door is unlocked. - -#### Step 3: Generating command inputs - -Just like regular property tests, commands need test data. Each command defines how to generate its input: - -```javascript -Command { - Name: "LogIn" - Precondition(currentState): currentState.isLoggedIn - - Generate(currentState): generateRandomUsername() -} -``` - -#### Step 4: Executing the command - -Now we need to actually *run* the command against the real system: - -```javascript -Command { - Name: "LogIn" - Precondition(currentState): currentState.isLoggedIn - Generate(currentState): generateRandomUsername() - - Execute(input): - actualSystem.login(input.username) -} -``` - -The `Execute` method takes the generated input and performs the actual operation, returning whatever the system returns. - -#### Step 5: Updating the model state - -After executing a command, we need to update our model state to reflect what happened: - -```javascript -Command { - Name: "LogIn" - Precondition(currentState): currentState.isLoggedIn - Generate(currentState): generateRandomUsername() - Execute(input): actualSystem.login(input.username) - - UpdateState(oldState, input, output): - oldState with { isLoggedIn: true, username: input.username } -} -``` - -This method takes the old state, the input we used, and the output we got, and produces the new state. - -#### Step 6: Making assertions - -Finally, we need to verify that the system behaved correctly. The `Ensure` method checks whether everything went as expected: - -```javascript -Command { - Name: "LogIn" - Precondition(currentState): currentState.isLoggedIn - Generate(currentState): generateRandomUsername() - Execute(input): actualSystem.login(input.username) - UpdateState(oldState, input, output): - oldState with { isLoggedIn: true, username: input.username } - - Ensure(oldState, newState, input, output): - assert output.success == true - assert output.username == input.username -} -``` - -With both states available, you can make rich assertions: "after logging in, the user should be logged in," "after adding an item, the cart count should increase by one," and so on. - -## Putting it all together - -Define all your commands (LogIn, LogOut, ChangePassword, etc.), and Hedgehog will: - -1. Generate random sequences of commands -2. Check preconditions to ensure valid sequences -3. Execute each command against your real system -4. Update the model state after each command -5. Assert that everything worked correctly -6. If something fails, shrink the sequence to find the minimal reproduction case - -You get comprehensive testing of complex stateful scenarios with minimal effort, and when bugs appear, you get a short, clear sequence showing exactly how to reproduce them. diff --git a/docs/stateful/require.md b/docs/stateful/require.md deleted file mode 100644 index 258f0b20..00000000 --- a/docs/stateful/require.md +++ /dev/null @@ -1,280 +0,0 @@ -# Runtime Preconditions with Require - -When you generate a test sequence, Hedgehog creates a plan of actions to execute. But what happens when that plan includes references to values that might not exist when execution time arrives? - -This is where the `Require` method becomes essential. - -## The Problem: Symbolic Variables as Input - -Consider a user registry system where commands can look up previously registered users. Your state might track registered user IDs: - -# [F#](#tab/fsharp) - -```fsharp -type RegistryState = { - RegisteredIds: Var list // List of IDs from previous Register commands -} -``` - -# [C#](#tab/csharp) - -```csharp -public record RegistryState -{ - public List> RegisteredIds { get; init; } = new(); -} -``` - ---- - -When generating a `LookupUser` command, you need to pick an ID from this list: - -# [F#](#tab/fsharp) - -```fsharp -type LookupUserCommand() = - inherit Command, UserInfo option>() - - override _.Precondition(state) = - not (List.isEmpty state.RegisteredIds) - - override _.Generate(state) = - Gen.item state.RegisteredIds // Returns a Var from the list -``` - -# [C#](#tab/csharp) - -```csharp -public class LookupUserCommand : Command, UserInfo?> -{ - public override bool Precondition(RegistryState state) => - state.RegisteredIds.Count > 0; - - public override Gen> Generate(RegistryState state) => - Gen.Element(state.RegisteredIds); // Returns a Var from the list -} -``` - ---- - -**Notice:** `Generate` returns a `Var` - a symbolic reference to an ID that some previous command produced. - -### The Hidden Danger: Shrinking Can Leave Variables Unbound - -Here's the subtle problem. Imagine Hedgehog generates this sequence (which passes): - -```text -1. RegisterUser("Alice") → Var₁ -2. RegisterUser("Bob") → Var₂ -3. RegisterUser("Charlie") → Var₃ -4. LookupUser(Var₂) ← succeeds -5. DeleteUser(Var₃) -6. SomeOtherOperation() ← THIS FAILS! -``` - -The test fails at step 6. Now Hedgehog tries to **shrink** the sequence to find the minimal failing case. It might try removing step 2: - -```text -1. RegisterUser("Alice") → Var₁ - [step 2 removed - "Bob" never registered] -3. RegisterUser("Charlie") → Var₃ -4. LookupUser(Var₂) ← CRASH! Var₂ is unbound -5. DeleteUser(Var₃) -6. SomeOtherOperation() -``` - -**What happened?** - -- When step 4 was originally generated, the state had `[Var₁, Var₂]` in `RegisteredIds` -- `Generate` picked `Var₂` randomly from that list -- During shrinking, step 2 (which produced `Var₂`) was removed -- Step 4 still has `Var₂` as its input, but `Var₂` was never bound to a concrete value -- Without `Require`, calling `Var₂.Resolve(env)` will throw an exception - -This isn't a problem with the test logic—it's a fundamental aspect of how shrinking works. Actions are removed from sequences, but the inputs to remaining actions are fixed when they're generated. - -**The fix:** Override `Require` to check `idVar.TryResolve(env, out var _)`. During shrinking, if the var can't be resolved, `Require` returns `false` and the action is skipped (not failed). The shrinking process continues and finds a valid minimal sequence. - -## The Solution: Override Require - -The `Require` method is your runtime safety check. Unlike `Precondition` (which only sees the structural state during generation), `Require` receives the `Env` parameter and can resolve symbolic variables to check if they're actually valid. - -Here's the safe version: - -# [F#](#tab/fsharp) - -```fsharp -type LookupUserCommand() = - inherit Command, UserInfo option>() - - override _.Name = "LookupUser" - - // Structural precondition: we need at least one ID in our list - override _.Precondition(state) = - not (List.isEmpty state.RegisteredIds) - - // Pick a random ID from the list - override _.Generate(state) = - Gen.item state.RegisteredIds - - // Runtime check: can we actually resolve this ID? - override _.Require(env, state, idVar) = - idVar |> Var.tryResolve env |> Result.isOk - - override _.Execute(registry, env, state, idVar) = - let actualId = idVar.Resolve(env) - Task.FromResult(registry.Lookup(actualId)) - - override _.Ensure(env, oldState, newState, idVar, result) = - result.IsSome // Should always find the user -``` - -# [C#](#tab/csharp) - -```csharp -public class LookupUserCommand : Command, UserInfo?> -{ - public override string Name => "LookupUser"; - - // Structural precondition: we need at least one ID in our list - public override bool Precondition(RegistryState state) => - state.RegisteredIds.Count > 0; - - // Pick a random ID from the list - public override Gen> Generate(RegistryState state) => - Gen.Element(state.RegisteredIds); - - // Runtime check: can we actually resolve this ID? - public override bool Require(Env env, RegistryState state, Var idVar) => - idVar.TryResolve(env, out var _); // Returns false if not bound yet - - public override Task Execute(UserRegistry sut, Env env, RegistryState state, Var idVar) - { - var actualId = idVar.Resolve(env); - return Task.FromResult(sut.Lookup(actualId)); - } - - public override bool Ensure(Env env, RegistryState oldState, RegistryState newState, Var idVar, UserInfo? result) => - result is not null; // Should always find the user -} -``` - ---- - -**What changes:** - -1. We override `Require` to check if `idVar` can actually be resolved -2. If `TryResolve` returns `false`, the command is **skipped** (not failed!) -3. The test continues with the remaining actions - -This prevents trying to lookup a user ID that was never actually created. - -## When to Override Require - -**Override `Require` when:** - -1. **Your `Generate` returns `Var` as part of the input** - You're selecting from a list of symbolic variables -2. **Commands can be skipped** - Previous commands might not execute, leaving vars unbound -3. **You need runtime value checks** - Validate concrete values that weren't available during generation - -**You can skip `Require` when:** - -1. **`Generate` returns concrete values only** - No symbolic variables in the input -2. **Simple preconditions** - Structural checks that `Precondition` already handles -3. **All commands always execute** - No risk of skipped actions (rare in practice) - -## Best Practices - -### 1. Use TryResolve for Safety - -Don't use `Resolve` directly in `Require` - it throws if the variable isn't bound. - -In F#, use the idiomatic `Var.tryResolve` which returns a `Result`: - -# [F#](#tab/fsharp) - -```fsharp -override _.Require(env, state, input) = - input.SomeVarField |> Var.tryResolve env |> Result.isOk -``` - -# [C#](#tab/csharp) - -In C#, use `TryResolve` with an out parameter: - -```csharp -public override bool Require(Env env, MyState state, MyInput input) => - input.SomeVarField.TryResolve(env, out var _); -``` - ---- - -### 2. Check the Symbolic Inputs You Use - -If your command's input contains `Var` fields that come from previous command outputs, and your `Execute` method will resolve them, you should check those in `Require`: - -# [F#](#tab/fsharp) - -```fsharp -type TransferInput = { - FromAccount: Var // From a previous CreateAccount command - ToAccount: Var // From a previous CreateAccount command - Amount: decimal -} - -override _.Require(env, state, input) = - // Check both vars since Execute will resolve both - (input.FromAccount |> Var.tryResolve env |> Result.isOk) && - (input.ToAccount |> Var.tryResolve env |> Result.isOk) -``` - -# [C#](#tab/csharp) - -```csharp -public record TransferInput -{ - // From previous CreateAccount commands - public required Var FromAccount { get; init; } - public required Var ToAccount { get; init; } - public decimal Amount { get; init; } -} - -public override bool Require(Env env, BankState state, TransferInput input) => - // Check both vars since Execute will resolve both - input.FromAccount.TryResolve(env, out var _) && - input.ToAccount.TryResolve(env, out var _); -``` - ---- - -**Important distinctions:** - -- **Vars from command inputs** (produced by `Generate` picking from state lists): These can become unbound during shrinking and need to be checked in `Require` -- **Vars in the state** (created with `Var.symbolic` in `InitialState`): These always have default values and are always resolvable, so they don't need `Require` checks -- **Only check what you use**: Only check the `Var` fields that your `Execute` method actually resolves. If your command doesn't use a particular var from the input, you don't need to check it in `Require` - -## Require vs Precondition - -It's important to understand the difference between these two methods: - -| Aspect | Precondition | Require | -|--------|-------------|---------| -| **When called** | During generation & execution | Only during execution | -| **Has Env?** | ❌ No - cannot resolve vars | ✅ Yes - can resolve vars | -| **Purpose** | Structural check ("do we have IDs?") | Runtime check ("can we resolve this ID?") | -| **Return false means** | Don't generate this command | Skip this command (continue test) | -| **Check frequency** | Every candidate command | Only generated commands | - -**In practice:** Use `Precondition` for structural state checks, and `Require` for validating symbolic variable inputs. - -## Summary - -**The Rule:** If your `Generate` method returns a `Var` (or contains one as a part of a generated input), -always override `Require` to check if that variable can be resolved. - -**Why:** Commands can be skipped during execution, leaving symbolic variables unbound. -Without `Require`, you'll crash trying to resolve non-existent values. - -**How:** Use `TryResolve` to safely check if a variable is bound before attempting to use it in `Execute`. - -This pattern keeps your stateful tests robust and prevents mysterious failures from unresolved symbolic variables. diff --git a/docs/stateful/specifications.md b/docs/stateful/specifications.md deleted file mode 100644 index ba4bacb0..00000000 --- a/docs/stateful/specifications.md +++ /dev/null @@ -1,431 +0,0 @@ -# Specifications - -Once you've defined your commands, you need a **specification** that ties everything together. A specification declares: - -- The initial state of your model -- Which commands are available -- How many actions to generate -- Whether to test sequentially or in parallel - -Hedgehog provides two types of specifications: - -- **SequentialSpecification**: Tests sequences of operations running one after another -- **ParallelSpecification**: Tests concurrent operations to verify linearizability - -## Sequential Specifications - -Sequential specifications test your system by generating and executing sequences of commands one at a time. This is the most common type of stateful test. - -### Basic Structure - -# [F#](#tab/fsharp) - -```fsharp -type CounterSpec() = - inherit SequentialSpecification() - - // The starting state of your model - override _.InitialState = { CurrentCount = Var.symbolic 0 } - - // How many actions to generate (1 to 10) - override _.Range = Range.linear 1 10 - - // Available commands - override _.Commands = [| - IncrementCommand() - DecrementCommand() - ResetCommand() - |] -``` - -# [C#](#tab/csharp) - -```csharp -public class CounterSpec : SequentialSpecification -{ - // The starting state of your model - public override CounterState InitialState => - new() { CurrentCount = Var.Symbolic(0) }; - - // How many actions to generate (1 to 10) - public override Range Range => Range.Linear(1, 10); - - // Available commands - public override ICommand[] Commands => - [ - new IncrementCommand(), - new DecrementCommand(), - new ResetCommand() - ]; -} -``` - ---- - -### Running the Test - -Convert the specification to a property and check it as a regular property: - -# [F#](#tab/fsharp) - -```fsharp -[] -let ``Counter behaves correctly``() = - // obtain sut somehow - let sut = Counter() - CounterSpec().ToProperty(sut).Check() -``` - -# [C#](#tab/csharp) - -```csharp -[Fact] -public void Counter_BehavesCorrectly() -{ - // obtain sut somehow - var sut = new Counter(); - new CounterSpec().ToProperty(sut).Check(); -} -``` - ---- - -### Setup and Cleanup - -Sequential specifications support setup and cleanup commands that run before and after each test sequence: - -# [F#](#tab/fsharp) - -```fsharp -type CounterSpec() = - inherit SequentialSpecification() - - override _.InitialState = { CurrentCount = Var.symbolic 0 } - override _.Range = Range.linear 1 10 - - // Setup runs BEFORE the test sequence - override _.SetupCommands = [| - InitializeCommand() // e.g., set counter to a random value - |] - - // Main test commands - override _.Commands = [| - IncrementCommand() - DecrementCommand() - |] - - // Cleanup runs AFTER the test sequence - override _.CleanupCommands = [| - ResetCommand() // e.g., reset counter to 0 - |] -``` - -# [C#](#tab/csharp) - -```csharp -public class CounterSpec : SequentialSpecification -{ - public override CounterState InitialState => - new() { CurrentCount = Var.Symbolic(0) }; - - public override Range Range => Range.Linear(1, 10); - - // Setup runs BEFORE the test sequence - public override ICommand[] SetupCommands => - [ - InitializeCommand() // e.g., set counter to a random value - ]; - - // Main test commands - public override ICommand[] Commands => - [ - new IncrementCommand(), - new DecrementCommand() - ]; - - // Cleanup runs AFTER the test sequence - public override ICommand[] CleanupCommands => - [ - new ResetCommand() // e.g., reset counter to 0 - ]; -} -``` - ---- - -**Key points about setup and cleanup:** - -- Setup commands execute **in order** before test commands. -- Cleanup commands execute **in order** after test commands. -- Cleanup runs **even if the test fails** -- Both setup and cleanup commands can have their **parameters shrink**, but they cannot be removed from the sequence during shrinking. - -## Parallel Specifications - -Parallel specifications test whether your system is **linearizable**—meaning concurrent operations behave as if they executed in *some* sequential order. - -### What is Linearizability? - -When operations run concurrently, they can interfere with each other. A linearizable system guarantees that despite this interference, the results match what *could have happened* if the operations ran sequentially. - -For example, if two threads both increment a counter, linearizability ensures the counter increases by 2—not 1 (which would indicate a lost update). - -### How Parallel Testing Works - -Parallel testing has three phases: - -1. **Sequential Prefix**: Run some operations sequentially to set up initial state -2. **Parallel Branches**: Run two sequences of operations **in parallel** on the same system -3. **Linearizability Check**: Verify the results match *some* interleaving of the operations - -### Basic Structure - -# [F#](#tab/fsharp) - -```fsharp -type ParallelCounterSpec() = - inherit ParallelSpecification() - - // Starting state - override _.InitialState = { CurrentCount = Var.symbolic 0 } - - // Length of sequential prefix (0-3 operations) - override _.PrefixRange = Range.linear 0 3 - - // Length of each parallel branch (1-5 operations each) - override _.BranchRange = Range.linear 1 5 - - // Commands that can run in parallel - override _.Commands = [| - IncrementCommand() - DecrementCommand() - GetCommand() - |] -``` - -# [C#](#tab/csharp) - -```csharp -public class ParallelCounterSpec : ParallelSpecification -{ - // Starting state - public override CounterState InitialState => - new() { CurrentCount = Var.Symbolic(0) }; - - // Length of sequential prefix (0-3 operations) - public override Range PrefixRange => Range.Linear(0, 3); - - // Length of each parallel branch (1-5 operations each) - public override Range BranchRange => Range.Linear(1, 5); - - // Commands that can run in parallel - public override ICommand[] Commands => - [ - new IncrementCommand(), - new DecrementCommand(), - new GetCommand() - ]; -} -``` - ---- - -### Running Parallel Tests - -# [F#](#tab/fsharp) - -```fsharp -[] -let ``Counter is thread-safe``() = - let sut = ThreadSafeCounter() - ParallelCounterSpec().ToProperty(sut).Check() -``` - -# [C#](#tab/csharp) - -```csharp -[Fact] -public void Counter_IsThreadSafe() -{ - var sut = new ThreadSafeCounter(); - new ParallelCounterSpec().ToProperty(sut).Check(); -} -``` - ---- - -### Important: Sharing the SUT - -**The same SUT instance is intentionally shared between parallel branches.** This is not a bug - it's the whole point! - -We *want* operations to interfere with each other because we're testing whether the system handles concurrent access correctly. If the system is properly thread-safe, all results will be linearizable. If it has concurrency bugs, some test runs will produce results that can't be explained by any sequential ordering. - -### Writing Commands for Parallel Testing - -When writing commands for parallel testing, remember: - -1. **Preconditions and Require** still check the model state -2. **Ensure** should verify weak postconditions—linearizability checking handles the strong guarantees -3. Return values matter—the framework uses them to verify linearizability - -Example of a weak postcondition in parallel context: - -# [F#](#tab/fsharp) - -```fsharp -type IncrementCommand() = - inherit Command() - - override _.Name = "Increment" - override _.Precondition(state) = true - override _.Execute(counter, env, state, input) = - Task.FromResult(counter.Increment()) - override _.Generate(state) = Gen.constant () - override _.Update(state, input, outputVar) = { CurrentCount = outputVar } - - // Weak postcondition: we can't assert the exact value - // Linearizability checking verifies the sequence is valid - override _.Ensure(env, oldState, newState, input, result) = - result > 0 // After increment, should be positive -``` - -# [C#](#tab/csharp) - -```csharp -public class IncrementCommand : Command -{ - public override string Name => "Increment"; - public override bool Precondition(CounterState state) => true; - - public override Task Execute(ThreadSafeCounter sut, Env env, CounterState state, NoInput input) => - Task.FromResult(sut.Increment()); - - public override Gen Generate(CounterState state) => - Gen.Constant(NoInput.Value); - - public override CounterState Update(CounterState state, NoInput input, Var outputVar) => - state with { CurrentCount = outputVar }; - - // Weak postcondition: we can't assert the exact value - // Linearizability checking verifies the sequence is valid - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoInput input, int result) => - result > 0; // After increment, should be positive -} -``` - ---- - -### Setup and Cleanup in Parallel Tests - -Parallel specifications also support setup and cleanup: - -# [F#](#tab/fsharp) - -```fsharp -type ParallelCounterSpec() = - inherit ParallelSpecification() - - override _.InitialState = { CurrentCount = Var.symbolic 0 } - override _.PrefixRange = Range.linear 0 3 - override _.BranchRange = Range.linear 1 5 - - // Setup runs BEFORE prefix and parallel branches - override _.SetupCommands = [| - InitializeCommand() - |] - - override _.Commands = [| - IncrementCommand() - DecrementCommand() - |] - - // Cleanup runs AFTER parallel branches complete - override _.CleanupCommands = [| - ResetCommand() - |] -``` - -# [C#](#tab/csharp) - -```csharp -public class ParallelCounterSpec : ParallelSpecification -{ - public override CounterState InitialState => - new() { CurrentCount = Var.Symbolic(0) }; - - public override Range PrefixRange => Range.Linear(0, 3); - public override Range BranchRange => Range.Linear(1, 5); - - // Setup runs BEFORE prefix and parallel branches - public override ICommand[] SetupCommands => - [ new InitializeCommand() ]; - - public override ICommand[] Commands => - [ - new IncrementCommand(), - new DecrementCommand() - ]; - - // Cleanup runs AFTER parallel branches complete - public override ICommand[] CleanupCommands => - [ new ResetCommand() ]; -} -``` - ---- - -**Note:** Cleanup is generated using the state **after the prefix** (before parallel execution), since the parallel branches can't be used to predict a single final state. But it is **executed** at the end of the whole sequence. - -## Using Fresh SUTs - -Instead of creating the SUT yourself and passing it to the specification, you can provide a factory function that creates a fresh SUT for each test run: - -# [F#](#tab/fsharp) - -```fsharp -[] -let ``Counter test with fresh SUT``() = - // Factory creates a new Counter for each test - let createSut() = Counter() - - CounterSpec().ToPropertyWith(createSut).Check() -``` - -# [C#](#tab/csharp) - -```csharp -[Fact] -public void Counter_TestWithFreshSUT() -{ - // Factory creates a new Counter for each test - Func createSut = () => new Counter(); - - new CounterSpec().ToPropertyWith(createSut).Check(); -} -``` - ---- - -This approach ensures test isolation—each test run gets a completely fresh system. - -## Summary - -**Sequential Specifications:** -- Test operations running one after another -- Use `SequentialSpecification` -- Define `InitialState`, `Range`, and `Commands` -- Optionally add `SetupCommands` and `CleanupCommands` - -**Parallel Specifications:** -- Test concurrent operations for linearizability -- Use `ParallelSpecification` -- Define `InitialState`, `PrefixRange`, `BranchRange`, and `Commands` -- The same SUT is intentionally shared between parallel branches -- Linearizability checking verifies results match some sequential interleaving -- Optionally add `SetupCommands` and `CleanupCommands` - -Both specifications provide: -- Automatic shrinking of test sequences -- Setup/cleanup command support -- Clear failure reporting -- Integration with property-based testing frameworks diff --git a/docs/stateful/toc.yml b/docs/stateful/toc.yml deleted file mode 100644 index 1374ac3a..00000000 --- a/docs/stateful/toc.yml +++ /dev/null @@ -1,12 +0,0 @@ -- name: Overview - href: index.md -- name: Building Blocks - items: - - name: Commands - href: commands.md - - name: Runtime Preconditions - href: require.md - - name: Specifications - href: specifications.md -- name: Complete Example - href: complete-example.md diff --git a/docs/toc.yml b/docs/toc.yml index cece4e2f..560fc87b 100644 --- a/docs/toc.yml +++ b/docs/toc.yml @@ -1,9 +1,6 @@ - name: Documentation href: articles/ homepage: index.md -- name: Stateful Testing - href: stateful/ - homepage: stateful/index.md - name: XUnit Integration href: xunit/ homepage: xunit/index.md diff --git a/gen-docfx.fsx b/gen-docfx.fsx index 7334e388..9aafb8ef 100644 --- a/gen-docfx.fsx +++ b/gen-docfx.fsx @@ -126,7 +126,6 @@ let defaultConfig = { Assemblies = [ ("src/Hedgehog/bin/Debug/net8.0/Hedgehog.dll", "Hedgehog") ("src/Hedgehog.Xunit/bin/Debug/net8.0/Hedgehog.Xunit.dll", "Hedgehog.Xunit") - ("src/Hedgehog.Stateful/bin/Debug/net8.0/Hedgehog.Stateful.dll", "Hedgehog.Stateful") ] OutputDir = "docs/api" @@ -135,7 +134,7 @@ let defaultConfig = { RootUrl = "/" SkipAutoOpenWrappers = true - CSharpNamespaces = Set.ofList ["Hedgehog.Linq"; "Hedgehog.Stateful.Linq"] + CSharpNamespaces = Set.ofList ["Hedgehog.Linq"] } // ============================================================================ @@ -1155,7 +1154,6 @@ let runWithArgs (args: string[]) : unit = let assemblies = [ ($"src/Hedgehog/bin/%s{buildConfiguration}/net8.0/Hedgehog.dll", "Hedgehog") ($"src/Hedgehog.Xunit/bin/%s{buildConfiguration}/net8.0/Hedgehog.Xunit.dll", "Hedgehog.Xunit") - ($"src/Hedgehog.Stateful/bin/%s{buildConfiguration}/net8.0/Hedgehog.Stateful.dll", "Hedgehog.Stateful") ] let config = { defaultConfig with Assemblies = assemblies } diff --git a/src/Hedgehog.Stateful/Action.fs b/src/Hedgehog.Stateful/Action.fs deleted file mode 100644 index f1b6757e..00000000 --- a/src/Hedgehog.Stateful/Action.fs +++ /dev/null @@ -1,50 +0,0 @@ -namespace Hedgehog.Stateful - -open System.Threading.Tasks - -/// Result of executing a command -type internal ActionResult<'TOutput> = - | Success of 'TOutput - | Failure of exn - -/// Category of action in a test sequence -type internal ActionCategory = - | Setup // Setup actions that run before the main test sequence - | Test // Main test actions - | Cleanup // Cleanup actions that run after the main test sequence - -/// An action is a command instance with concrete input. -/// Actions are generated with symbolic inputs and executed against the SUT. -/// The SUT is passed as a typed parameter, separate from Env. -[] -type internal Action<'TSystem, 'TState> = private { - /// Unique identifier for this action instance (generated from Env.freshName) - Id: Name - /// Human-readable description - Name: string - /// The input to the command (boxed) - Input: obj - /// Category of this action (Setup, Test, or Cleanup) - Category: ActionCategory - /// Execute the action against the real system (SUT passed as typed parameter) - /// Returns a Task that completes with ExecutionResult - sync commands return completed tasks - Execute: 'TSystem -> Env -> 'TState -> Task> - /// Structural precondition check (on model state only, no env) - Precondition: 'TState -> bool - /// Check precondition with concrete values (env allows resolving symbolic variables in state) - Require: Env -> 'TState -> bool - /// Update the model state - Update: 'TState -> Var -> 'TState - /// Verify postcondition (SUT not passed - verify based on state transitions only) - /// Returns true if postcondition is satisfied, false otherwise. - /// May throw exceptions which will be caught and treated as failures. - Ensure: Env -> 'TState -> 'TState -> obj -> bool -} -with - member private this.DisplayText = this.Name - -/// A sequence of actions to execute -type internal Actions<'TSystem, 'TState> = { - Initial: 'TState - Steps: Action<'TSystem, 'TState> list -} diff --git a/src/Hedgehog.Stateful/Command.fs b/src/Hedgehog.Stateful/Command.fs deleted file mode 100644 index 773e8c7e..00000000 --- a/src/Hedgehog.Stateful/Command.fs +++ /dev/null @@ -1,234 +0,0 @@ -namespace Hedgehog.Stateful - -open System.Threading.Tasks -open Hedgehog -open Hedgehog.FSharp -open Hedgehog.Stateful.FSharp - -/// -/// Base class for commands that perform stateful operations and return values. -/// Commands are the building blocks of state machine tests - they represent operations -/// on a system under test (SUT) that can be generated, executed, and verified. -/// The SUT is passed as a typed parameter to Execute and Ensure. -/// Execute returns a Task to support both synchronous and asynchronous operations. -/// -/// The type of the system under test. -/// The type of the model state. -/// The type of input required to execute the command. -/// The type of output produced by the command. -[] -type Command<'TSystem, 'TState, 'TInput, 'TOutput>() = - - /// Human-readable name of the command (e.g., "Push", "Pop") - abstract member Name : string - - /// - /// Structural precondition that determines if this command can be generated/executed in the given state. - /// Return true if the command can run, false to skip generation. - /// This is automatically used by both generation and Require (unless Require is overridden). - /// - /// The current model state. - abstract member Precondition : state:'TState -> bool - - /// - /// Generate random input for this command given the current model state. - /// This is only called when Precondition returns true. - /// - /// The current model state. - abstract member Generate: state:'TState -> Gen<'TInput> - - /// - /// Check if the command can be executed in the given state with concrete values. - /// Return false if the command should not be executed in this state. - /// The env parameter allows resolving symbolic variables from the state. - /// By default, returns true. Override only when you need to check concrete values with env. - /// Note: Precondition is always checked separately, so you don't need to duplicate those checks here. - /// - /// The environment containing resolved values from previous commands. - /// The current model state. - /// The concrete input value for this command. - abstract member Require : env:Env * state:'TState * input:'TInput -> bool - default this.Require(_, _, _) = true - - /// - /// Execute the command against the real system, returning a Task. - /// For synchronous operations, use Task.FromResult(value). - /// The sut parameter is the typed System Under Test. - /// The state parameter is the current model state. - /// The env contains resolved values from previous commands. - /// - /// The system under test. - /// The environment containing resolved values from previous commands. - /// The current model state. - /// The input value for this command. - abstract member Execute: sut:'TSystem * env:Env * state:'TState * input:'TInput -> Task<'TOutput> - - /// - /// Update the model state after the command executes. - /// The Var represents the symbolic output that can be referenced by future commands. - /// - /// The current model state. - /// The input value for this command. - /// The symbolic output variable that can be referenced by future commands. - abstract member Update : state:'TState * input:'TInput * output:Var<'TOutput> -> 'TState - default this.Update(state, _, _) = state - - /// - /// Verify the command's postcondition after execution. - /// Compare the model state transitions (s0 -> s1) with the actual output. - /// Should only verify based on states, input, and output - not inspect the SUT directly. - /// Returns true if postcondition is satisfied, false otherwise. - /// May throw exceptions which will be caught and treated as failures. - /// - /// The environment containing resolved values from previous commands. - /// The model state before the command executed. - /// The model state after the command executed. - /// The input value for this command. - /// The actual output value produced by the command. - abstract member Ensure : env:Env * oldState:'TState * newState:'TState * input:'TInput * output:'TOutput -> bool - default this.Ensure(_, _, _, _, _) = true - - interface ICommand<'TSystem, 'TState> with - member this.ToActionGen() = { - TryGen = fun category state env -> - if this.Precondition(state) then - Some (this.Generate(state) |> Gen.map (fun input -> - let actionId, env' = Env.freshName env - let action : Action<'TSystem, 'TState> = { - Id = actionId - Name = $"%s{this.Name} %A{input}" - Input = box input - Category = category - Precondition = this.Precondition - Require = fun e s -> this.Require(e, s, input) - Execute = fun sut environment state -> - task { - try - let! result = this.Execute(sut, environment, state, input) - return ActionResult.Success (box result) - with ex -> - return ActionResult.Failure ex - } - Update = fun s v -> - // Convert Var to Var<'TOutput> - they have different runtime types - this.Update(s, input, Var.convertFrom v) - Ensure = fun environment s0 s1 o -> - this.Ensure(environment, s0, s1, input, unbox<'TOutput> o) - } - action, env' - )) - else - None - } - - -/// -/// Base class for commands that perform side-effects without returning meaningful values. -/// Examples: closing a connection, clearing a cache, deleting a file. -/// Simpler than Command because no output variable is needed. -/// Execute returns a Task to support both synchronous and asynchronous operations. -/// The SUT is passed as a typed parameter to Execute and Ensure. -/// -/// The type of the system under test. -/// The type of the model state. -/// The type of input required to execute the action. -[] -type ActionCommand<'TSystem, 'TState, 'TInput>() = - - /// Human-readable name of the action (e.g., "Close", "Clear", "Delete") - abstract member Name : string - - /// - /// Structural precondition that determines if this action can be generated/executed in the given state. - /// Return true if the action can run, false to skip generation. - /// This is automatically used by both generation and Require (unless Require is overridden). - /// - /// The current model state. - abstract member Precondition : state:'TState -> bool - - /// - /// Generate random input for this action given the current model state. - /// This is only called when Precondition returns true. - /// - /// The current model state. - abstract member Generate: state:'TState -> Gen<'TInput> - - /// - /// Check if the action can be executed in the given state with concrete values. - /// Return false if the action should not be executed in this state. - /// The env parameter allows resolving symbolic variables from the state. - /// By default, returns true. Override only when you need to check concrete values with env. - /// Note: Precondition is always checked separately, so you don't need to duplicate those checks here. - /// - /// The environment containing resolved values from previous commands. - /// The current model state. - /// The concrete input value for this action. - abstract member Require : env:Env * state:'TState * input:'TInput -> bool - default this.Require(_, _, _) = true - - /// - /// Execute the action against the real system without returning a value. - /// For synchronous operations, use Task.CompletedTask. - /// The sut parameter is the typed System Under Test. - /// The state parameter is the current model state. - /// The env contains resolved values from previous commands. - /// - /// The system under test. - /// The environment containing resolved values from previous commands. - /// The current model state. - /// The input value for this action. - abstract member Execute: sut:'TSystem * env:Env * state:'TState * input:'TInput -> Task - - /// - /// Update the model state after the action executes. - /// No output variable since actions don't produce values to reference later. - /// - /// The current model state. - /// The input value for this action. - abstract member Update : state:'TState * input:'TInput -> 'TState - default this.Update(state, _) = state - - /// - /// Verify the action's postcondition after execution. - /// Compare the model state transitions (s0 -> s1) with the input. - /// Should only verify based on states and input - not inspect the SUT directly. - /// No output parameter since actions don't produce values. - /// Returns true if postcondition is satisfied, false otherwise. - /// May throw exceptions which will be caught and treated as failures. - /// - /// The environment containing resolved values from previous commands. - /// The model state before the action executed. - /// The model state after the action executed. - /// The input value for this action. - abstract member Ensure : env:Env * oldState:'TState * newState:'TState * input:'TInput -> bool - default this.Ensure(_, _, _, _) = true - - interface ICommand<'TSystem, 'TState> with - member this.ToActionGen() = { - TryGen = fun category state env -> - if this.Precondition(state) then - Some (this.Generate(state) |> Gen.map (fun input -> - let actionId, env' = Env.freshName env - let action : Action<'TSystem, 'TState> = { - Id = actionId - Name = $"%s{this.Name} %A{input}" - Input = box input - Category = category - Precondition = this.Precondition - Require = fun e s -> this.Require(e, s, input) - Execute = fun sut environment state -> - task { - try - do! this.Execute(sut, environment, state, input) - return ActionResult.Success (box ()) - with ex -> - return ActionResult.Failure ex - } - Update = fun s _ -> this.Update(s, input) // Ignore Var parameter - Ensure = fun environment s0 s1 _ -> this.Ensure(environment, s0, s1, input) // Ignore output parameter - } - action, env' // Return updated env with fresh name - )) - else - None - } diff --git a/src/Hedgehog.Stateful/Hedgehog.Stateful.fsproj b/src/Hedgehog.Stateful/Hedgehog.Stateful.fsproj deleted file mode 100644 index ee7dc362..00000000 --- a/src/Hedgehog.Stateful/Hedgehog.Stateful.fsproj +++ /dev/null @@ -1,51 +0,0 @@ - - - - net8.0 - true - 0.7.0-beta3 - Stateful testing for Hedgehog - Alexey Raga - Copyright © 2025 - true - true - Hedgehog.Stateful - LICENSE - https://hedgehogqa.github.io/fsharp-hedgehog/ - hedgehog-logo.png - https://github.com/hedgehogqa/fsharp-hedgehog/raw/master/img/hedgehog-logo.png - fsharp;f#;c#;csharp;dotnet;testing - https://github.com/hedgehogqa/fsharp-hedgehog - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/src/Hedgehog.Stateful/ICommand.fs b/src/Hedgehog.Stateful/ICommand.fs deleted file mode 100644 index 08f60eed..00000000 --- a/src/Hedgehog.Stateful/ICommand.fs +++ /dev/null @@ -1,22 +0,0 @@ -namespace Hedgehog.Stateful - -open Hedgehog - -/// Interface for types that helps with converting commands to executable actions. -/// This allows seamless mixing of different commands and action commands. -[] -type ICommand<'TSystem, 'TState> = - abstract member ToActionGen: unit -> ActionGen<'TSystem, 'TState> - -/// Used internally. -/// Existential wrapper to allow heterogeneous command lists. -/// This erases the input/output types so different commands can be in the same list. -and ActionGen<'TSystem, 'TState> = - internal - { - /// Attempt to generate an action from this command - TryGen: ActionCategory -> 'TState -> Env -> Gen * Env> option - } - - interface ICommand<'TSystem, 'TState> with - member this.ToActionGen() = this diff --git a/src/Hedgehog.Stateful/Linq/NoValue.fs b/src/Hedgehog.Stateful/Linq/NoValue.fs deleted file mode 100644 index 55810e85..00000000 --- a/src/Hedgehog.Stateful/Linq/NoValue.fs +++ /dev/null @@ -1,9 +0,0 @@ -namespace Hedgehog.Stateful.Linq - -/// Represents the absence of value, that can be used for commands that don't require input parameters. -/// Similar to F#'s unit type, this is a zero-sized struct with a single instance. -[] -[] -type NoValue = - static member val Value = Unchecked.defaultof - member private this.DisplayText = "" diff --git a/src/Hedgehog.Stateful/Linq/SpecificationExtensions.fs b/src/Hedgehog.Stateful/Linq/SpecificationExtensions.fs deleted file mode 100644 index 9648a001..00000000 --- a/src/Hedgehog.Stateful/Linq/SpecificationExtensions.fs +++ /dev/null @@ -1,37 +0,0 @@ -namespace Hedgehog.Stateful.Linq - -open System -open System.Runtime.CompilerServices -open Hedgehog -open Hedgehog.Stateful - - -/// -/// Extension methods for working with specifications in C#. -/// -[] -type SpecificationExtensions private () = - - /// - /// Convert a sequential specification to a property using a SUT factory. - /// The factory is called once per property test run to create a fresh SUT. - /// This is the recommended approach to ensure test isolation. - /// - /// The sequential specification. - /// A Func delegate that creates a new SUT instance for each test run. - /// A property representing the sequential specification test. - [] - static member ToPropertyWith(spec: SequentialSpecification<'TSystem, 'TState>, createSut: Func<'TSystem>) : Property = - spec.ToPropertyWith(fun () -> createSut.Invoke()) - - /// - /// Convert a parallel specification to a property using a SUT factory. - /// The factory is called once per property test run to create a fresh SUT. - /// This is the recommended approach to ensure test isolation. - /// - /// The parallel specification. - /// A Func delegate that creates a new SUT instance for each test run. - /// A property representing the parallel specification test. - [] - static member ToPropertyWith(spec: ParallelSpecification<'TSystem, 'TState>, createSut: Func<'TSystem>) : Property = - spec.ToPropertyWith(fun () -> createSut.Invoke()) diff --git a/src/Hedgehog.Stateful/Linq/VarExtensions.fs b/src/Hedgehog.Stateful/Linq/VarExtensions.fs deleted file mode 100644 index d8604c58..00000000 --- a/src/Hedgehog.Stateful/Linq/VarExtensions.fs +++ /dev/null @@ -1,24 +0,0 @@ -namespace Hedgehog.Stateful.Linq - -open System -open System.Runtime.CompilerServices -open Hedgehog.Stateful -open Hedgehog.Stateful.FSharp - - -/// -/// Extension methods for working with Var<T> in C#. -/// -[] -type VarExtensions private () = - - /// - /// Projects the value of a variable using a selector function. - /// This allows extracting fields from structured command outputs. - /// - /// The variable to project from. - /// A function to apply to the variable's value. - /// A new variable with the projection applied. - [] - static member Select(var: Var<'T>, selector: Func<'T, 'U>) : Var<'U> = - Var.map selector.Invoke var diff --git a/src/Hedgehog.Stateful/Parallel.fs b/src/Hedgehog.Stateful/Parallel.fs deleted file mode 100644 index 2c805897..00000000 --- a/src/Hedgehog.Stateful/Parallel.fs +++ /dev/null @@ -1,259 +0,0 @@ -namespace Hedgehog.Stateful - -open Hedgehog -open Hedgehog.FSharp -open Hedgehog.Stateful.FSharp - -type internal ParallelActions<'TSystem, 'TState> = { - Initial: 'TState - Setup: Action<'TSystem, 'TState> list - Prefix: Action<'TSystem, 'TState> list - Branch1: Action<'TSystem, 'TState> list - Branch2: Action<'TSystem, 'TState> list - Cleanup: Action<'TSystem, 'TState> list -} - -[] -module Parallel = - - let internal genActions - (prefixRange: Range) - (branchRange: Range) - (setupActions: ActionGen<'TSystem, 'TState> list) - (testActions: ActionGen<'TSystem, 'TState> list) - (cleanupActions: ActionGen<'TSystem, 'TState> list) - (initial: 'TState) - : Gen> = - gen { - // Generate setup actions first - let! setup = Sequential.genActions (Range.singleton 0) setupActions [] [] initial - - // Calculate state after setup - let stateAfterSetup = - setup.Steps - |> List.fold (fun s a -> - let name, _ = Env.freshName Env.empty - a.Update s (Var.bound name) - ) initial - - // Generate prefix using state after setup - let! prefix = Sequential.genActions prefixRange [] testActions [] stateAfterSetup - - // Calculate state after prefix - let stateAfterPrefix = - prefix.Steps - |> List.fold (fun s a -> - a.Update s (Var.bound a.Id) - ) stateAfterSetup - - // Generate branches from state after prefix - let! branch1 = Sequential.genActions branchRange [] testActions [] stateAfterPrefix - let! branch2 = Sequential.genActions branchRange [] testActions [] stateAfterPrefix - - // Generate cleanup based on state after prefix (not after branches, since branches run in parallel) - let! cleanup = Sequential.genActions (Range.singleton 0) cleanupActions [] [] stateAfterPrefix - - return { - Initial = initial - Setup = setup.Steps - Prefix = prefix.Steps - Branch1 = branch1.Steps - Branch2 = branch2.Steps - Cleanup = cleanup.Steps - } - } - - /// Check if there exists a valid interleaving of two action branches. - /// This function integrates interleaving generation with validation, allowing early - /// termination and pruning of invalid branches for better performance. - /// Instead of generating all O(2^(n+m)) interleavings, it searches depth-first - /// and stops as soon as a valid interleaving is found. - let internal isLinearizable - (initial: 'TState) - (prefix: Action<'TSystem, 'TState> list) - (branch1: Action<'TSystem, 'TState> list) - (branch2: Action<'TSystem, 'TState> list) - (results: Map) - : bool = - - /// Try to execute a single action and return the new state/env if successful - let tryExecuteAction state env (action: Action<'TSystem, 'TState>) = - if not (action.Precondition state && action.Require env state) then - None - else - match Map.tryFind action.Id results with - | None -> None - | Some output -> - let outputVar = Var.bound action.Id - let env' = Env.add outputVar output env - let state' = action.Update state outputVar - 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). - /// Prunes branches that fail preconditions or action execution. - let rec searchInterleavings state env xs ys = - match xs, ys with - | [], [] -> - // Successfully reached the end - found a valid interleaving - true - | x :: xs', [] -> - // Only branch1 actions remaining - match tryExecuteAction state env x with - | Some (state', env') -> searchInterleavings state' env' xs' [] - | None -> false - | [], y :: ys' -> - // Only branch2 actions remaining - match tryExecuteAction state env y with - | Some (state', env') -> searchInterleavings state' env' [] ys' - | None -> false - | x :: xs', y :: ys' -> - // Both branches have actions - try both orderings - // First try executing action from branch1 - match tryExecuteAction state env x with - | Some (state', env') when searchInterleavings state' env' xs' ys -> - true // Found valid path through branch1 first - | _ -> - // Branch1 first either failed or led to invalid path, try branch2 first - match tryExecuteAction state env y with - | Some (state', env') -> searchInterleavings state' env' xs ys' - | None -> false - - /// First execute the prefix sequentially - let rec runPrefix state env = function - | [] -> Some (state, env) - | action :: rest -> - match tryExecuteAction state env action with - | Some (state', env') -> runPrefix state' env' rest - | None -> None - - // Execute prefix, then search for valid interleaving of branches - match runPrefix initial Env.empty prefix with - | None -> false - | Some (state, env) -> searchInterleavings state env branch1 branch2 - - let internal executeWithSUT (sut: 'TSystem) (actions: ParallelActions<'TSystem, 'TState>) : Property = - let formatActionName (action: Action<'TSystem, 'TState>) : string = - match action.Category with - | ActionCategory.Setup -> $"+ %s{action.Name}" - | ActionCategory.Test -> action.Name - | ActionCategory.Cleanup -> $"- %s{action.Name}" - - property { - // Run setup actions sequentially first - let mutable state = actions.Initial - let mutable env = Env.empty - - for action in actions.Setup do - let! result = Property.ofTask (action.Execute sut env state) - - match result with - | ActionResult.Failure ex -> - do! Property.counterexample (fun () -> formatActionName action) - 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' - state <- action.Update state outputVar - - // Run prefix sequentially - let prefixResults = ResizeArray() - - for action in actions.Prefix do - let! result = Property.ofTask (action.Execute sut env state) - - match result with - | ActionResult.Failure ex -> - do! Property.counterexample (fun () -> formatActionName action) - do! Property.counterexample (fun () -> $"Final state: %A{state}") - return! Property.exn ex - | ActionResult.Success output -> - prefixResults.Add(action.Id, output) - let outputVar = Var.bound action.Id - env <- Env.add outputVar output env - state <- action.Update state outputVar - - // Save state before parallel branches (which is also before cleanup) - let stateBeforeBranches = state - - // Run branches in parallel - let runBranch (branch: Action<'TSystem, 'TState> list) : Async> = - let rec loop results branchEnv branchState = function - | [] -> async { return Ok (List.rev results) } - | action :: rest -> - async { - let! result = action.Execute sut branchEnv branchState |> Async.AwaitTask - match result with - | ActionResult.Failure ex -> - return Error ex - | ActionResult.Success output -> - let outputVar = Var.bound action.Id - let newEnv = Env.add outputVar output branchEnv - let newState = action.Update branchState outputVar - return! loop ((action.Id, output) :: results) newEnv newState rest - } - loop [] env state branch - - let! branchResults = - async { - return! Async.Parallel [runBranch actions.Branch1; runBranch actions.Branch2] - } - - let results = branchResults : Result<(Name * obj) list, exn> array - - // Check linearizability regardless of branch success/failure - // Then run cleanup actions - let linearizabilityCheck = - match results[0], results[1] with - | Error ex, _ | _, Error ex -> - // Branch failed - report state before branches - property { - do! Property.counterexample (fun () -> $"Final state: %A{stateBeforeBranches}") - return! Property.exn ex - } - | Ok results1, Ok results2 -> - let allResults = - [ yield! prefixResults; yield! results1; yield! results2 ] - |> Map.ofList - - let linearizable = - isLinearizable actions.Initial actions.Prefix actions.Branch1 actions.Branch2 allResults - - if not linearizable then - property { - do! Property.counterexample (fun () -> "No valid interleaving found") - do! Property.counterexample (fun () -> $"Final state: %A{stateBeforeBranches}") - return! Property.failure - } - else - Property.ofBool true - - // Run cleanup actions - these always run even if tests failed - // We catch any cleanup failures and report them after linearizability check - let mutable cleanupError = None - - for action in actions.Cleanup do - match cleanupError with - | Some _ -> () // Skip remaining cleanup if one fails - | None -> - if action.Precondition state && action.Require env state then - let! result = Property.ofTask (action.Execute sut env state) - match result with - | ActionResult.Failure ex -> - cleanupError <- Some (formatActionName action, ex) - | ActionResult.Success output -> - let outputVar = Var.bound action.Id - env <- Env.add outputVar output env - - // Check linearizability first - do! linearizabilityCheck - - // Then report any cleanup errors - match cleanupError with - | Some (actionName, ex) -> - do! Property.counterexample (fun () -> actionName) - do! Property.exn ex - | None -> () - } diff --git a/src/Hedgehog.Stateful/ParallelSpecification.fs b/src/Hedgehog.Stateful/ParallelSpecification.fs deleted file mode 100644 index fc1a6059..00000000 --- a/src/Hedgehog.Stateful/ParallelSpecification.fs +++ /dev/null @@ -1,94 +0,0 @@ -namespace Hedgehog.Stateful - -open Hedgehog -open Hedgehog.FSharp - - -/// -/// Abstract base class for parallel state machine tests. -/// Tests concurrent execution by running two branches in parallel after a sequential prefix. -/// The SUT (System Under Test) is created externally and passed to Check/ToProperty methods. -/// -[] -type ParallelSpecification<'TSystem, 'TState>() = - - - /// - /// The initial model state. - /// - abstract member InitialState : 'TState - - - /// - /// Range of prefix sequence lengths to generate (sequential actions before parallel execution). - /// - abstract member PrefixRange : Range - - - /// - /// Range of branch sequence lengths to generate (parallel actions in each branch). - /// - abstract member BranchRange : Range - - - /// - /// Commands that operate on the SUT during the test sequence. - /// The SUT is passed as a typed parameter to Execute methods. - /// - abstract member Commands : ICommand<'TSystem, 'TState> array - - - /// - /// Setup commands that execute before the prefix and parallel branches. - /// These commands are generated (parameters can shrink) but always execute in the order specified. - /// Setup commands cannot be shrunk away from the action sequence. - /// Default is an empty list (no setup). - /// - abstract member SetupCommands : ICommand<'TSystem, 'TState> array - default _.SetupCommands = [||] - - - /// - /// Cleanup commands that execute after the parallel branches complete. - /// These commands are generated (parameters can shrink) but always execute in the order specified. - /// Cleanup commands cannot be shrunk away and are guaranteed to run even if tests fail. - /// Cleanup is generated using the state after prefix (before parallel execution). - /// Default is an empty list (no cleanup). - /// - abstract member CleanupCommands : ICommand<'TSystem, 'TState> array - default _.CleanupCommands = [||] - - /// - /// Convert this specification to a property that can be checked. - /// - /// The system under test (SUT) instance to use for the test run. - /// A property representing the parallel specification test. - member this.ToProperty(sut: 'TSystem) : Property = - let setupActions = this.SetupCommands |> Seq.map _.ToActionGen() |> List.ofSeq - let testActions = this.Commands |> Seq.map _.ToActionGen() |> List.ofSeq - let cleanupActions = this.CleanupCommands |> Seq.map _.ToActionGen() |> List.ofSeq - let gen = Parallel.genActions this.PrefixRange this.BranchRange setupActions testActions cleanupActions this.InitialState - - property { - let! actions = gen - do! Parallel.executeWithSUT sut actions - } - - /// - /// Convert this specification to a property using a SUT factory. - /// The factory is called once per property test run to create a fresh SUT. - /// This is the recommended approach to ensure test isolation. - /// - /// A function that creates a new SUT instance for each test run. - /// A property representing the parallel specification test. - member this.ToPropertyWith(createSut: unit -> 'TSystem) : Property = - let setupActions = this.SetupCommands |> Seq.map _.ToActionGen() |> List.ofSeq - let testActions = this.Commands |> Seq.map _.ToActionGen() |> List.ofSeq - let cleanupActions = this.CleanupCommands |> Seq.map _.ToActionGen() |> List.ofSeq - let gen = Parallel.genActions this.PrefixRange this.BranchRange setupActions testActions cleanupActions this.InitialState - - property { - let! actions = gen - let sut = createSut() // Create fresh SUT for this test run - do! Parallel.executeWithSUT sut actions - } diff --git a/src/Hedgehog.Stateful/Sequential.fs b/src/Hedgehog.Stateful/Sequential.fs deleted file mode 100644 index 10c319d0..00000000 --- a/src/Hedgehog.Stateful/Sequential.fs +++ /dev/null @@ -1,233 +0,0 @@ -namespace Hedgehog.Stateful - -open Hedgehog -open Hedgehog.FSharp -open Hedgehog.Stateful.FSharp - -[] -module Sequential = - - let internal genActions - (range: Range) - (setupActions: ActionGen<'TSystem, 'TState> list) - (testActions: ActionGen<'TSystem, 'TState> list) - (cleanupActions: ActionGen<'TSystem, 'TState> list) - (initial: 'TState) - : Gen> = - - // Generate a fixed list of actions from command specs (for setup/cleanup) - // The list structure is fixed, but individual action parameters can shrink - // Returns a Random function that produces a Tree of action lists - let rec genFixedActionsRandom - (category: ActionCategory) - (actions: ActionGen<'TSystem, 'TState> list) - (state: 'TState) - (env: Env) - : Random list> * Env> = - - Random (fun seed size -> - // Helper to thread state through action generation - // Returns list of (action tree, updated env) pairs and final env - let rec generateWithStateThreading seeds currentState currentEnv = function - | [] -> [], currentEnv - | spec :: rest -> - match spec.TryGen category currentState currentEnv with - | None -> - failwithf $"Required %A{category} command failed to generate in current state. Command: %s{spec.GetType().Name}" - | Some actionGen -> - let seed1, seed2 = Seed.split seeds - - // Generate action tree with environment - let actionAndEnvTree = Random.run seed1 size (Gen.toRandom actionGen) - - // 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 nextState = outcomeAction.Update currentState outputVar - - // Recursively generate rest with updated state - let restTrees, finalEnv = generateWithStateThreading seed2 nextState nextEnv rest - - // Extract just action tree (discard env from tree structure) - let actionTree = Tree.map fst actionAndEnvTree - - (actionTree :: restTrees), finalEnv - - // Generate all action trees with proper state threading - let actionTrees, finalEnv = generateWithStateThreading seed state env actions - - // Combine trees into a single tree of action lists - // This preserves shrinking: each action can shrink independently, - // and the tree structure ensures we test all valid combinations - let rec combineTrees = function - | [] -> Tree.singleton [] - | tree :: rest -> - tree |> Tree.bind (fun action -> - combineTrees rest |> Tree.map (fun actions -> - action :: actions - ) - ) - - combineTrees actionTrees, finalEnv - ) - - - // Helper: Collect action trees with state threading (for main test commands) - let rec collectTrees n state env = Random (fun seed size -> - if n <= 0 then - [], env - else - let available = testActions |> List.choose (fun cmd -> cmd.TryGen ActionCategory.Test state env) - - if List.isEmpty available then - [], env - else - // Select one of the available action generators - let selectedGenTree = Gen.toRandom (Gen.item available) - let selectedGen = Random.run seed size selectedGenTree - - // Generate the action tree from the selected generator - let seed1, seed2 = Seed.split seed - let actionAndEnvTree = Gen.toRandom (Tree.outcome selectedGen) - let actionAndEnvTreeResult = Random.run seed1 size actionAndEnvTree - - // Extract outcome for state evolution - let action, env' = Tree.outcome actionAndEnvTreeResult - let name = fst (Env.freshName env) - let outputVar = Var.bound name - let state' = action.Update state outputVar - - // Recurse with split seed - let restTrees, envFinal = - Random.run seed2 size (collectTrees (n - 1) state' env') - - // Map the tree to just extract the action (discard env for tree structure) - let actionTree = Tree.map fst actionAndEnvTreeResult - (actionTree :: restTrees), envFinal - ) - - // Validate a sequence of actions - let rec validateSequence env state = function - | [] -> true - | action :: rest -> - if action.Require env state then - let state' = action.Update state (Var.bound action.Id) - validateSequence env state' rest - else false - - // Project final state by applying Updates from action lists - let projectFinalState (setupActions: Action<'TSystem, 'TState> list) (testActions: Action<'TSystem, 'TState> list) (initial: 'TState) : 'TState = - let allActions = setupActions @ testActions - allActions - |> List.fold (fun state action -> - action.Update state (Var.bound action.Id) - ) initial - - // Main generator - gen { - let! count = Gen.int32 range - - return! Gen.ofRandom (Random (fun seed size -> - // Split seed for setup, test, and cleanup - let seed1, seed2 = Seed.split seed - let seed2a, seed2b = Seed.split seed2 - - // Generate setup actions - let setupTree, envAfterSetup = Random.run seed1 size (genFixedActionsRandom ActionCategory.Setup - setupActions initial Env.empty) - - // Compute state after setup - let setupActions = Tree.outcome setupTree - let stateAfterSetup = projectFinalState setupActions [] initial - - // Generate test actions - let actionTrees, _ = Random.run seed2a size (collectTrees count stateAfterSetup envAfterSetup) - - let testActionsTree = - if List.isEmpty actionTrees then - Tree.singleton [] - else - actionTrees - |> Shrink.sequenceList - |> Tree.filter (validateSequence envAfterSetup stateAfterSetup) - - // Compute final state using outcomes - let testActionsOutcome = Tree.outcome testActionsTree - let finalStateOutcome = projectFinalState setupActions testActionsOutcome initial - - // Generate cleanup actions based on final state - let cleanupTree, _ = Random.run seed2b size (genFixedActionsRandom ActionCategory.Cleanup cleanupActions - finalStateOutcome envAfterSetup) - - // Combine all three trees - let combinedTree = - setupTree |> Tree.bind (fun setupShrunk -> - testActionsTree |> Tree.bind (fun testShrunk -> - cleanupTree |> Tree.map (fun cleanupShrunk -> - { Initial = initial; Steps = setupShrunk @ testShrunk @ cleanupShrunk } - ) - ) - ) - - combinedTree - )) - } - - /// Execute actions with a SUT instance. - /// The SUT is passed as a typed parameter to each command's Execute and Ensure methods. - let internal executeWithSUT (sut: 'TSystem) (actions: Actions<'TSystem, 'TState>) : Property = - let formatActionName (action: Action<'TSystem, 'TState>) : string = - match action.Category with - | ActionCategory.Setup -> $"+ %s{action.Name}" - | ActionCategory.Test -> action.Name - | ActionCategory.Cleanup -> $"- %s{action.Name}" - - let rec loop state env steps : Property = - match steps with - | [] -> Property.ofBool true - | action :: rest -> - if not (action.Precondition state && action.Require env state) then - // Skip this action and continue with the rest - loop state env rest - else - property { - // Execute always returns Task> - let! result = Property.ofTask (action.Execute sut env state) - - match result with - | ActionResult.Failure ex -> - // 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{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 state0 = state - let state1 = action.Update state outputVar - - do! Property.counterexample (fun () -> formatActionName action) - // Ensure returns bool - wrap it in a property that handles exceptions - // If ensure fails, add final state before propagating - do! - try - 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{state1}") - do! Property.exn ex - } - else - Property.exn ex - do! loop state1 env'' rest - } - - property { - do! Property.counterexample (fun () -> $"Initial state: %A{actions.Initial}") - do! loop actions.Initial Env.empty actions.Steps - } diff --git a/src/Hedgehog.Stateful/SequentialSpecification.fs b/src/Hedgehog.Stateful/SequentialSpecification.fs deleted file mode 100644 index 3ecd98c7..00000000 --- a/src/Hedgehog.Stateful/SequentialSpecification.fs +++ /dev/null @@ -1,90 +0,0 @@ -namespace Hedgehog.Stateful - -open Hedgehog -open Hedgehog.FSharp -open Hedgehog.Stateful - - -/// -/// Abstract base class for sequential state machine tests. -/// The SUT (System Under Test) is created externally and passed to Check/ToProperty methods. -/// Setup and cleanup are modeled as command lists that execute before/after test actions. -/// -[] -type SequentialSpecification<'TSystem, 'TState>() = - - - /// - /// The initial model state. - /// - abstract member InitialState : 'TState - - - /// - /// Range of action sequence lengths to generate. - /// - abstract member Range : Range - - - /// - /// Commands that operate on the SUT during the test sequence. - /// The SUT is passed as a typed parameter to Execute methods. - /// - abstract member Commands : ICommand<'TSystem, 'TState> array - - - /// - /// Setup commands that execute before the test sequence. - /// These commands are generated (parameters can shrink) but always execute in the order specified. - /// Setup commands cannot be shrunk away from the action sequence. - /// Default is an empty list (no setup). - /// - abstract member SetupCommands : ICommand<'TSystem, 'TState> array - default _.SetupCommands = [||] - - - /// - /// Cleanup commands that execute after the test sequence. - /// These commands are generated (parameters can shrink) but always execute in the order specified. - /// Cleanup commands cannot be shrunk away and are guaranteed to run even if tests fail. - /// Cleanup is generated using the final state after setup and test actions complete. - /// Default is an empty list (no cleanup). - /// - abstract member CleanupCommands : ICommand<'TSystem, 'TState> array - default _.CleanupCommands = [||] - - /// - /// Convert this specification to a property that can be checked. - /// - /// The system under test (SUT) instance to use for the test run. - /// A property representing the sequential specification test. - member this.ToProperty(sut: 'TSystem) : Property = - let setupActions = this.SetupCommands |> Seq.map _.ToActionGen() |> List.ofSeq - let testActions = this.Commands |> Seq.map _.ToActionGen() |> List.ofSeq - let cleanupActions = this.CleanupCommands |> Seq.map _.ToActionGen() |> List.ofSeq - - let gen = Sequential.genActions this.Range setupActions testActions cleanupActions this.InitialState - - property { - let! actions = gen - do! Sequential.executeWithSUT sut actions - } - - /// - /// Convert this specification to a property using a SUT factory. - /// The factory is called once per property test run to create a fresh SUT. - /// This is the recommended approach to ensure test isolation. - /// - /// A function that creates a new SUT instance for each test run. - /// A property representing the sequential specification test. - member this.ToPropertyWith(createSut: unit -> 'TSystem) : Property = - let setupActions = this.SetupCommands |> Seq.map _.ToActionGen() |> List.ofSeq - let testActions = this.Commands |> Seq.map _.ToActionGen() |> List.ofSeq - let cleanupActions = this.CleanupCommands |> Seq.map _.ToActionGen() |> List.ofSeq - let gen = Sequential.genActions this.Range setupActions testActions cleanupActions this.InitialState - - property { - let! actions = gen - let sut = createSut() // Create fresh SUT for this test run - do! Sequential.executeWithSUT sut actions - } diff --git a/src/Hedgehog.Stateful/Types.fs b/src/Hedgehog.Stateful/Types.fs deleted file mode 100644 index 391ff081..00000000 --- a/src/Hedgehog.Stateful/Types.fs +++ /dev/null @@ -1,167 +0,0 @@ -namespace Hedgehog.Stateful - -open System.Diagnostics.CodeAnalysis - -/// -/// Unique identifier for a symbolic variable. -/// -[] -type Name = internal Name of int - - -/// -/// Environment mapping symbolic variable names to concrete values. -/// The SUT is passed separately to Execute, not stored in Env. -/// -type Env = private { - values: Map - nextId: int -} - - -/// -/// 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. -/// -[] -[] -type Var<'T> = private { - /// - /// The unique integer name of the variable. - /// Symbolic (unbound) variables have Name = -1. - /// Bound variables have Name >= 0 and can be looked up in the environment. - /// - Name: int - /// - /// 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 for caching resolved values to avoid redundant environment lookups and Transform applications. - /// Eagerly populated when a concrete value is bound via Env.add. - /// Also used for displaying resolved values in counterexamples. - /// - /// The cache eliminates the need to repeatedly look up values from Env and apply Transform, - /// which is especially beneficial since most Var instances are created with concrete values - /// that are immediately known, not from symbolic references that need delayed resolution. - /// - mutable ResolvedValue: 'T option -} -with - - member private this.DisplayText = - // If resolved for display (during counterexample formatting), show the resolved value - let value = this.ResolvedValue |> Option.orElse this.Default - match value with - | Some value -> $"%A{value}" - | None -> "" - - /// - /// Resolve the variable using its default if not found in the environment. - /// - /// The environment to resolve the variable from. - /// The resolved value of the variable. - member this.Resolve(env: Env) : 'T = - let mutable value = Unchecked.defaultof<'T> - if this.TryResolve(env, &value) then - value - else - failwithf $"Var<{typeof<'T>}>(%A{Name this.Name}) not found in environment and no default provided. -This likely indicates a missing Require check in your command specification. -Commands that use Var inputs must override Require to call TryResolve and return false if the variable cannot be resolved." - - - /// - /// Resolve the variable with an explicit fallback value, overriding the variable's default. - /// - /// 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. - member this.ResolveOr(env: Env, fallback: 'T) : 'T = - let mutable value = Unchecked.defaultof<'T> - if this.TryResolve(env, &value) then - value - else - fallback - - /// - /// Attempts to resolve a variable from the environment. - /// - /// The environment to resolve the variable from. - /// When this method returns, contains the resolved value if successful; otherwise, the default value for the type. - /// true if the variable was successfully resolved; otherwise, false. - member this.TryResolve(env: Env, [] [] value: byref<'T>) : bool = - // Check cache first to avoid redundant environment lookups and Transform applications - match this.ResolvedValue with - | Some cached -> - value <- cached - true - | None -> - // Try to look up in environment - match Map.tryFind (Name this.Name) env.values with - | Some v -> - try - let resolved = this.Transform v - // Cache the resolved value for future calls (memoization) - this.ResolvedValue <- Some resolved - value <- resolved - true - with _ -> - value <- Unchecked.defaultof<'T> - false - | None -> - // Try default value - match this.Default with - | Some d -> - value <- d - true - | None -> - value <- Unchecked.defaultof<'T> - false - - static member internal CreateSymbolic(value: 'T) : Var<'T> = - { Name = -1; Default = Some value; Transform = unbox<'T>; ResolvedValue = None } - - override this.Equals(other: obj) : bool = - match other with - | :? Var<'T> as otherVar -> this.Name = otherVar.Name - | _ -> false - - override this.GetHashCode() : int = - hash this.Name - - interface System.IComparable with - member this.CompareTo(other: obj) : int = - match other with - | :? Var<'T> as otherVar -> compare this.Name otherVar.Name - | _ -> invalidArg (nameof other) "Cannot compare values of different types" - - -module internal Env = - /// Empty environment - let empty : Env = { values = Map.empty; nextId = 0 } - - /// Generate a fresh variable name - 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 = - // Eagerly cache the resolved value to avoid future environment lookups - // Apply Transform to ensure the cache contains the correctly transformed value - try - let resolved = v.Transform (box value) - v.ResolvedValue <- Some resolved - with - | _ -> () // If Transform fails, leave cache empty and let Resolve handle it later - { 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 deleted file mode 100644 index 6638d45d..00000000 --- a/src/Hedgehog.Stateful/Var.fs +++ /dev/null @@ -1,83 +0,0 @@ -namespace Hedgehog.Stateful - - -[] -module Var = - - /// - /// Initialise a symbolic (unbound) variable with a default value for the initial state. - /// A symbolic variable is not yet bound to a generated value and is used to represent - /// a placeholder in the model before generation or binding occurs. - /// - /// The default value to assign to the variable. - /// A new symbolic (unbound) Var<T> with the given default value. - [] - let symbolic (defaultValue: 'T) : Var<'T> = - { Name = -1; Default = Some defaultValue; Transform = unbox<'T>; ResolvedValue = None } - -namespace Hedgehog.Stateful.FSharp - -open Hedgehog.Stateful - - -[] -module Var = - /// - /// Resolve a variable using its default value if not found in the environment. - /// - /// The environment to resolve the variable from. - /// 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. - /// - /// The fallback value to use if the variable is not found. - /// The environment to resolve the variable from. - /// 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. - /// - /// 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. - let tryResolve<'T> (v: Var<'T>) (env: Env) : Result<'T, string> = - let mutable value = Unchecked.defaultof<'T> - if v.TryResolve(env, &value) then - Ok value - else - Error $"Var_{v.Name} not found in environment and no default provided" - - /// - /// Map a function over a variable, creating a new variable that projects - /// a value from the original variable's output. This allows extracting - /// fields from structured command outputs. - /// - /// The projection function to apply. - /// The variable to map over. - /// A new variable with the projection applied. - let map (f: 'T -> 'U) (v: Var<'T>) : Var<'U> = - let transform = v.Transform >> f - { Name = v.Name - Default = v.Default |> Option.map f - Transform = transform - ResolvedValue = v.ResolvedValue |> Option.map transform } - - /// Create a bounded var from a Name (used during generation) - let internal bound (name: Name) : Var<'T> = - let (Name n) = name - { Name = n; Default = None; Transform = unbox<'T>; ResolvedValue = None } - - /// Convert from obj var to typed var (used internally) - let internal convertFrom<'T> (v: Var) : Var<'T> = - let transform = v.Transform >> unbox<'T> - { Name = v.Name - Default = v.Default |> Option.map unbox<'T> - Transform = transform - ResolvedValue = v.ResolvedValue |> Option.map transform } diff --git a/src/Hedgehog/Property.fs b/src/Hedgehog/Property.fs index 1aeb9518..c178cb27 100644 --- a/src/Hedgehog/Property.fs +++ b/src/Hedgehog/Property.fs @@ -118,7 +118,12 @@ module Property = /// The property succeeds when the async computation completes successfully, and fails if it throws an exception. /// This enables testing of asynchronous F# code. let ofAsync (asyncComputation : Async<'T>) : Property<'T> = - Gen.constant (lazy (PropertyResult.ofAsyncWith asyncComputation)) + Gen.constant (lazy (PropertyResult.ofAsync asyncComputation)) + |> Property + + /// Create Property from an async computation that produces a journal and outcome + let ofAsyncWithJournal (asyncComputation : Async>) : Property<'T> = + Gen.constant (lazy (PropertyResult.ofAsyncWithJournal asyncComputation)) |> Property /// Discards test cases where the predicate returns false, causing Hedgehog to generate a new test case. diff --git a/src/Hedgehog/PropertyResult.fs b/src/Hedgehog/PropertyResult.fs index f2c66381..de038f5a 100644 --- a/src/Hedgehog/PropertyResult.fs +++ b/src/Hedgehog/PropertyResult.fs @@ -14,11 +14,11 @@ module internal PropertyResult = PropertyResult.Sync (journal, outcome) /// Create an async PropertyResult from an async computation that produces a journal and outcome - let ofAsync (asyncResult : Async>) : PropertyResult<'a> = + let ofAsyncWithJournal (asyncResult : Async>) : PropertyResult<'a> = PropertyResult.Async asyncResult /// Create an async PropertyResult by capturing exceptions from an async computation - let ofAsyncWith (asyncComputation : Async<'a>) : PropertyResult<'a> = + let ofAsync (asyncComputation : Async<'a>) : PropertyResult<'a> = PropertyResult.Async (async { try let! result = asyncComputation diff --git a/tests/Hedgehog.Stateful.Tests.CSharp/AsyncCounterSpec.cs b/tests/Hedgehog.Stateful.Tests.CSharp/AsyncCounterSpec.cs deleted file mode 100644 index 050748b3..00000000 --- a/tests/Hedgehog.Stateful.Tests.CSharp/AsyncCounterSpec.cs +++ /dev/null @@ -1,260 +0,0 @@ -namespace Hedgehog.Stateful.Tests.CSharp; - -using Hedgehog.Linq; -using Xunit; - -/// -/// Async Counter - all operations return Tasks -/// -public class AsyncCounter -{ - private int _value; - - public async Task IncrementAsync() - { - await Task.Delay(1); // Simulate async work - _value++; - } - - public async Task DecrementAsync() - { - await Task.Delay(1); - _value--; - } - - public async Task AddRandomAsync() - { - await Task.Delay(1); - var rnd = new Random().Next(100); - _value += rnd; - return _value; - } - - public async Task SetAsync(int n) - { - await Task.Delay(1); - _value = n; - } - - public async Task GetAsync() - { - await Task.Delay(1); - return _value; - } - - public async Task ResetAsync() - { - await Task.Delay(1); - _value = 0; - } -} - -/// -/// Model state for async counter -/// -public record AsyncCounterState -{ - public required Var CurrentCount { get; init; } -} - -/// -/// Async increment command -/// -public class AsyncIncrementCommand : Command -{ - public override string Name => "IncrementAsync"; - - public override bool Precondition(AsyncCounterState state) => true; - public override bool Require(Env env, AsyncCounterState state, bool input) => Precondition(state); - - public override async Task Execute(AsyncCounter sut, Env env, AsyncCounterState state, bool input) - { - await sut.IncrementAsync(); - return await sut.GetAsync(); - } - - public override Gen Generate(AsyncCounterState state) => - Gen.Constant(true); - - - public override AsyncCounterState Update(AsyncCounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, AsyncCounterState oldState, AsyncCounterState newState, bool input, int result) - { - var oldCount = oldState.CurrentCount.Resolve(env); - return result == oldCount + 1; - } -} - -/// -/// Async decrement command -/// -public class AsyncDecrementCommand : Command -{ - public override string Name => "DecrementAsync"; - - public override bool Precondition(AsyncCounterState state) => true; - public override bool Require(Env env, AsyncCounterState state, bool input) => Precondition(state); - - public override async Task Execute(AsyncCounter sut, Env env, AsyncCounterState state, bool input) - { - await sut.DecrementAsync(); - return await sut.GetAsync(); - } - - public override Gen Generate(AsyncCounterState state) => - Hedgehog.Linq.Gen.Constant(true); - - - public override AsyncCounterState Update(AsyncCounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, AsyncCounterState oldState, AsyncCounterState newState, bool input, int result) - { - var oldCount = oldState.CurrentCount.Resolve(env); - return result == oldCount - 1; - } -} - -/// -/// Async reset command -/// -public class AsyncResetCommand : Command -{ - public override string Name => "ResetAsync"; - - public override bool Precondition(AsyncCounterState state) => true; - public override bool Require(Env env, AsyncCounterState state, bool input) => Precondition(state); - - public override async Task Execute(AsyncCounter sut, Env env, AsyncCounterState state, bool input) - { - await sut.ResetAsync(); - return await sut.GetAsync(); - } - - public override Gen Generate(AsyncCounterState state) => - Gen.Constant(true); - - - public override AsyncCounterState Update(AsyncCounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, AsyncCounterState oldState, AsyncCounterState newState, bool input, int result) - { - return result == 0; - } -} - -/// -/// Async set command -/// -public class AsyncSetCommand : Command -{ - public override string Name => "SetAsync"; - - public override bool Precondition(AsyncCounterState state) => true; - - public override bool Require(Env env, AsyncCounterState state, int input) => Precondition(state); - - public override async Task Execute(AsyncCounter sut, Env env, AsyncCounterState state, int value) - { - await sut.SetAsync(value); - return await sut.GetAsync(); - } - - public override Gen Generate(AsyncCounterState state) => - Gen.Int32(Range.LinearFromInt32(0, -10, 100)); - - - public override AsyncCounterState Update(AsyncCounterState state, int input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, AsyncCounterState oldState, AsyncCounterState newState, int input, int result) - { - return result == input; - } -} - -/// -/// Async get command -/// -public class AsyncGetCommand : Command -{ - public override string Name => "GetAsync"; - - public override bool Precondition(AsyncCounterState state) => true; - public override bool Require(Env env, AsyncCounterState state, bool input) => Precondition(state); - - public override Task Execute(AsyncCounter sut, Env env, AsyncCounterState state, bool input) => - sut.GetAsync(); - - public override Gen Generate(AsyncCounterState state) => - Gen.Constant(true); - - - public override AsyncCounterState Update(AsyncCounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, AsyncCounterState oldState, AsyncCounterState newState, bool input, int result) - { - return result == oldState.CurrentCount.Resolve(env); - } -} - -/// -/// Async AddRandom command -/// -public class AsyncAddRandomCommand : Command -{ - public override string Name => "AddRandomAsync"; - - public override bool Precondition(AsyncCounterState state) => true; - public override bool Require(Env env, AsyncCounterState state, bool input) => Precondition(state); - - public override Task Execute(AsyncCounter sut, Env env, AsyncCounterState state, bool input) => - sut.AddRandomAsync(); - - public override Gen Generate(AsyncCounterState state) => - Gen.Constant(true); - - public override bool Ensure(Env env, AsyncCounterState oldState, AsyncCounterState newState, bool input, int output) => true; - - public override AsyncCounterState Update(AsyncCounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; -} - -/// -/// Async Counter Specification -/// -public class AsyncCounterSpec : SequentialSpecification -{ - public override ICommand[] SetupCommands => - [new AsyncResetCommand()]; - - public override ICommand[] CleanupCommands => []; - - public override AsyncCounterState InitialState => new() { CurrentCount = Var.Symbolic(0) }; - - public override Range Range => Hedgehog.Linq.Range.LinearInt32(1, 50); - - public override ICommand[] Commands => - [ - new AsyncIncrementCommand(), - new AsyncDecrementCommand(), - new AsyncResetCommand(), - new AsyncGetCommand(), - new AsyncSetCommand(), - new AsyncAddRandomCommand() - ]; -} - -public class AsyncCounterTests -{ - [Fact] - public void AsyncCounterTest() - { - var sut = new AsyncCounter(); - new AsyncCounterSpec().ToProperty(sut).Check(); - } -} diff --git a/tests/Hedgehog.Stateful.Tests.CSharp/Hedgehog.Stateful.Tests.CSharp.csproj b/tests/Hedgehog.Stateful.Tests.CSharp/Hedgehog.Stateful.Tests.CSharp.csproj deleted file mode 100644 index 9627cbb8..00000000 --- a/tests/Hedgehog.Stateful.Tests.CSharp/Hedgehog.Stateful.Tests.CSharp.csproj +++ /dev/null @@ -1,34 +0,0 @@ - - - - net8.0 - enable - enable - - false - true - - - - - all - runtime; build; native; contentfiles; analyzers; buildtransitive - - - - all - runtime; build; native; contentfiles; analyzers; buildtransitive - - - - - - - - - - - - - - diff --git a/tests/Hedgehog.Stateful.Tests.CSharp/ParallelCounterSpec.cs b/tests/Hedgehog.Stateful.Tests.CSharp/ParallelCounterSpec.cs deleted file mode 100644 index d155b177..00000000 --- a/tests/Hedgehog.Stateful.Tests.CSharp/ParallelCounterSpec.cs +++ /dev/null @@ -1,188 +0,0 @@ -namespace Hedgehog.Stateful.Tests.CSharp; - -using Hedgehog.Linq; -using Xunit; - -/* - PARALLEL TESTING: Testing Linearizability of Concurrent Operations - - This example demonstrates how parallel state machine testing works. - - WHAT DOES IT TEST? - ------------------- - Parallel testing verifies that a concurrent data structure (like our ThreadSafeCounter) - is "linearizable" - meaning that despite operations running in parallel, the observed - results match what could happen if those operations executed in SOME sequential order. - - HOW DOES IT WORK? - ----------------- - 1. SEQUENTIAL PREFIX: First, a sequence of operations runs sequentially to set up - some initial state (e.g., counter might be at value 5). - - 2. PARALLEL BRANCHES: Then, TWO branches of operations run IN PARALLEL on the SAME SUT. - For example: - Thread 1: Increment, Get, Increment - Thread 2: Decrement, Get - These run concurrently - they WILL interfere with each other! - - 3. LINEARIZABILITY CHECK: After parallel execution, the framework checks if there exists - ANY valid sequential ordering of all operations that would produce the same results. - - If Branch 1 observed: [6, 6, 7] and Branch 2 observed: [5, 5], the framework checks: - - Could Increment, Decrement, Get, Increment, Get produce these results? - - Could Decrement, Increment, Get, Get, Increment produce these results? - - ... checks all possible interleavings ... - - If ANY interleaving matches, the test passes (operations are linearizable). - If NO interleaving matches, the test FAILS (there's a concurrency bug). - - WHY DOES THIS WORK? - ------------------- - The key insight: The same SUT is INTENTIONALLY shared between parallel branches. - This is not a bug - it's the whole point! We WANT operations to interfere, because - we're testing whether the SUT can handle concurrent access correctly. - - If the SUT is correctly thread-safe (like ThreadSafeCounter with Interlocked operations), - all observed results will be linearizable. - - If the SUT has concurrency bugs (e.g., unsynchronized read-modify-write), some test - runs will observe results that can't be explained by ANY sequential ordering, and the - test will fail. -*/ - -/// -/// Thread-safe counter for parallel testing using Interlocked operations -/// This tests whether concurrent operations are linearizable -/// -public class ThreadSafeCounter -{ - private int _value; - - public int Increment() => Interlocked.Increment(ref _value); - - public int Decrement() => Interlocked.Decrement(ref _value); - - public int Get() => Interlocked.CompareExchange(ref _value, 0, 0); -} - -/// -/// Model state for parallel counter testing -/// -public record ParallelCounterState -{ - public required Var CurrentCount { get; init; } -} - -/// -/// Parallel increment command - returns the new value after incrementing -/// -public class ParallelIncrementCommand : Command -{ - public override string Name => "Increment"; - public override bool Precondition(ParallelCounterState state) => true; - public override bool Require(Env env, ParallelCounterState state, bool input) => Precondition(state); - - public override Task Execute(ThreadSafeCounter sut, Env env, ParallelCounterState state, bool input) => - Task.FromResult(sut.Increment()); - - public override Gen Generate(ParallelCounterState state) => - Gen.Constant(true); - - - - public override ParallelCounterState Update(ParallelCounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, ParallelCounterState oldState, ParallelCounterState newState, bool input, int result) - { - // For parallel testing, Ensure should only check weak postconditions - // The framework will verify linearizability by checking all interleavings - // We can only check that the result is a valid counter value - return result > 0; // After increment, value should be positive (assuming we start at 0) - } -} - -/// -/// Parallel decrement command - returns the new value after decrementing -/// -public class ParallelDecrementCommand : Command -{ - public override string Name => "Decrement"; - - public override bool Precondition(ParallelCounterState state) => true; - public override bool Require(Env env, ParallelCounterState state, bool input) => Precondition(state); - - public override Task Execute(ThreadSafeCounter sut, Env env, ParallelCounterState state, bool input) => - Task.FromResult(sut.Decrement()); - - public override Gen Generate(ParallelCounterState state) => - Gen.Constant(true); - - - public override ParallelCounterState Update(ParallelCounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, ParallelCounterState oldState, ParallelCounterState newState, bool input, int output) => true; -} - -/// -/// Parallel get command - reads the current value -/// -public class ParallelGetCommand : Command -{ - public override string Name => "Get"; - - public override bool Precondition(ParallelCounterState state) => true; - public override bool Require(Env env, ParallelCounterState state, bool input) => Precondition(state); - - public override Task Execute(ThreadSafeCounter sut, Env env, ParallelCounterState state, bool input) => - Task.FromResult(sut.Get()); - - public override Gen Generate(ParallelCounterState state) => - Gen.Constant(true); - - - public override ParallelCounterState Update(ParallelCounterState state, bool input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, ParallelCounterState oldState, ParallelCounterState newState, bool input, int output) => true; -} - -/// -/// Parallel specification for testing linearizability of ThreadSafeCounter -/// -public class ParallelCounterSpec : ParallelSpecification -{ - public override ParallelCounterState InitialState => new() { CurrentCount = Var.Symbolic(0) }; - - // Generate prefix sequences of 0-3 actions (setup some initial state) - public override Range PrefixRange => Range.LinearInt32(0, 3); - - // Generate branch sequences of 1-5 actions per thread - public override Range BranchRange => Range.LinearInt32(1, 5); - - // Commands that can run in parallel - public override ICommand[] Commands => - [ - new ParallelIncrementCommand(), - new ParallelDecrementCommand(), - new ParallelGetCommand() - ]; - - public override ICommand[] SetupCommands => []; - public override ICommand[] CleanupCommands => []; -} - -public class ParallelCounterTests -{ - [Fact] - public void ParallelCounterTest() - { - var sut = new ThreadSafeCounter(); - // This will: - // 1. Run a sequential prefix to set up initial state - // 2. Run two branches in parallel - // 3. Verify that the results are linearizable (match some sequential interleaving) - new ParallelCounterSpec().ToProperty(sut).Check(); - } -} diff --git a/tests/Hedgehog.Stateful.Tests.CSharp/SequentialCounterSpec.cs b/tests/Hedgehog.Stateful.Tests.CSharp/SequentialCounterSpec.cs deleted file mode 100644 index af0ea847..00000000 --- a/tests/Hedgehog.Stateful.Tests.CSharp/SequentialCounterSpec.cs +++ /dev/null @@ -1,242 +0,0 @@ -using Hedgehog.Stateful.Linq; - -namespace Hedgehog.Stateful.Tests.CSharp; - -using Hedgehog.Linq; -using Xunit; - -/// -/// Simple counter for demonstrating sequential state machine testing -/// -public class Counter -{ - private int _value; - - public void Increment() => _value++; - - public void Decrement() => _value--; - - public int AddRandom() - { - var rnd = new Random().Next(100); - _value += rnd; - return _value; - } - - public void Set(int n) => _value = n; - - public int Get() => _value; - - public void Reset() => _value = 0; -} - -/// -/// Model state tracking the current count symbolically -/// -public record CounterState(Var CurrentCount); - -/// -/// Increment command - increments the counter and returns new value -/// -public class IncrementCommand : Command -{ - public override string Name => "Increment"; - - public override bool Precondition(CounterState state) => true; - public override bool Require(Env env, CounterState state, NoValue value) => Precondition(state); - - public override Task Execute(Counter sut, Env env, CounterState state, NoValue value) - { - sut.Increment(); - var result = sut.Get(); - return Task.FromResult(result); - } - - public override Gen Generate(CounterState state) => - Gen.Constant(NoValue.Value); - - public override CounterState Update(CounterState state, NoValue value, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoValue value, int result) - { - var oldCount = oldState.CurrentCount.Resolve(env); - return result == oldCount + 1; - } -} - -/// -/// AddRandom command - adds a random value to the counter -/// -public class AddRandomCommand : Command -{ - public override string Name => "AddRandom"; - - public override bool Precondition(CounterState state) => true; - public override bool Require(Env env, CounterState state, NoValue value) => Precondition(state); - - public override Task Execute(Counter sut, Env env, CounterState state, NoValue value) => - Task.FromResult(sut.AddRandom()); - - public override Gen Generate(CounterState state) => - Gen.Constant(NoValue.Value); - - - public override CounterState Update(CounterState state, NoValue value, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoValue value, int output) => true; -} - -/// -/// Decrement command - decrements the counter and returns new value -/// -public class DecrementCommand : Command -{ - public override string Name => "Decrement"; - - public override bool Precondition(CounterState state) => true; - public override bool Require(Env env, CounterState state, NoValue value) => Precondition(state); - - public override Task Execute(Counter sut, Env env, CounterState state, NoValue value) - { - sut.Decrement(); - var result = sut.Get(); - return Task.FromResult(result); - } - - public override Gen Generate(CounterState state) => - Gen.Constant(NoValue.Value); - - - public override CounterState Update(CounterState state, NoValue value, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoValue value, int result) - { - var oldCount = oldState.CurrentCount.Resolve(env); - return result == oldCount - 1; - } -} - -/// -/// Reset command - resets the counter to 0 -/// -public class ResetCommand : Command -{ - public override string Name => "Reset"; - - public override bool Precondition(CounterState state) => true; - public override bool Require(Env env, CounterState state, NoValue value) => Precondition(state); - - public override Task Execute(Counter sut, Env env, CounterState state, NoValue value) - { - sut.Reset(); - var result = sut.Get(); - return Task.FromResult(result); - } - - public override Gen Generate(CounterState state) => - Gen.Constant(NoValue.Value); - - - public override CounterState Update(CounterState state, NoValue value, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoValue value, int result) - { - // Reset always sets to 0 - return result == 0; - } -} - -/// -/// Set command - sets the counter to a specific value -/// -public class SetCommand : Command -{ - public override string Name => "Set"; - - public override bool Precondition(CounterState state) => true; - public override bool Require(Env env, CounterState state, int input) => true; - - public override Task Execute(Counter sut, Env env, CounterState state, int value) - { - sut.Set(value); - var result = sut.Get(); - return Task.FromResult(result); - } - - public override Gen Generate(CounterState state) => - Gen.Int32(Range.LinearFromInt32(0, -10, 100)); - - public override CounterState Update(CounterState state, int input, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, int input, int result) - { - Assert.Equal(input, result); - return result == input; - } -} - -/// -/// Get command - returns the current counter value -/// -public class GetCommand : Command -{ - public override string Name => "Get"; - - public override bool Precondition(CounterState state) => true; - public override bool Require(Env env, CounterState state, NoValue value) => Precondition(state); - - public override Task Execute(Counter sut, Env env, CounterState state, NoValue value) => - Task.FromResult(sut.Get()); - - public override Gen Generate(CounterState state) => - Gen.Constant(NoValue.Value); - - public override CounterState Update(CounterState state, NoValue value, Var outputVar) => - state with { CurrentCount = outputVar }; - - public override bool Ensure(Env env, CounterState oldState, CounterState newState, NoValue value, int result) - { - return result == oldState.CurrentCount.Resolve(env); - } -} - -/// -/// Sequential specification that manages Counter lifecycle -/// -public class CounterSpec : SequentialSpecification -{ - public override ICommand[] SetupCommands => [new ResetCommand()]; - - public override ICommand[] CleanupCommands => [ - new ResetCommand() - ]; - - public override CounterState InitialState => new(Var.Symbolic(0)); - - public override Range Range => Hedgehog.Linq.Range.LinearInt32(1, 50); - - public override ICommand[] Commands => - [ - new IncrementCommand(), - new DecrementCommand(), - new ResetCommand(), - new GetCommand(), - new SetCommand(), - new AddRandomCommand() - ]; -} - -public class SequentialCounterTests -{ - [Fact] - public void CounterTest() - { - var sut = new Counter(); - new CounterSpec().ToProperty(sut).Check(); - } -} diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/AsyncCounterSpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/AsyncCounterSpec.fs deleted file mode 100644 index 5061e9eb..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/AsyncCounterSpec.fs +++ /dev/null @@ -1,181 +0,0 @@ -module Hedgehog.Stateful.Tests.AsyncCounterSpec - -open Hedgehog.FSharp -open Hedgehog.Linq -open Hedgehog.Stateful -open Xunit -open System.Threading.Tasks - -/// Async Counter - all operations return Tasks -type AsyncCounter() = - let mutable value = 0 - - member _.IncrementAsync() = task { - do! Task.Delay(1) // Simulate async work - value <- value + 1 - } - - member _.DecrementAsync() = task { - do! Task.Delay(1) - value <- value - 1 - } - - member _.AddRandomAsync() = task { - do! Task.Delay(1) - let rnd = System.Random().Next(100) - value <- value + rnd - return value - } - - member _.SetAsync(n: int) = task { - do! Task.Delay(1) - value <- n - } - - member _.GetAsync() = task { - do! Task.Delay(1) - return value - } - - member _.ResetAsync() = task { - do! Task.Delay(1) - value <- 0 - } - -type AsyncCounterState = { - CurrentCount: Var -} - -/// Async Increment command -type AsyncIncrementCommand() = - inherit Command() - - override _.Name = "IncrementAsync" - - override _.Precondition _ = true - - override _.Execute(counter, _, _, _) = task { - do! counter.IncrementAsync() - return! counter.GetAsync() - } - - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(env, oldState, _, _, result) = - let oldCount = oldState.CurrentCount.Resolve(env) - result = oldCount + 1 - -/// Async Decrement command -type AsyncDecrementCommand() = - inherit Command() - - override _.Name = "DecrementAsync" - - override _.Precondition _ = true - - override _.Execute(counter, _, _, _) = task { - do! counter.DecrementAsync() - return! counter.GetAsync() - } - - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(env, oldState, _, _, result) = - let oldCount = oldState.CurrentCount.Resolve(env) - result = oldCount - 1 - -/// Async Reset command -type AsyncResetCommand() = - inherit Command() - - override _.Name = "ResetAsync" - - override _.Execute(counter, _, _, _) = task { - do! counter.ResetAsync() - return! counter.GetAsync() - } - - override _.Precondition _ = true - - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(_, _, _, _, result) = - result = 0 - -/// Async Set command -type AsyncSetCommand() = - inherit Command() - - override _.Name = "SetAsync" - - override _.Precondition _ = true - - override _.Execute(counter, _, _, value) = task { - do! counter.SetAsync(value) - return! counter.GetAsync() - } - - override _.Generate _ = Gen.int32 (Range.linearFrom 0 -10 100) - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(_, _, _, input, result) = - result = input - -/// Async Get command -type AsyncGetCommand() = - inherit Command() - - override _.Name = "GetAsync" - - override _.Precondition _ = true - - override _.Execute(counter, _, _, _) = counter.GetAsync() - - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(env, oldState, _, _, result) = - result = oldState.CurrentCount.Resolve(env) - -/// Async AddRandom command -type AsyncAddRandomCommand() = - inherit Command() - - override _.Name = "AddRandomAsync" - - override _.Precondition _ = true - - override _.Execute(counter, _, _, _) = counter.AddRandomAsync() - - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - -/// Async Counter Specification -type AsyncCounterSpec() = - inherit SequentialSpecification() - - override _.SetupCommands = [| - AsyncResetCommand() - |] - - override _.InitialState = { CurrentCount = Var.symbolic 0 } - - override _.Range = Range.linear 1 50 - - override _.Commands = [| - AsyncIncrementCommand() - AsyncDecrementCommand() - AsyncResetCommand() - AsyncGetCommand() - AsyncSetCommand() - AsyncAddRandomCommand() - |] - - -[] -let ``AsyncCounter test with async operations``() = - let sut = AsyncCounter() - AsyncCounterSpec().ToProperty(sut).Check() diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/Hedgehog.Stateful.Tests.FSharp.fsproj b/tests/Hedgehog.Stateful.Tests.FSharp/Hedgehog.Stateful.Tests.FSharp.fsproj deleted file mode 100644 index dc0cd774..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/Hedgehog.Stateful.Tests.FSharp.fsproj +++ /dev/null @@ -1,38 +0,0 @@ - - - - net8.0 - - false - false - true - Hedgehog.Stateful.Tests.FSharp - - - - - - - - - - - - - - - - - - all - runtime; build; native; contentfiles; analyzers; buildtransitive - - - - - - - - - - diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/ParallelCounterSpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/ParallelCounterSpec.fs deleted file mode 100644 index 29923345..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/ParallelCounterSpec.fs +++ /dev/null @@ -1,139 +0,0 @@ -module Hedgehog.Stateful.Tests.ParallelCounterFixtureClean - -(* - PARALLEL TESTING: Testing Linearizability of Concurrent Operations - - This example demonstrates how parallel state machine testing works. - - WHAT DOES IT TEST? - ------------------- - Parallel testing verifies that a concurrent data structure (like our ThreadSafeCounter) - is "linearizable" - meaning that despite operations running in parallel, the observed - results match what could happen if those operations executed in SOME sequential order. - - HOW DOES IT WORK? - ----------------- - 1. SEQUENTIAL PREFIX: First, a sequence of operations runs sequentially to set up - some initial state (e.g., counter might be at value 5). - - 2. PARALLEL BRANCHES: Then, TWO branches of operations run IN PARALLEL on the SAME SUT. - For example: - Thread 1: Increment, Get, Increment - Thread 2: Decrement, Get - These run concurrently - they WILL interfere with each other! - - 3. LINEARIZABILITY CHECK: After parallel execution, the framework checks if there exists - ANY valid sequential ordering of all operations that would produce the same results. - - If Branch 1 observed: [6, 6, 7] and Branch 2 observed: [5, 5], the framework checks: - - Could Increment, Decrement, Get, Increment, Get produce these results? - - Could Decrement, Increment, Get, Get, Increment produce these results? - - ... checks all possible interleavings ... - - If ANY interleaving matches, the test passes (operations are linearizable). - If NO interleaving matches, the test FAILS (there's a concurrency bug). - - WHY DOES THIS WORK? - ------------------- - The key insight: The same SUT is INTENTIONALLY shared between parallel branches. - This is not a bug - it's the whole point! We WANT operations to interfere, because - we're testing whether the SUT can handle concurrent access correctly. - - If the SUT is correctly thread-safe (like ThreadSafeCounter with Interlocked operations), - all observed results will be linearizable. - - If the SUT has concurrency bugs (e.g., unsynchronized read-modify-write), some test - runs will observe results that can't be explained by ANY sequential ordering, and the - test will fail. -*) - -open System.Threading.Tasks -open Hedgehog.FSharp -open Hedgehog.Linq -open Hedgehog.Stateful -open Xunit - -/// Thread-safe counter for parallel testing -/// This tests whether concurrent operations are linearizable -type ThreadSafeCounter() = - let mutable value = 0 - - member _.Increment() = - System.Threading.Interlocked.Increment(&value) - - member _.Decrement() = - System.Threading.Interlocked.Decrement(&value) - - member _.Get() = - System.Threading.Interlocked.CompareExchange(&value, 0, 0) - -type ParallelCounterState = { - CurrentCount: Var // Symbolic reference to current count -} - -/// Increment command - returns the new value after incrementing -type ParallelIncrementCommand() = - inherit Command() - - override _.Name = "Increment" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = Task.FromResult(counter.Increment()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - // For parallel testing, Ensure should only check weak postconditions - // The framework will verify linearizability by checking all interleavings - override _.Ensure(_, _, _, _, result) = - // In a parallel context, we can't make strong assertions about the exact value - // The linearizability checker will verify the sequence is valid - // We can only check that the result is a valid counter value - result > 0 // After increment, value should be positive (assuming we start at 0) - -/// Decrement command - returns the new value after decrementing -type ParallelDecrementCommand() = - inherit Command() - - override _.Name = "Decrement" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = Task.FromResult(counter.Decrement()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - -/// Get command - reads the current value -type ParallelGetCommand() = - inherit Command() - - override _.Name = "Get" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = Task.FromResult(counter.Get()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - -/// ParallelSpecification for testing linearizability of ThreadSafeCounter -type ParallelCounterSpec() = - inherit ParallelSpecification() - - // Initial model state - counter starts at 0 - override _.InitialState = { CurrentCount = Var.symbolic 0 } - - // Generate prefix sequences of 0-3 actions (setup some initial state) - override _.PrefixRange = Range.linear 0 3 - - // Generate branch sequences of 1-5 actions per thread - override _.BranchRange = Range.linear 1 5 - - // Commands that can run in parallel - override _.Commands = [| - ParallelIncrementCommand() - ParallelDecrementCommand() - ParallelGetCommand() - |] - -[] -let ``Parallel counter test - verifies linearizability of concurrent operations``() = - let sut = ThreadSafeCounter() - // This will: - // 1. Run a sequential prefix to set up initial state - // 2. Run two branches in parallel - // 3. Verify that the results are linearizable (match some sequential interleaving) - ParallelCounterSpec().ToProperty(sut).Check() diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/ParallelCounterWithSetupCleanupSpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/ParallelCounterWithSetupCleanupSpec.fs deleted file mode 100644 index 07257ed8..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/ParallelCounterWithSetupCleanupSpec.fs +++ /dev/null @@ -1,123 +0,0 @@ -module Hedgehog.Stateful.Tests.ParallelCounterWithSetupCleanup - -open System.Threading.Tasks -open Hedgehog.FSharp -open Hedgehog.Linq -open Hedgehog.Stateful -open Xunit - -/// Thread-safe counter for parallel testing with setup/cleanup -type ThreadSafeCounterWithTracking() = - let mutable value = 0 - let mutable setupCalled = false - let mutable cleanupCalled = false - - member _.Increment() = - System.Threading.Interlocked.Increment(&value) - - member _.Decrement() = - System.Threading.Interlocked.Decrement(&value) - - member _.Get() = - System.Threading.Interlocked.CompareExchange(&value, 0, 0) - - member _.Setup(initialValue: int) = - setupCalled <- true - System.Threading.Interlocked.Exchange(&value, initialValue) - - member _.Cleanup() = - cleanupCalled <- true - System.Threading.Interlocked.Exchange(&value, 0) - - member _.IsSetupCalled = setupCalled - member _.IsCleanupCalled = cleanupCalled - -type ParallelCounterStateWithSetup = { - CurrentCount: Var -} - -/// Setup command - initializes counter to a specific value -type SetupCounterCommand() = - inherit Command() - - override _.Name = "Setup" - override _.Precondition _ = true - override _.Execute(counter, _, _, initialValue) = - Task.FromResult(counter.Setup(initialValue)) - override _.Generate _ = Gen.int32 (Range.linearFrom 10 0 50) - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - -/// Cleanup command - resets counter to zero -type CleanupCounterCommand() = - inherit Command() - - override _.Name = "Cleanup" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = Task.FromResult(counter.Cleanup()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(_, _, _, _, result) = - // After cleanup, value should be 0 - result = 0 - -/// Increment command -type ParallelIncrementWithSetupCommand() = - inherit Command() - - override _.Name = "Increment" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = Task.FromResult(counter.Increment()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - -/// Decrement command -type ParallelDecrementWithSetupCommand() = - inherit Command() - - override _.Name = "Decrement" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = Task.FromResult(counter.Decrement()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - -/// Get command -type ParallelGetWithSetupCommand() = - inherit Command() - - override _.Name = "Get" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = Task.FromResult(counter.Get()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - -/// ParallelSpecification with setup and cleanup -type ParallelCounterWithSetupSpec() = - inherit ParallelSpecification() - - override _.InitialState = { CurrentCount = Var.symbolic 0 } - override _.PrefixRange = Range.linear 0 3 - override _.BranchRange = Range.linear 1 5 - - override _.SetupCommands = [| - SetupCounterCommand() - |] - - override _.Commands = [| - ParallelIncrementWithSetupCommand() - ParallelDecrementWithSetupCommand() - ParallelGetWithSetupCommand() - |] - - override _.CleanupCommands = [| - CleanupCounterCommand() - |] - -[] -let ``Parallel counter with setup and cleanup test``() = - let sut = ThreadSafeCounterWithTracking() - ParallelCounterWithSetupSpec().ToProperty(sut).Check() - - // Verify setup and cleanup were called - Assert.True(sut.IsSetupCalled, "Setup should have been called") - Assert.True(sut.IsCleanupCalled, "Cleanup should have been called") diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/Prelude.fs b/tests/Hedgehog.Stateful.Tests.FSharp/Prelude.fs deleted file mode 100644 index 8b3ec3aa..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/Prelude.fs +++ /dev/null @@ -1,14 +0,0 @@ -[] -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/SequentialCounterSpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/SequentialCounterSpec.fs deleted file mode 100644 index a14829b3..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/SequentialCounterSpec.fs +++ /dev/null @@ -1,145 +0,0 @@ -module Hedgehog.Stateful.Tests.CounterFixtureClean - -open Hedgehog.FSharp -open Hedgehog.Linq -open Hedgehog.Stateful -open Xunit -type Counter() = - let mutable value = 0 - member _.Increment() = value <- value + 1 - member _.Decrement() = value <- value - 1 - member _.AddRandom() = - let rnd = System.Random().Next(100) - value <- value + rnd - value - member _.Set(n: int) = - value <- n - member _.Get() = value - member _.Reset() = value <- 0 - -type CounterState = { - CurrentCount: Var // Symbolic reference to current count -} - -/// Increment command - SUT is a typed parameter! -type IncrementCommand() = - inherit Command() - - override _.Name = "Increment" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = - counter.Increment() - let result = counter.Get() // Return new value - System.Threading.Tasks.Task.FromResult(result) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(env, oldState, _, _, result) = - let oldCount = oldState.CurrentCount.Resolve(env) - result = oldCount + 1 - -type AddRandomCommand() = - inherit Command() - - override _.Name = "AddRandom" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = System.Threading.Tasks.Task.FromResult(counter.AddRandom()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - -/// Decrement command -type DecrementCommand() = - inherit Command() - - override _.Name = "Decrement" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = - counter.Decrement() - let result = counter.Get() // Return new value - System.Threading.Tasks.Task.FromResult(result) - - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(env, oldState, _, _, result) = - let oldCount = oldState.CurrentCount.Resolve(env) - result = oldCount - 1 - -/// Reset command -type ResetCommand() = - inherit Command() - - override _.Name = "Reset" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = - counter.Reset() - let result = counter.Get() // Return new value (should be 0) - System.Threading.Tasks.Task.FromResult(result) - - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(_, _, _, _, result) = - // Reset always sets to 0 - result = 0 - -/// Set command - demonstrates the bug detection -type SetCommand() = - inherit Command() - - override _.Name = "Set" - override _.Precondition _ = true - override _.Execute(counter, _, _, value) = - counter.Set(value) - let result = counter.Get() - System.Threading.Tasks.Task.FromResult(result) - override _.Generate _ = Gen.int32 (Range.linearFrom 0 -10 100) - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(_, _, _, input, result) = - Assert.Equal(result, input) - result = input - -/// Get command - returns a value -type GetCommand() = - inherit Command() - - override _.Name = "Get" - override _.Precondition _ = true - override _.Execute(counter, _, _, _) = System.Threading.Tasks.Task.FromResult(counter.Get()) - override _.Generate _ = Gen.constant () - override _.Update(_, _, outputVar) = { CurrentCount = outputVar } - - override _.Ensure(env, oldState, _, _, result) = - result = oldState.CurrentCount.Resolve(env) - -/// SequentialSpecification that manages Counter lifecycle -type CounterSpec() = - inherit SequentialSpecification() - - override _.SetupCommands = [| - ResetCommand() - |] - - // Initial model state - unbound var with default value 0 - override _.InitialState = { CurrentCount = Var.symbolic 0 } - - // Generate sequences of 1-50 actions - override _.Range = Range.linear 1 50 - - // Commands - no SUT needed in constructors! - override _.Commands = [| - IncrementCommand() - DecrementCommand() - ResetCommand() - GetCommand() - SetCommand() - AddRandomCommand() - |] - - -[] -let ``Counter test with clean SUT parameter API``() = - let sut = Counter() - // Use CheckWith to create a fresh Counter for each property test run - CounterSpec().ToProperty(sut).Check() diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/VarMapSpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/VarMapSpec.fs deleted file mode 100644 index 332c5821..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/VarMapSpec.fs +++ /dev/null @@ -1,101 +0,0 @@ -module Hedgehog.Stateful.Tests.VarMapSpec - -open System.Threading.Tasks -open Hedgehog.FSharp -open Hedgehog.Linq -open Hedgehog.Stateful -open Hedgehog.Stateful.FSharp -open Xunit - -// A structured result type -type Person = { - Name: string - Age: int -} - -// SUT that manages people -type PersonRegistry() = - let mutable people : Person list = [] - - member _.AddPerson(name: string, age: int) : Person = - let person = { Name = name; Age = age } - people <- person :: people - person - - member _.GetPeople() = people - member _.Clear() = people <- [] - -// State that tracks individual fields from the last added person -type RegistryState = { - LastPersonName: Var - LastPersonAge: Var -} - -/// Command that adds a person and returns the structured Person result -type AddPersonCommand() = - inherit Command() - - override _.Name = "AddPerson" - override _.Precondition _ = true - - override _.Execute(registry, _, _, (name, age)) = - let person = registry.AddPerson(name, age) - Task.FromResult(person) - - override _.Generate _ = - Gen.zip (Gen.alpha |> Gen.string (Range.linear 1 10)) - (Gen.int32 (Range.linear 0 100)) - - // Use Var.map to project individual fields from the Person result - override _.Update(_, _, 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 - result.Name = name && result.Age = age - -/// Specification for testing Var.map -type VarMapSpec() = - inherit SequentialSpecification() - - override _.SetupCommands = [||] - - override _.InitialState = - { LastPersonName = Var.symbolic "" - LastPersonAge = Var.symbolic 0 } - - override _.Range = Range.linear 1 20 - - override _.Commands = [| - AddPersonCommand() - |] - -[] -let ``Var.map allows projecting fields from structured command outputs``() = - let sut = PersonRegistry() - VarMapSpec().ToProperty(sut).Check() - -[] -let ``Var.map preserves symbolic variable behavior``() = - // Create a symbolic var with a default person - let personVar = Var.symbolic { Name = "Alice"; Age = 30 } - - // Map to get name - should preserve symbolic behavior - let nameVar = Var.map _.Name personVar - - // Resolve without environment should use default value - let resolvedName = nameVar.Resolve(Env.empty) - Assert.Equal("Alice", resolvedName) - -[] -let ``Var.map chains multiple projections``() = - let personVar = Var.symbolic { Name = "Bob"; Age = 25 } - - // Chain projections - let nameVar = Var.map _.Name personVar - let nameLengthVar = Var.map String.length nameVar - - // Should resolve through the chain correctly - let length = nameLengthVar.Resolve(Env.empty) - Assert.Equal(3, length) // "Bob" has length 3 diff --git a/tests/Hedgehog.Stateful.Tests.FSharp/VarReferenceSpec.fs b/tests/Hedgehog.Stateful.Tests.FSharp/VarReferenceSpec.fs deleted file mode 100644 index f92885ae..00000000 --- a/tests/Hedgehog.Stateful.Tests.FSharp/VarReferenceSpec.fs +++ /dev/null @@ -1,121 +0,0 @@ -module Hedgehog.Stateful.Tests.VarReferenceSpec - -open System.Threading.Tasks -open Hedgehog.FSharp -open Hedgehog.Linq -open Hedgehog.Stateful -open Hedgehog.Stateful.FSharp -open Xunit - -/// Simple ID registry SUT that creates and looks up IDs -type IdRegistry() = - let mutable nextId = 1 - let mutable registeredIds : Map = Map.empty - - member _.Register(name: string) : int = - let id = nextId - nextId <- nextId + 1 - registeredIds <- Map.add id name registeredIds - id - - member _.Lookup(id: int) : string option = - Map.tryFind id registeredIds - - member _.Clear() = - nextId <- 1 - registeredIds <- Map.empty - -/// State that tracks registered IDs as symbolic variables -type RegistryState = { - RegisteredIds: Var list // List of symbolic IDs from Register commands -} - -/// Command that registers a name and returns an ID -type RegisterCommand() = - inherit Command() - - override _.Name = "Register" - override _.Precondition _ = true - - override _.Execute(registry, _, _, name) = - let id = registry.Register(name) - Task.FromResult(id) - - override _.Generate _ = - Gen.alpha |> Gen.string (Range.linear 1 5) - - // Add the new ID (as Var) to the list of registered IDs - override _.Update(state, _, idVar) = - { RegisteredIds = idVar :: state.RegisteredIds } - - override _.Ensure(_, _, _, _, result) = - // IDs should be positive - result > 0 - -/// Command that looks up a previously registered ID -type LookupCommand() = - inherit Command, string option>() - - override _.Name = "Lookup" - - // Can only lookup if we have registered IDs - override _.Precondition state = - not (List.isEmpty state.RegisteredIds) - - override _.Execute(registry, env, _, idVar) = - // Resolve the symbolic ID to get the actual ID value - let actualId = Var.resolve env idVar - let result = registry.Lookup(actualId) - Task.FromResult(result) - - // Pick a random ID from the list of registered IDs - override _.Generate state = - Gen.item state.RegisteredIds - - override _.Ensure(_, _, _, _, result) = - // The ID we looked up should exist in the registry - result.IsSome - -/// Specification for testing Var references in command inputs -type VarReferenceSpec() = - inherit SequentialSpecification() - - override _.SetupCommands = [||] - - override _.InitialState = - { RegisteredIds = [] } - - override _.Range = Range.linear 1 20 - - override _.Commands = [| - RegisterCommand() - LookupCommand() - |] - -[] -let ``Commands can use Var from state as input``() = - let sut = IdRegistry() - VarReferenceSpec().ToProperty(sut).Check() - -[] -let ``Var resolves correctly during execution``() = - // Manually test that a Var can be stored and resolved - let registry = IdRegistry() - - // Register a name and get an ID - let id = registry.Register("Alice") - - // Create a bound var and bind it to the ID - let env = Env.empty - let name, env' = Env.freshName env - let boundVar = Var.bound name - let env'' = Env.add boundVar id env' - - // Resolve the var to get the ID back - let resolvedId = Var.resolve env'' boundVar - - // Lookup using the resolved ID - let result = registry.Lookup(resolvedId) - - Assert.Equal(Some "Alice", result) - Assert.Equal(id, resolvedId)