graduate_code/solutions/contracts.py

"""G01: a finite state model. This is sequential, not a thread model."""
from collections import deque
from dataclasses import dataclass


@dataclass(frozen=True)
class Stock:
    available: int
    sold: int = 0


def reserve(state: Stock, amount: int) -> Stock:
    if any(type(x) is not int or x < 0
           for x in (state.available, state.sold, amount)):
        raise ValueError("nonnegative mathematical integers required")
    if amount > state.available:
        return state
    return Stock(state.available - amount, state.sold + amount)


def explore(initial: int, max_amount: int = 4) -> set[Stock]:
    if (type(initial) is not int or not 0 <= initial <= 100
            or type(max_amount) is not int or not 0 <= max_amount <= 100):
        raise ValueError("finite model bounds must be integers in [0,100]")
    start = Stock(initial)
    seen, todo = {start}, deque([start])
    while todo:
        state = todo.popleft()
        for amount in range(max_amount + 1):
            nxt = reserve(state, amount)
            if nxt.available < 0 or nxt.available + nxt.sold != initial:
                raise AssertionError((state, amount, nxt))
            if nxt not in seen:
                seen.add(nxt)
                todo.append(nxt)
    return seen


if __name__ == "__main__":
    print(sorted(explore(4), key=lambda s: s.sold))