tiny.hypothesis.stateful

1pub const stateful = @import("stateful.zig");

1const std = @import("std");2const Allocator = std.mem.Allocator;3const conjecture = @import("conjecture.zig");4const ConjectureData = conjecture.ConjectureData;5const DrawError = conjecture.DrawError;6const engine_mod = @import("engine.zig");7const report_mod = @import("report.zig");8const Settings = engine_mod.Settings;910pub fn StateMachine(comptime Model: type) type {11    validateModel(Model);1213    return struct {14        const Self = @This();1516        pub fn check(allocator: Allocator) !void {17            try checkWithSettings(allocator, .{});18        }1920        pub fn checkWithSettings(allocator: Allocator, settings: Settings) !void {21            const Wrapper = struct {22                fn testFn(data: *ConjectureData, alloc: Allocator) anyerror!void {23                    try data.beginSpan("stateful");2425                    var state = Model.initialState();26                    const sut = try Model.initSut(alloc);27                    defer Model.deinitSut(sut, alloc);2829                    const max_commands: usize = 50;30                    for (0..max_commands) |_| {31                        const more = data.drawBoolean() catch break;32                        if (!more) break;3334                        try data.beginSpan("command");3536                        const cmd = Model.genCommand(state, data, alloc) catch break;3738                        if (!Model.precondition(state, cmd)) {39                            data.endSpan();40                            continue;41                        }4243                        const result = Model.runCommand(cmd, sut);4445                        if (!Model.postcondition(state, cmd, result)) {46                            data.endSpan();47                            data.endSpan();48                            return error.PostconditionFailed;49                        }5051                        state = Model.nextState(state, cmd);52                        data.endSpan();53                    }5455                    data.endSpan();56                }57            };5859            var result = try engine_mod.run(allocator, &Wrapper.testFn, settings);60            defer result.deinit();6162            if (!result.passed) {63                if (settings.report_failure) {64                    report_mod.printStatefulFailure(&result);65                }66                return error.StatefulTestFailed;67            }68        }69    };70}7172fn validateModel(comptime Model: type) void {73    const info = @typeInfo(Model);74    if (info != .@"struct") @compileError("StateMachine Model must be a struct");7576    if (!@hasDecl(Model, "State")) @compileError("Model must declare 'State' type");77    if (!@hasDecl(Model, "Command")) @compileError("Model must declare 'Command' type");78    if (!@hasDecl(Model, "Sut")) @compileError("Model must declare 'Sut' type");7980    if (!@hasDecl(Model, "initialState")) @compileError("Model must declare 'initialState()'");81    if (!@hasDecl(Model, "genCommand")) @compileError("Model must declare 'genCommand()'");82    if (!@hasDecl(Model, "precondition")) @compileError("Model must declare 'precondition()'");83    if (!@hasDecl(Model, "nextState")) @compileError("Model must declare 'nextState()'");84    if (!@hasDecl(Model, "postcondition")) @compileError("Model must declare 'postcondition()'");85    if (!@hasDecl(Model, "runCommand")) @compileError("Model must declare 'runCommand()'");86    if (!@hasDecl(Model, "initSut")) @compileError("Model must declare 'initSut()'");87    if (!@hasDecl(Model, "deinitSut")) @compileError("Model must declare 'deinitSut()'");88}8990const StackModel = struct {91    pub const State = struct {92        size: usize = 0,93    };9495    pub const Command = union(enum) {96        push: i32,97        pop,98    };99100    pub const Sut = struct {101        items: std.ArrayListUnmanaged(i32) = .empty,102        allocator: Allocator,103104        fn init(allocator: Allocator) Sut {105            return .{ .allocator = allocator };106        }107108        fn deinit(self: *Sut) void {109            self.items.deinit(self.allocator);110        }111    };112113    pub fn initialState() State {114        return .{};115    }116117    pub fn genCommand(state: State, data: *ConjectureData, _: Allocator) DrawError!Command {118        if (state.size == 0) {119            const val_raw = try data.drawInteger(0, 200, 100);120            const val: i32 = @intCast(val_raw);121            return .{ .push = val - 100 };122        }123        const choice = try data.drawBoolean();124        if (choice) {125            return .pop;126        } else {127            const val_raw = try data.drawInteger(0, 200, 100);128            const val: i32 = @intCast(val_raw);129            return .{ .push = val - 100 };130        }131    }132133    pub fn precondition(state: State, cmd: Command) bool {134        return switch (cmd) {135            .pop => state.size > 0,136            .push => true,137        };138    }139140    pub fn nextState(state: State, cmd: Command) State {141        return switch (cmd) {142            .push => .{ .size = state.size + 1 },143            .pop => .{ .size = state.size - 1 },144        };145    }146147    pub fn postcondition(state: State, cmd: Command, _: void) bool {148        _ = state;149        _ = cmd;150        return true;151    }152153    pub fn runCommand(cmd: Command, sut: *Sut) void {154        switch (cmd) {155            .push => |v| sut.items.append(sut.allocator, v) catch {},156            .pop => {157                _ = sut.items.pop();158            },159        }160    }161162    pub fn initSut(allocator: Allocator) !*Sut {163        const sut = try allocator.create(Sut);164        sut.* = Sut.init(allocator);165        return sut;166    }167168    pub fn deinitSut(sut: *Sut, allocator: Allocator) void {169        sut.deinit();170        allocator.destroy(sut);171    }172};173174test "stateful: stack model" {175    const allocator = std.testing.allocator;176    try StateMachine(StackModel).check(allocator);177}178179const BrokenDepthModel = struct {180    pub const State: type = StackModel.State;181    pub const Command: type = StackModel.Command;182    pub const Sut: type = StackModel.Sut;183184    pub const initialState = StackModel.initialState;185    pub const genCommand = StackModel.genCommand;186    pub const precondition = StackModel.precondition;187    pub const nextState = StackModel.nextState;188    pub const runCommand = StackModel.runCommand;189    pub const initSut = StackModel.initSut;190    pub const deinitSut = StackModel.deinitSut;191192    pub fn postcondition(state: State, cmd: Command, _: void) bool {193        return switch (cmd) {194            .push => state.size < 2,195            .pop => true,196        };197    }198};199200test "stateful: failing postcondition shrinks without corrupting memory" {201    const allocator = std.testing.allocator;202    try std.testing.expectError(203        error.StatefulTestFailed,204        StateMachine(BrokenDepthModel).checkWithSettings(allocator, .{205            .seed = 7,206            .report_failure = false,207        }),208    );209}