tstl_hypothesis.py

import sys
from hypothesis import given, strategies as st, settings, Verbosity, HealthCheck
from hypothesis.searchstrategy.featureflags import FeatureStrategy
import traceback


if __name__ == '__main__':
    target = sys.argv[1]
    with open(target) as i:
        source = i.read()

    exec_globals = {}

    exec(source, exec_globals)

    sut_class = exec_globals["sut"]

    @settings(verbosity=Verbosity.debug, deadline=None, suppress_health_check=HealthCheck.all())
    @given(st.data())
    def test(data):
        n_steps = data.draw(st.integers(1, 100))
        sut = sut_class()

        features = data.draw(FeatureStrategy())

        actions = {t[0]: t for t in sut.actions()}
        action_names = sorted(actions, key=lambda s: (len(s), s))

        for _ in range(n_steps):
            name, guard, act = actions[data.draw(st.sampled_from(action_names).filter(lambda t: actions[t][1]() and features.is_enabled(t)))]
            act()

    test()