# Original code by Mark Seaborn <http://lackingrhoticity.blogspot.com>
# Slight modifications by Kay Schluehr


class ModelCheckEscape(Exception):
    pass

class ChooserException(Exception):
    pass

class Chooser(object):
    def __init__(self, chosen, stack):
        self._chosen = chosen
        self._stack  = stack
        self._it     = iter(chosen)

    def choose(self, choices):
        try:
            choice = self._it.next()
            if choice not in choices:
                raise ChooserException("Program is not deterministic")
            return choice
        except StopIteration:
            self._stack+=[self._chosen + [choice] for choice in choices]
            raise ModelCheckEscape()

def check(func, chooser = Chooser):
    stack = [[]]
    while len(stack) > 0:
        chosen = stack.pop()
        print chosen
        try:
            func(chooser(chosen, stack))
        except ModelCheckEscape:
            pass