diff --git a/stl/__init__.py b/stl/__init__.py index e9e248a..e0b5059 100644 --- a/stl/__init__.py +++ b/stl/__init__.py @@ -1,4 +1,4 @@ -from stl.utils import terms_lens, lineq_lens, walk, tree, and_or_lens +from stl.utils import terms_lens, lineq_lens, walk, and_or_lens from stl.utils import alw, env, andf, orf from stl.ast import dt_sym, t_sym from stl.ast import LinEq, Interval, NaryOpSTL, Or, And, F, G, ModalOp, Neg, Var, AtomicPred diff --git a/stl/test_parser.py b/stl/test_parser.py index 480e4d3..51208a5 100644 --- a/stl/test_parser.py +++ b/stl/test_parser.py @@ -5,17 +5,17 @@ import unittest from sympy import Symbol ex1 = ('x1 > 2', stl.LinEq( - (stl.Var(1, Symbol("x1"), stl.ast.t_sym),), + (stl.Var(1, Symbol("x1"), stl.t_sym),), ">", 2.0 )) ex1_ = ('x1 > a?', stl.LinEq( - (stl.Var(1, Symbol("x1"), stl.ast.t_sym),), + (stl.Var(1, Symbol("x1"), stl.t_sym),), ">", Symbol("a?") )) -ex1__ = ('x1', stl.AtomicPred('x1')) +ex1__ = ('x1', stl.AtomicPred('x1', stl.t_sym)) i1 = stl.Interval(0., 1.) i1_ = stl.Interval(0., Symbol("b?")) diff --git a/stl/test_utils.py b/stl/test_utils.py index f417d4c..a2c78fc 100644 --- a/stl/test_utils.py +++ b/stl/test_utils.py @@ -28,3 +28,31 @@ class TestSTLUtils(unittest.TestCase): self.assertEqual(set(map(str, stl.utils.param_lens(phi).get_all())), set()) self.assertEqual(phi, phi2) + + def test_walk(self): + raise NotImplementedError + + + def test_type_pred(self): + raise NotImplementedError + + + def test_ast_lens(self): + raise NotImplementedError + + + def test_terms_lens(self): + raise NotImplementedError + + + def test_f_neg_or_canonical_form(self): + raise NotImplementedError + + def test_to_from_mtl(self): + raise NotImplementedError + + def test_get_polarity(self): + raise NotImplementedError + + def test_canonical_polarity(self): + raise NotImplementedError diff --git a/stl/utils.py b/stl/utils.py index 19e7bf2..0209c0a 100644 --- a/stl/utils.py +++ b/stl/utils.py @@ -22,10 +22,6 @@ def walk(phi:STL, bfs:bool=False) -> STL_Generator: children.extend(node.children()) -def tree(phi:STL) -> Dict[STL, STL]: - return {x:set(x.children()) for x in walk(phi) if x.children()} - - def type_pred(*args:List[Type]) -> Mapping[Type, bool]: ast_types = set(args) return lambda x: type(x) in ast_types @@ -80,16 +76,6 @@ def param_lens(phi:STL) -> Lens: focus_lens=focus_lens).filter_(is_sym) -def symbol_lens(phi:STL) -> Lens: - is_sym = lambda x: isinstance(x, sympy.Symbol) - def focus_lens(leaf): - spacial = [lens().const] + lens().terms.each_().id.get_all() - temporal = [lens().interval[0], lens().interval[1]] - return spacial if isinstance(leaf, LinEq) else temp - - return ast_lens(phi, pred=type_pred(LinEq, F, G), - focus_lens=focus_lens).filter_(is_sym) - def set_params(stl_or_lens, val) -> STL: l = stl_or_lens if isinstance(stl_or_lens, Lens) else param_lens(stl_or_lens) return l.modify(lambda x: val.get(x, val.get(str(x), x))) @@ -131,6 +117,13 @@ def from_mtl(phi:MTL, ap_map:Dict[AtomicPred, LinEq]) -> STL: return focus.modify(ap_map.get) +def get_polarity(phi, traces=None): + raise NotImplementedError + +def canonical_polarity(phi, traces=None): + raise NotImplementedError + + # EDSL def alw(phi, *, lo, hi):