diff --git a/stl/hypothesis.py b/stl/hypothesis.py index 75b6d18..02b75eb 100644 --- a/stl/hypothesis.py +++ b/stl/hypothesis.py @@ -12,42 +12,12 @@ GRAMMAR = { ('AP',)), 'Unary': (('~',), ('G',), ('F',), ('X',)), 'Binary': ((' | ',), (' & ',), (' U ',)), + 'AP': (('AP1',), ('AP2',), ('AP3',), ('AP4',), ('AP5',)), } +def to_stl(term): + return stl.parse(''.join(term)) - -def build_lineq(params): - pass - - -LinEqStrategy = st.builds( - lambda x: stl.ast.LinEq(*x), - st.tuples( - st.lists( - st.tuples( - st.sampled_from(["x", "y", "z","w"]), - st.integers(min_value=-5, max_value=5)), - min_size=1, max_size=4, unique=True), - st.sampled_from([">=", "<=", "<", ">", "="]), - st.integers(min_value=-5, max_value=5) -)) - - -class SignalTemporalLogicStategy(SearchStrategy): - def __init__(self, max_length: int): - super().__init__() - self.cfg_gen = ContextFreeGrammarStrategy( - GRAMMAR, max_length=max_length, start='phi') - self.ap_gen = st.builds( - lambda i: stl.ast.AtomicPred(f"AP{i}"), - st.integers(min_value=0, max_value=max_length)) - - 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))) - ap_lens = stl.utils.AP_lens(phi).Each() - phi = ap_lens.modify(lambda _: self.ap_gen.do_draw(data)) - return phi +SignalTemporalLogicStrategy = st.builds( + to_stl, ContextFreeGrammarStrategy( + GRAMMAR, max_length=25, start='phi')) diff --git a/stl/test_parser.py b/stl/test_parser.py index dac702f..7d6c644 100644 --- a/stl/test_parser.py +++ b/stl/test_parser.py @@ -2,12 +2,10 @@ import stl from hypothesis import given, event -from stl.hypothesis import SignalTemporalLogicStategy +from stl.hypothesis import SignalTemporalLogicStrategy -@given(SignalTemporalLogicStategy(max_length=25)) +@given(SignalTemporalLogicStrategy) def test_invertable_repr(phi): event(str(phi)) assert str(phi) == str(stl.parse(str(phi))) - - diff --git a/stl/utils.py b/stl/utils.py index 52979a6..57a67b5 100644 --- a/stl/utils.py +++ b/stl/utils.py @@ -37,13 +37,15 @@ def type_pred(*args: List[Type]) -> Mapping[Type, bool]: return lambda x: type(x) in ast_types -def ast_lens(phi: STL, bind=True, *, pred=None, focus_lens=None) -> Lens: +def ast_lens(phi: STL, bind=True, *, pred=None, focus_lens=None, + getter=False) -> Lens: if focus_lens is None: focus_lens = lambda _: [lens] if pred is None: pred = lambda _: False l = lenses.bind(phi) if bind else lens - return l.Fork(*_ast_lens(phi, pred=pred, focus_lens=focus_lens)) + child_lenses = _ast_lens(phi, pred=pred, focus_lens=focus_lens) + return (l.Tuple if getter else l.Fork)(*child_lenses) def _ast_lens(phi: STL, pred, focus_lens) -> Lens: @@ -67,9 +69,9 @@ def _ast_lens(phi: STL, pred, focus_lens) -> Lens: yield from [l & cl for cl in _ast_lens(l.get()(phi), pred, focus_lens)] -lineq_lens = fn.partial(ast_lens, pred=type_pred(LinEq)) -AP_lens = fn.partial(ast_lens, pred=type_pred(stl.ast.AtomicPred)) -and_or_lens = fn.partial(ast_lens, pred=type_pred(And, Or)) +lineq_lens = fn.partial(ast_lens, pred=type_pred(LinEq), getter=True) +AP_lens = fn.partial(ast_lens, pred=type_pred(stl.ast.AtomicPred), getter=True) +and_or_lens = fn.partial(ast_lens, pred=type_pred(And, Or), getter=True) def terms_lens(phi: STL, bind: bool = True) -> Lens: