//! a map that caches the sum of its values and forgets to invalidate the
//! cache when a put overwrites an existing key. the minimal history is
//! put(k0, 0); sum(); put(k0, 1); sum().

const std = @import("std");
const hegel = @import("hegel");

const Toy = struct {
    values: [4]?u8 = @splat(null),
    cached: ?u32 = null,

    fn put(self: *Toy, key: usize, value: u8) void {
        if (self.values[key] == null) self.cached = null;
        self.values[key] = value;
    }

    fn sum(self: *Toy) u32 {
        if (self.cached) |s| return s;
        self.cached = self.recompute();
        return self.cached.?;
    }

    fn count(self: *const Toy) u64 {
        var keys: u64 = 0;
        for (self.values) |value| keys += @intFromBool(value != null);
        return keys;
    }

    fn recompute(self: *const Toy) u32 {
        var total: u32 = 0;
        for (self.values) |value| total += value orelse 0;
        return total;
    }
};

const Rule = enum { put, sum };

var tally: hegel.Tally(Rule) = .{};

fn property(_: void, case: *hegel.TestCase) !void {
    var toy: Toy = .{};
    tally.case();
    var machine = try case.machine(Rule, &.{ 2, 1 }, 20);
    defer machine.deinit();
    while (try machine.next()) |rule| {
        tally.step(rule);
        switch (rule) {
            .put => {
                const key = try case.index(4);
                const value = try case.int(u8, 0, 255);
                case.note("put(k{d}, {d})", .{ key, value });
                toy.put(key, value);
            },
            .sum => {
                case.note("sum()", .{});
                if (toy.sum() != toy.recompute()) return case.fail("sum() disagrees with a recompute");
            },
        }
    }
    tally.finish(toy.count());
}

pub fn main() void {
    const outcome = hegel.run(.{ .test_cases = 500 }, {}, property);
    tally.print();
    outcome catch {
        std.debug.print("\nfound the planted bug, as expected\n", .{});
        return;
    };
    std.debug.print("the planted bug was not found\n", .{});
    std.process.exit(1);
}