die-hard.py

# The MIT License (MIT) 
# Copyright (c) 2022-present Nathan Todd-Stone 
# https://en.wikipedia.org/wiki/MIT_License#License_terms

from hypothesis import given, settings
from hypothesis.strategies import lists, sampled_from

def new_state():
    return {'big': 0, 'small': 0}

def desired_state(state):
    return state['big'] != 4

def empty_big(state):
    return {'big': 0, 'small': state['small']}

def fill_big(state):
    return {'big': 5, 'small': state['small']}

def empty_small(state):
    return {'big': state['big'], 'small': 0}

def fill_small(state):
    return {'big': state['big'], 'small': 3}

def pour_big_to_small(state):
    new_small = min(3, state['big'] + state['small'])
    amount_poured = new_small - state['small']
    return {'big': state['big'] - amount_poured,
            'small': new_small}

def pour_small_to_big(state):
    new_big = min(5, state['big'] + state['small'])
    amount_poured = new_big - state['big']
    return {'big': new_big,
            'small': state['small'] - amount_poured}

def message(actions):
    msg = '\n\nstate transitions:\n'
    state = new_state()
    for action in actions:
        msg += ' state: %s\n' % state
        state = action(state)
        msg += ' action: %s\n' % action.__name__
    msg += ' state: %s\n' % state
    return msg

@given(lists(sampled_from([empty_big, empty_small, fill_big, fill_small, pour_big_to_small, pour_small_to_big])))
@settings(max_examples=10000)
def test(actions):
    state = new_state()
    for action in actions:
        state = action(state)
        assert desired_state(state), message(actions)

if __name__ == '__main__':
    test()