diff --git a/stl/ast.py b/stl/ast.py index 7054827..a85adfb 100644 --- a/stl/ast.py +++ b/stl/ast.py @@ -140,7 +140,7 @@ class Var(namedtuple("Var", ["coeff", "id"])): elif self.coeff == +1: coeff_str = "" else: - coeff_str = f"{self.coeff}*" + coeff_str = f"{self.coeff}" return f"{coeff_str}{self.id}" diff --git a/stl/boolean_eval.py b/stl/boolean_eval.py index 4d56522..6304206 100644 --- a/stl/boolean_eval.py +++ b/stl/boolean_eval.py @@ -13,7 +13,7 @@ oo = float('inf') def pointwise_sat(phi): - ap_names = [z.id.name for z in stl.ast.AP_lens(phi).Each().collect()] + ap_names = [z.id for z in phi.atomic_predicates] def _eval_stl(x, t): evaluated = stl.utils.eval_lineqs(phi, x) diff --git a/stl/hypothesis.py b/stl/hypothesis.py index 77b4cd8..9c3a78e 100644 --- a/stl/hypothesis.py +++ b/stl/hypothesis.py @@ -5,10 +5,12 @@ import stl GRAMMAR = { 'phi': (('Unary', '(', 'phi', ')'), ('(', 'phi', ')', 'Binary', '(', 'phi', - ')'), ('AP', )), - 'Unary': (('~', ), ('G', ), ('F', ), ('X', )), - 'Binary': ((' | ', ), (' & ', ), (' U ', )), + ')'), ('AP', ), ('LINEQ', )), + 'Unary': (('~', ), ('G', 'Interval'), ('F', 'Interval'), ('X', )), + 'Interval': (('',), ('[1, 3]',)), + 'Binary': ((' | ', ), (' & ', ), (' U ',)), 'AP': (('AP1', ), ('AP2', ), ('AP3', ), ('AP4', ), ('AP5', )), + 'LINEQ': (('x > 4', ), ('y < 2', ), ('y >= 3', ), ('x + y >= 2',)), } @@ -19,5 +21,5 @@ def to_stl(term): SignalTemporalLogicStrategy = st.builds(to_stl, ContextFreeGrammarStrategy( GRAMMAR, - max_length=25, + max_length=27, start='phi')) diff --git a/stl/parser.py b/stl/parser.py index 34f633e..7ad1c43 100644 --- a/stl/parser.py +++ b/stl/parser.py @@ -6,7 +6,7 @@ from functools import partialmethod -from lenses import lens +from lenses import bind from parsimonious import Grammar, NodeVisitor from stl import ast from stl.utils import alw, env, iff, implies, xor @@ -77,10 +77,6 @@ class STLVisitor(NodeVisitor): _, _, (left, ), _, _, _, (right, ), _, _ = children left = left if left != [] else float("inf") right = right if right != [] else float("inf") - if isinstance(left, int): - left = float(left) - if isinstance(right, int): - left = float(right) return ast.Interval(left, right) def get_text(self, node, _): @@ -136,7 +132,7 @@ class STLVisitor(NodeVisitor): def visit_terms(self, _, children): if isinstance(children[0], list): term, _1, sgn, _2, terms = children[0] - terms = lens(terms)[0].coeff * sgn + terms = bind(terms)[0].coeff * sgn return [term] + terms else: return children diff --git a/stl/test_boolean_eval.py b/stl/test_boolean_eval.py index a77ff5c..7bb78f4 100644 --- a/stl/test_boolean_eval.py +++ b/stl/test_boolean_eval.py @@ -23,14 +23,13 @@ TODO: Automatically generate input time series. """ x = { - "A": traces.TimeSeries([(0, 1), (0.1, 1), (0.2, 4)]), - "B": traces.TimeSeries([(0, 2), (0.1, 4), (0.2, 2)]), - "C": traces.TimeSeries([(0, True), (0.1, True), (0.2, False)]), - 'D': traces.TimeSeries({ - 0.0: 2, - 13.8: 3, - 19.7: 2 - }), + "x": traces.TimeSeries([(0, 1), (0.1, 1), (0.2, 4)]), + "y": traces.TimeSeries([(0, 2), (0.1, 4), (0.2, 2)]), + "AP1": traces.TimeSeries([(0, True), (0.1, True), (0.2, False)]), + "AP2": traces.TimeSeries([(0, False), (0.2, True), (0.5, False)]), + "AP3": traces.TimeSeries([(0, True), (0.1, True), (0.3, False)]), + "AP4": traces.TimeSeries([(0, False), (0.1, False), (0.3, False)]), + "AP5": traces.TimeSeries([(0, False), (0.1, False), (0.1, True)]), }