readme.md

From this blog post: http://nchammas.com/writing/how-not-to-die-hard-with-hypothesis

die_hard.py

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

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

def invariants(state):
    return (0 <= state['small'] <= 3 and
            0 <= state['big']   <= 5)

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}

@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 invariants(state)
        assert state['big'] != 4

if __name__ == '__main__':
    test()

hypothesis_fsm.py

from hypothesis import note, settings
from hypothesis.stateful import RuleBasedStateMachine, rule, invariant

class DieHardProblem(RuleBasedStateMachine):
    small = 0
    big = 0

    @rule()
    def fill_small(self):
        self.small = 3

    @rule()
    def fill_big(self):
        self.big = 5

    @rule()
    def empty_small(self):
        self.small = 0

    @rule()
    def empty_big(self):
        self.big = 0

    @rule()
    def pour_small_into_big(self):
        old_big = self.big
        self.big = min(5, self.big + self.small)
        self.small = self.small - (self.big - old_big)

    @rule()
    def pour_big_into_small(self):
        old_small = self.small
        self.small = min(3, self.small + self.big)
        self.big = self.big - (self.small - old_small)

    @invariant()
    def physics_of_jugs(self):
        assert 0 <= self.small <= 3
        assert 0 <= self.big <= 5

    @invariant()
    def die_hard_problem_not_solved(self):
        note("> small: {s} big: {b}".format(s=self.small, b=self.big))
        assert self.big != 4


# The default of 200 is sometimes not enough for Hypothesis to find
# a falsifying example.
with settings(max_examples=2000):
    DieHardTest = DieHardProblem.TestCase

requirements.txt

hypothesis
pytest