lib/hypothesis/src/stateful.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const std = @import("std");
2 const Allocator = std.mem.Allocator;
3 const conjecture = @import("conjecture.zig");
4 const ConjectureData = conjecture.ConjectureData;
5 const DrawError = conjecture.DrawError;
6 const engine_mod = @import("engine.zig");
7 const report_mod = @import("report.zig");
8 const Settings = engine_mod.Settings;
9
10 pub fn StateMachine(comptime Model: type) type {
11 validateModel(Model);
12
13 return struct {
14 const Self = @This();
15
16 pub fn check(allocator: Allocator) !void {
17 try checkWithSettings(allocator, .{});
18 }
19
20 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");
24
25 var state = Model.initialState();
26 const sut = try Model.initSut(alloc);
27 defer Model.deinitSut(sut, alloc);
28
29 const max_commands: usize = 50;
30 for (0..max_commands) |_| {
31 const more = data.drawBoolean() catch break;
32 if (!more) break;
33
34 try data.beginSpan("command");
35
36 const cmd = Model.genCommand(state, data, alloc) catch break;
37
38 if (!Model.precondition(state, cmd)) {
39 data.endSpan();
40 continue;
41 }
42
43 const result = Model.runCommand(cmd, sut);
44
45 if (!Model.postcondition(state, cmd, result)) {
46 data.endSpan();
47 data.endSpan();
48 return error.PostconditionFailed;
49 }
50
51 state = Model.nextState(state, cmd);
52 data.endSpan();
53 }
54
55 data.endSpan();
56 }
57 };
58
59 var result = try engine_mod.run(allocator, &Wrapper.testFn, settings);
60 defer result.deinit();
61
62 if (!result.passed) {
63 if (settings.report_failure) {
64 report_mod.printStatefulFailure(&result);
65 }
66 return error.StatefulTestFailed;
67 }
68 }
69 };
70 }
71
72 fn validateModel(comptime Model: type) void {
73 const info = @typeInfo(Model);
74 if (info != .@"struct") @compileError("StateMachine Model must be a struct");
75
76 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");
79
80 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 }
89
90 const StackModel = struct {
91 pub const State = struct {
92 size: usize = 0,
93 };
94
95 pub const Command = union(enum) {
96 push: i32,
97 pop,
98 };
99
100 pub const Sut = struct {
101 items: std.ArrayListUnmanaged(i32) = .empty,
102 allocator: Allocator,
103
104 fn init(allocator: Allocator) Sut {
105 return .{ .allocator = allocator };
106 }
107
108 fn deinit(self: *Sut) void {
109 self.items.deinit(self.allocator);
110 }
111 };
112
113 pub fn initialState() State {
114 return .{};
115 }
116
117 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 }
132
133 pub fn precondition(state: State, cmd: Command) bool {
134 return switch (cmd) {
135 .pop => state.size > 0,
136 .push => true,
137 };
138 }
139
140 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 }
146
147 pub fn postcondition(state: State, cmd: Command, _: void) bool {
148 _ = state;
149 _ = cmd;
150 return true;
151 }
152
153 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 }
161
162 pub fn initSut(allocator: Allocator) !*Sut {
163 const sut = try allocator.create(Sut);
164 sut.* = Sut.init(allocator);
165 return sut;
166 }
167
168 pub fn deinitSut(sut: *Sut, allocator: Allocator) void {
169 sut.deinit();
170 allocator.destroy(sut);
171 }
172 };
173
174 test "stateful: stack model" {
175 const allocator = std.testing.allocator;
176 try StateMachine(StackModel).check(allocator);
177 }
178
179 const BrokenDepthModel = struct {
180 pub const State: type = StackModel.State;
181 pub const Command: type = StackModel.Command;
182 pub const Sut: type = StackModel.Sut;
183
184 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;
191
192 pub fn postcondition(state: State, cmd: Command, _: void) bool {
193 return switch (cmd) {
194 .push => state.size < 2,
195 .pop => true,
196 };
197 }
198 };
199
200 test "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 }