Skip to content

Instantly share code, notes, and snippets.

@wting
Forked from nathants/die-hard.py
Last active April 7, 2017 00:16
Show Gist options
  • Save wting/1da9178705429cb8d98c7db7c19f4fff to your computer and use it in GitHub Desktop.
Save wting/1da9178705429cb8d98c7db7c19f4fff to your computer and use it in GitHub Desktop.
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()
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
hypothesis
pytest
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment