Skip to content

Instantly share code, notes, and snippets.

@sureshvv
Last active July 29, 2019 00:07
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save sureshvv/0fb78ef221fb8c1ed85dd034c83abefa to your computer and use it in GitHub Desktop.
Save sureshvv/0fb78ef221fb8c1ed85dd034c83abefa to your computer and use it in GitHub Desktop.
diehard.py
from hypothesis import note, settings
from hypothesis.stateful import RuleBasedStateMachine, rule, invariant, precondition
from hypothesis import strategies as st
class Person():
def __init__(self, time_taken):
self.crossed = False
self.time_taken = time_taken
class BoatProblem(RuleBasedStateMachine):
solutions = {}
def __init__(self):
super().__init__()
self.start()
def start(self):
self.persons = []
self.persons.append(Person(1))
self.persons.append(Person(2))
self.persons.append(Person(5))
self.persons.append(Person(10))
self.flash_light = Person(0)
self.total_time = 0
self.moves = []
@precondition(lambda self: self.flash_light.crossed)
@rule()
def make_return_move(self):
persons = [x for x in self.persons if x.crossed]
persons.sort(key=lambda x: x.time_taken)
self.moves.append([persons[0]])
persons[0].crossed = False
self.flash_light.crossed = False
self.total_time += persons[0].time_taken
@precondition(lambda self: not self.flash_light.crossed)
@rule(choice=st.choices())
def make_forward_move(self, choice):
persons = [x for x in self.persons if not x.crossed]
pers1 = choice(persons)
persons.remove(pers1)
pers2 = choice(persons)
sample = [pers1, pers2]
self.moves.append(sample)
for x in sample:
x.crossed = True
self.flash_light.crossed = True
self.total_time += max(sample[0].time_taken, sample[1].time_taken)
@invariant()
def problem_solved(self):
persons = [x for x in self.persons if x.crossed]
if len(persons) == 4 and self.flash_light.crossed:
if self.total_time not in self.solutions:
self.solutions[self.total_time] = self.moves
self.write_notes()
# 5 is by trial and error. Seems like the max number of solutions is 6
if len(self.solutions) > 5:
assert False
self.start()
def write_notes(self):
timings = [x for x in self.solutions]
note("timings: %s" % timings)
min_timing = min(timings)
for y in self.solutions[min_timing]:
note("%s" % [z.time_taken for z in y])
note("min timing: %s" % min_timing)
# The default of 200 is sometimes not enough for Hypothesis to find
# a falsifying example.
with settings(max_examples=700):
DieHardTest = BoatProblem.TestCase
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment