Last active
July 29, 2019 00:07
-
-
Save sureshvv/0fb78ef221fb8c1ed85dd034c83abefa to your computer and use it in GitHub Desktop.
diehard.py
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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