diff --git a/agent/skills/concurrency/SKILL.md b/agent/skills/concurrency/SKILL.md index d6c343f..d9a125a 100644 --- a/agent/skills/concurrency/SKILL.md +++ b/agent/skills/concurrency/SKILL.md @@ -89,15 +89,19 @@ public async Task ConcurrentTests_FindsRaceConditions() spec.GetOperation<(string, string), ApiResult>("BookSlot").With(("9am", "Bob"), "Bob books"), }; + var testCases = spec.GenerateConcurrentTests( + new BookingState(), + inputs, + new TestGenerationOptions { MaxDepth = 4 }); + var context = spec.CreateTestingContext(); context.Register(new BookingApiClient(CreateHttpClient())); - var results = await spec.RunConcurrentTests( + var results = await spec.RunTests( context, new BookingState(), - inputs, - generationOptions: new TestGenerationOptions { MaxDepth = 4 }, - executionOptions: new TestExecutionOptions + testCases, + new TestExecutionOptions { BeforeEachAsync = async _ => await ResetDatabase() }); diff --git a/agent/skills/operations/SKILL.md b/agent/skills/operations/SKILL.md index fa5128e..f46ab56 100644 --- a/agent/skills/operations/SKILL.md +++ b/agent/skills/operations/SKILL.md @@ -63,7 +63,7 @@ public class WithdrawOperation : Operation, public override async Task> ExecuteAsync( WithdrawRequest request, - ITestContext context) + TestingContext context) { var client = context.Get(); return await client.WithdrawAsync(request.AccountId, request.Amount); diff --git a/agent/skills/quickref/SKILL.md b/agent/skills/quickref/SKILL.md index c991890..eeca88e 100644 --- a/agent/skills/quickref/SKILL.md +++ b/agent/skills/quickref/SKILL.md @@ -186,12 +186,11 @@ Assert.That(results.All(r => r.Success)); ## Concurrent Tests ```csharp -var results = await spec.RunConcurrentTests( - context, - initialState, - inputs, - generationOptions: new TestGenerationOptions { MaxDepth = 4 }, - executionOptions: new TestExecutionOptions { ... }); +var concurrentTestCases = spec.GenerateConcurrentTests(initialState, inputs, + new TestGenerationOptions { MaxDepth = 4 }); + +var results = await spec.RunTests(context, initialState, concurrentTestCases, + new TestExecutionOptions { ... }); ``` ## Manual Conformance Testing @@ -220,7 +219,7 @@ File.WriteAllText("graph.dot", dot); |--------|------|---------|-------------| | `MaxDepth` | int | 5 | Max sequence length | | `StateConstraint` | Func | null | Prune states | -| `MaxConcurrencyLevel` | int | 2 | Concurrent ops | +| `MaxConcurrencyLevel` | int | 3 | Concurrent ops | | `SequentialTestCaseAlgorithm` | delegate | StateCoverage | Walk algorithm | ## Test Case Algorithms diff --git a/agent/skills/test-generation/SKILL.md b/agent/skills/test-generation/SKILL.md index 294eb71..67bd498 100644 --- a/agent/skills/test-generation/SKILL.md +++ b/agent/skills/test-generation/SKILL.md @@ -44,7 +44,7 @@ var testCases = spec.GenerateTests(initialState, inputs, new TestGenerationOptio |--------|-------------|---------| | `MaxDepth` | Maximum sequence length | 5 | | `StateConstraint` | Prune states during exploration | None | -| `MaxConcurrencyLevel` | For concurrent test generation | 2 | +| `MaxConcurrencyLevel` | For concurrent test generation | 3 | | `SequentialTestCaseAlgorithm` | How paths are extracted | StateCoverage | ### Constraining the State Space @@ -135,7 +135,7 @@ Assert.IsEmpty(failures, $"Failed: {failures.FirstOrDefault()?.LastFailureMessag |--------|-------------| | `BeforeEachAsync` | Reset system before each test case | | `AfterEachAsync` | Cleanup after each test case | -| `LogLevel` | Control verbosity | +| `OnStepExecuted` | Log each operation's request/response for debugging | ## Resetting State @@ -170,8 +170,7 @@ File.WriteAllText("state-graph.dot", dot); ### Custom Node Labels ```csharp -var dot = TestCaseGenerator.VisualizeStateSpace( - new TestingContext(spec), +var dot = spec.VisualizeStateSpace( initialState, inputs, new TestGenerationOptions { MaxDepth = 3 }, @@ -259,5 +258,5 @@ public async Task AutoGeneratedTests() ## Next Steps -- **Concurrency Testing**: Test race conditions with `RunConcurrentTests` +- **Concurrency Testing**: Test race conditions with `GenerateConcurrentTests` and `RunTests` - **Async Operations**: Handle background work with polling diff --git a/agent/skills/troubleshooting/SKILL.md b/agent/skills/troubleshooting/SKILL.md index 889b33b..66b30e4 100644 --- a/agent/skills/troubleshooting/SKILL.md +++ b/agent/skills/troubleshooting/SKILL.md @@ -264,7 +264,8 @@ var seqResults = await spec.RunTests(context, initialState, testCases); Assert.That(seqResults.All(r => r.Success), "Fix sequential tests first!"); // Then run concurrent -var concResults = await spec.RunConcurrentTests(context, initialState, inputs, options); +var concTestCases = spec.GenerateConcurrentTests(initialState, inputs, options); +var concResults = await spec.RunTests(context, initialState, concTestCases); ``` ### Non-Deterministic Failures @@ -282,7 +283,8 @@ var concResults = await spec.RunConcurrentTests(context, initialState, inputs, o for (int i = 0; i < 10; i++) { await ResetState(); - var result = await spec.RunConcurrentTests(...); + var concTestCases = spec.GenerateConcurrentTests(initialState, inputs, options); + var result = await spec.RunTests(context, initialState, concTestCases); Console.WriteLine($"Run {i}: {(result.All(r => r.Success) ? "PASS" : "FAIL")}"); } ``` @@ -342,7 +344,11 @@ Console.WriteLine($"Remaining possible states: {stateProfile.StatesAndStepFuncti ```csharp var results = await spec.RunTests(context, initialState, testCases, new TestExecutionOptions { - LogLevel = LogLevel.Verbose + OnStepExecuted = info => + { + foreach (var (op, req, resp) in info.Operations) + Console.WriteLine($"{op.Name}({req}) → {resp}"); + } }); ``` diff --git a/agent/starter/ExampleTests.cs b/agent/starter/ExampleTests.cs index 7f6a30c..9368901 100644 --- a/agent/starter/ExampleTests.cs +++ b/agent/starter/ExampleTests.cs @@ -25,13 +25,7 @@ public async Task GeneratedSequentialTests() .BindAsync("Delete", (client, key) => client.DeleteAsync(key)); - // 3. Provide a way to get a fresh client and initial state - spec.ProvideTargetAndInitialState(() => ( - new KvClient(/* your HttpClient or service reference */), - new KvState() // Empty — no items exist initially - )); - - // 4. Define inputs — Accordant explores all sequences of these + // 3. Define inputs — Accordant explores all sequences of these var put = spec.GetOperation("Put"); var get = spec.GetOperation>("Get"); var delete = spec.GetOperation("Delete"); @@ -45,14 +39,22 @@ public async Task GeneratedSequentialTests() delete.With("key1", "Delete key1"), }; - // 5. Run tests + // 4. Generate test cases + var initialState = new KvState(); + var testCases = spec.GenerateTests(initialState, inputs, new TestGenerationOptions + { + MaxDepth = 4 // Sequences up to 4 operations long + }); + + // 5. Create context and run tests + var context = spec.CreateTestingContext(); + context.Register(new KvClient(/* your HttpClient or service reference */)); + var results = await spec.RunTests( - inputs, - generationOptions: new TestGenerationOptions - { - MaxDepth = 4 // Sequences up to 4 operations long - }, - executionOptions: new TestExecutionOptions + context, + initialState, + testCases, + new TestExecutionOptions { BeforeEachAsync = async ctx => { diff --git a/agent/starter/README.md b/agent/starter/README.md index a56331e..383d4b2 100644 --- a/agent/starter/README.md +++ b/agent/starter/README.md @@ -14,7 +14,7 @@ Use this as a reference when helping a user build their first spec. Adapt the pa |------|---------| | `ExampleState.cs` | The `[State]` class — minimal, just what operations need | | `ExampleSpec.cs` | A few related operations with error cases and success cases | -| `ExampleTests.cs` | Wiring up execution, state reset, inputs, and running tests | +| `ExampleTests.cs` | Wiring up execution, generating tests, state reset, and running tests | ## Key Patterns Shown @@ -26,4 +26,4 @@ Use this as a reference when helping a user build their first spec. Adapt the pa - Execution bindings with `spec.ExecuteWith().BindAsync(...)` - `InputSet` with labeled inputs - `BeforeEachAsync` for state reset -- `spec.RunTests(...)` to generate and execute +- `spec.GenerateTests(...)` and `spec.RunTests(...)` to generate and execute diff --git a/docs/concepts/conformance-testing.md b/docs/concepts/conformance-testing.md index 54dcb66..ab20bc6 100644 --- a/docs/concepts/conformance-testing.md +++ b/docs/concepts/conformance-testing.md @@ -261,7 +261,7 @@ public async Task SequentialConformanceTests() var testCases = spec.GenerateTests(initialState, inputs); var results = await spec.RunTests(context, initialState, testCases); - Assert.IsTrue(results.All(r => r.Passed)); + Assert.IsTrue(results.All(r => r.Success)); } [TestMethod] @@ -275,7 +275,7 @@ public async Task ConcurrentConformanceTests() var testCases = spec.GenerateConcurrentTests(initialState, inputs); var results = await spec.RunTests(context, initialState, testCases); - Assert.IsTrue(results.All(r => r.Passed)); + Assert.IsTrue(results.All(r => r.Success)); } ``` diff --git a/docs/concepts/models-vs-fakes.md b/docs/concepts/models-vs-fakes.md index a0035ca..1fd083f 100644 --- a/docs/concepts/models-vs-fakes.md +++ b/docs/concepts/models-vs-fakes.md @@ -36,7 +36,8 @@ public class KeyValueFake ### As a Model ```csharp -public class KeyValueState : JsonState +[State] +public partial class KeyValueState { public Dictionary Store { get; set; } = new(); } diff --git a/docs/concepts/operations-and-expect.md b/docs/concepts/operations-and-expect.md index 47cc48d..0ed2607 100644 --- a/docs/concepts/operations-and-expect.md +++ b/docs/concepts/operations-and-expect.md @@ -11,9 +11,14 @@ An **operation** represents a single, atomic action your system can perform — Every operation has a name, a typed request, and a typed response. The key design decision: *specification* and *execution* are separate. ```csharp +// Define the spec (Apply): what SHOULD happen spec.Operation("Withdraw", - (request, state) => { ... }) // Apply: what SHOULD happen - .WithExecution(async (request, ctx) => { ... }); // Execute: what ACTUALLY happens + (request, state) => { ... }); + +// Bind execution: what ACTUALLY happens +spec.ExecuteWith() + .BindAsync("Withdraw", + (client, request) => client.WithdrawAsync(request)); ``` The **Apply** method describes valid behavior. Given this request and this state, what should the response look like? How should the state change? Apply doesn't touch the real system — it's pure logic, a specification of correctness. @@ -187,16 +192,18 @@ So far we've talked about Apply — the specification side. But at some point, y When you define operations as classes, you override both Apply and ExecuteAsync: ```csharp -public class WithdrawOperation : Operation +public class WithdrawOperation : Operation { + public WithdrawOperation() : base("Withdraw") { } + public override ExpectedOutcomes Apply(WithdrawRequest request, BankState state) { // ... spec logic ... } public override async Task ExecuteAsync( - WithdrawRequest request, - ITestContext context) + TestingContext context, + WithdrawRequest request) { var client = context.Get(); var response = await client.PostAsync($"/accounts/{request.Id}/withdraw", ...); @@ -212,9 +219,11 @@ Apply says what *should* happen. ExecuteAsync makes it *actually* happen. For simpler specs, you can define everything inline: ```csharp -spec.Operation("GetBalance", (request, state) => { ... }) - .WithExecution(async (request, ctx) => - await ctx.Get().GetBalanceAsync(request.AccountId)); +spec.Operation("GetBalance", (request, state) => { ... }); + +spec.ExecuteWith() + .BindAsync("GetBalance", + (client, request) => client.GetBalanceAsync(request.AccountId)); ``` Same separation, more compact syntax. diff --git a/docs/how-to/indefinite-failures.md b/docs/how-to/indefinite-failures.md index 5f9d82b..fbb4dea 100644 --- a/docs/how-to/indefinite-failures.md +++ b/docs/how-to/indefinite-failures.md @@ -133,8 +133,8 @@ spec.Operation>("CreateJob", (jobName, state) => return Expect.OneOf( // Success - server created the job and assigned an ID Expect.That>(r => r.IsSuccess && !string.IsNullOrEmpty(r.Data.JobId)) - .ThenState>( - (response, next) => + .ThenState( + (ApiResult response, AppState next) => next.Jobs[response.Data.JobId] = new JobState { Name = jobName, diff --git a/docs/tutorials/01-your-first-spec.md b/docs/tutorials/01-your-first-spec.md index 4f27908..cd76225 100644 --- a/docs/tutorials/01-your-first-spec.md +++ b/docs/tutorials/01-your-first-spec.md @@ -277,12 +277,7 @@ public async Task SequentialTests_UsersAndTodos() { using var factory = new TodoServiceFactory(); // Starts the API var spec = CreateSpec(); - - // Tell the spec how to get a client and initial state - spec.ProvideTargetAndInitialState(() => ( - new TodoApiClient(factory.CreateTestClient()), - new AppState() // Empty state - )); + var client = new TodoApiClient(factory.CreateTestClient()); // Get operation references for building inputs var createUser = spec.GetOperation>("CreateUser"); @@ -300,21 +295,27 @@ public async Task SequentialTests_UsersAndTodos() getTodo.With(("alice", "todo-1"), "Get todo"), }; + // Generate test sequences from inputs + var initialState = new AppState(); + var testCases = spec.GenerateTests(initialState, inputs, new TestGenerationOptions + { + MaxDepth = 4 // Sequences up to length 4 + }); + + // Create a testing context and register the client + var context = spec.CreateTestingContext(); + context.Register(client); + // Run the tests - var results = await spec.RunTests( - inputs, - generationOptions: new TestGenerationOptions - { - MaxDepth = 4 // Sequences up to length 4 - }, - executionOptions: new TestExecutionOptions + var results = await spec.RunTests(context, initialState, testCases, + new TestExecutionOptions { - BeforeEachAsync = async ctx => + BeforeEachAsync = async info => { // Reset database before each test - var client = ctx.Context.Get(); - await client.DeleteUserAsync("alice"); - await client.DeleteUserAsync("unknown"); + var c = info.Context.Get(); + await c.DeleteUserAsync("alice"); + await c.DeleteUserAsync("unknown"); } }); @@ -375,7 +376,7 @@ You've learned the core Accordant workflow: 1. **Define State** - `[State]` partial class tracking what matters 2. **Define Operations** - `spec.Operation(...)` with `Expect.That(...)` 3. **Bind Execution** - `spec.ExecuteWith().BindAsync(...)` -4. **Configure & Run** - `ProvideTargetAndInitialState`, `InputSet`, `RunTests` +4. **Configure & Run** - `CreateTestingContext`, `Register`, `InputSet`, `GenerateTests`, `RunTests` ### Key Concepts @@ -386,6 +387,8 @@ You've learned the core Accordant workflow: | `.SameState()` | Operation doesn't change state | | `.ThenState(newState)` | Operation transitions to new state | | `InputSet` | Values to try—Accordant explores sequences | +| `CreateTestingContext` | Create context for DI and test execution | +| `context.Register(client)` | Register your API client for use during tests | | `MaxDepth` | Limit sequence length | | `BeforeEachAsync` | Reset state before each test | diff --git a/docs/tutorials/03-response-dependent-state.md b/docs/tutorials/03-response-dependent-state.md index 176d9cd..61036c0 100644 --- a/docs/tutorials/03-response-dependent-state.md +++ b/docs/tutorials/03-response-dependent-state.md @@ -39,7 +39,7 @@ Accordant handles this with a two-part approach: ### Part 1: Capture with Response Lambda -When creating a todo, use `.ThenState` which passes both a cloned state and the response to your lambda: +When creating a todo, use `.ThenState` which passes both a cloned state and the response to your lambda: ```csharp spec.Operation>("CreateTodo", (request, state) => @@ -65,9 +65,9 @@ spec.Operation>("CreateTodo", (request, state) => r.Data.TodoId == request.TodoId && r.Data.LastModified != null, // Just verify it exists "Should create todo with timestamp") - .ThenState>( + .ThenState( // Lambda receives response and clone, modifies the clone - (response, nextState) => + (ApiResult response, AppState nextState) => nextState.Users[request.UserId].Todos[request.TodoId] = new TodoState { Title = request.Title, @@ -174,8 +174,8 @@ spec.Operation>("CreateOrder", (request, st !string.IsNullOrEmpty(r.Data.OrderId) && // Server generates r.Data.Product == request.Product, "Should create order with server-generated ID") - .ThenState>( - (response, nextState) => + .ThenState( + (ApiResult response, AppState nextState) => { var orderId = response.Data!.OrderId; // Capture! nextState.Orders[orderId] = new OrderState @@ -210,8 +210,8 @@ if (job.ResultPath == null && response.Data.Status == JobStatus.Completed) return Expect.That>( r => r.Data.ResultPath != null, "Should have a ResultPath") - .ThenState>( - (resp, nextState) => + .ThenState( + (ApiResult resp, JobQueueState nextState) => nextState.Jobs[jobId].ResultPath = resp.Data!.ResultPath, // Capture mock: () => new ApiResult { /* ... */ }); } @@ -236,7 +236,7 @@ Response-dependent state handles values you can't predict: | Pattern | Use Case | |---------|----------| -| `.ThenState((response, nextState) => ..., mock)` | Capture server-generated values | +| `.ThenState((TResponse response, TState nextState) => ..., mock)` | Capture server-generated values | | Mock responses | Enable state exploration without real server | | Stability checks | Enforce values don't change unexpectedly | diff --git a/docs/tutorials/04-visualizing-state-space.md b/docs/tutorials/04-visualizing-state-space.md index 1054846..a34bc90 100644 --- a/docs/tutorials/04-visualizing-state-space.md +++ b/docs/tutorials/04-visualizing-state-space.md @@ -133,8 +133,7 @@ Before running tests, check that the state graph matches your mental model: You can customize how nodes are labeled: ```csharp -var dotContent = TestCaseGenerator.VisualizeStateSpace( - new TestingContext(spec), +var dotContent = spec.VisualizeStateSpace( new AppState(), inputs, new TestGenerationOptions { MaxDepth = 3 }, @@ -187,7 +186,7 @@ Visualization helps you understand and debug: ### Key Command ```csharp -var dot = TestCaseGenerator.VisualizeStateSpace(context, initialState, inputs, options); +var dot = spec.VisualizeStateSpace(initialState, inputs, options); File.WriteAllText("graph.dot", dot); // Then: dot -Tpng graph.dot -o graph.png ``` diff --git a/docs/tutorials/05-testing-race-conditions.md b/docs/tutorials/05-testing-race-conditions.md index 1c2a62f..9f55c90 100644 --- a/docs/tutorials/05-testing-race-conditions.md +++ b/docs/tutorials/05-testing-race-conditions.md @@ -5,7 +5,7 @@ Concurrency bugs are notoriously hard to find. A system might work perfectly in **Time:** 20 minutes **What you'll learn:** -- Using `RunConcurrentTests` to test interleavings +- Using `GenerateConcurrentTests` to test interleavings - Understanding linearizability (the correctness criterion) - The "double-booking" pattern for finding race conditions @@ -114,7 +114,7 @@ private static Spec CreateSpec() ## Running Concurrent Tests -The magic is in `RunConcurrentTests`: +The magic is in `GenerateConcurrentTests`: ```csharp [Test] @@ -122,10 +122,7 @@ public async Task ConcurrentTests_DoubleBookingPrevented() { using var factory = new BookingServiceFactory(); var spec = CreateSpec(); - - spec.ProvideTargetAndInitialState(() => ( - new BookingApiClient(factory.CreateTestClient()), - new BookingState())); + var client = new BookingApiClient(factory.CreateTestClient()); var createSlot = spec.GetOperation>("CreateSlot"); var bookSlot = spec.GetOperation<(string, string), ApiResult>("BookSlot"); @@ -144,15 +141,24 @@ public async Task ConcurrentTests_DoubleBookingPrevented() getSlot.With("9am", "Check who got the slot"), }; - var results = await spec.RunConcurrentTests( // <-- Note: RunConcurrentTests - inputs, - generationOptions: new TestGenerationOptions { MaxDepth = 4 }, - executionOptions: new TestExecutionOptions + // Generate concurrent test cases + var initialState = new BookingState(); + var testCases = spec.GenerateConcurrentTests( // <-- Generates concurrent tests + initialState, inputs, + new TestGenerationOptions { MaxDepth = 4 }); + + // Create context and register client + var context = spec.CreateTestingContext(); + context.Register(client); + + // Run the tests + var results = await spec.RunTests(context, initialState, testCases, + new TestExecutionOptions { - BeforeEachAsync = async ctx => + BeforeEachAsync = async info => { - var client = ctx.Context.Get(); - await client.DeleteSlotAsync("9am"); + var c = info.Context.Get(); + await c.DeleteSlotAsync("9am"); } }); @@ -189,7 +195,7 @@ T3: GetSlot("9am") ## What Gets Generated -`RunConcurrentTests` generates test cases with concurrent operation pairs: +`GenerateConcurrentTests` generates test cases with concurrent operation pairs: ``` Test Case 1: @@ -284,7 +290,7 @@ Concurrent testing finds race conditions: | Concept | Meaning | |---------|---------| -| `RunConcurrentTests` | Tests operations running in parallel | +| `GenerateConcurrentTests` | Generates test cases with concurrent operations | | Linearizability | Results must match some sequential order | | Double-booking | Classic race condition pattern |