diff --git a/.gitignore b/.gitignore index 4be6e16..4e904c1 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ -dist/* \ No newline at end of file +dist/* +.cache/* +.hypothesis/* \ No newline at end of file diff --git a/stl/hypothesis.py b/stl/hypothesis.py new file mode 100644 index 0000000..86c0cb0 --- /dev/null +++ b/stl/hypothesis.py @@ -0,0 +1,30 @@ +from hypothesis_cfg import ContextFreeGrammarStrategy + +from hypothesis.searchstrategy.strategies import SearchStrategy +from hypothesis.strategies import integers + +import stl + + +GRAMMAR = { + 'phi': (('Unary', '(', 'phi', ')'), + ('(', 'phi', ')', 'Binary', '(', 'phi', ')'), + ('AP',)), + 'Unary': (('~',), ('G',), ('F',), ('X',)), + 'Binary': ((' | ',), (' & ',), (' U ',)), +} + + +class SignalTemporalLogicStategy(SearchStrategy): + def __init__(self, max_length: int): + super(SearchStrategy, self).__init__() + self.cfg_gen = ContextFreeGrammarStrategy( + GRAMMAR, max_length=max_length, start='phi') + + def do_draw(self, data): + # TODO: randomly assign all intervals + # TODO: randomly decide between linear predicate or boolean predicates + # TODO: randomly generate boolean predicate + # TODO: randomly generate linear predicate + phi = stl.parse("".join(self.cfg_gen.do_draw(data))) + return phi diff --git a/stl/test_parser.py b/stl/test_parser.py index 92de3b8..dac702f 100644 --- a/stl/test_parser.py +++ b/stl/test_parser.py @@ -1,21 +1,13 @@ # -*- coding: utf-8 -*- import stl -from hypothesis import given, note -from hypothesis_cfg import ContextFreeGrammarStrategy +from hypothesis import given, event -GRAMMAR = { - 'phi': (('Unary', '(', 'phi', ')'), - ('(', 'phi', ')', 'Binary', '(', 'phi', ')'), - ('AP',)), - 'Unary': (('~',), ('G',), ('F',), ('X',)), - 'Binary': ((' | ',), (' & ',), (' U ',)), -} +from stl.hypothesis import SignalTemporalLogicStategy -@given(ContextFreeGrammarStrategy(GRAMMAR, length=15, start='phi')) -def test_invertable_repr(foo): - note(''.join(foo)) - phi = stl.parse(''.join(foo)) +@given(SignalTemporalLogicStategy(max_length=25)) +def test_invertable_repr(phi): + event(str(phi)) assert str(phi) == str(stl.parse(str(phi)))