diff --git a/stl/__init__.py b/stl/__init__.py index 063bb16..a3574eb 100644 --- a/stl/__init__.py +++ b/stl/__init__.py @@ -5,4 +5,3 @@ from stl.parser import parse from stl.synth import lex_param_project from stl.boolean_eval import pointwise_sat from stl.fastboolean_eval import pointwise_satf -from stl.smooth_robustness import smooth_robustness diff --git a/stl/smooth_robustness.py b/stl/smooth_robustness.py index 25ef934..f618398 100644 --- a/stl/smooth_robustness.py +++ b/stl/smooth_robustness.py @@ -42,11 +42,13 @@ def admissible_params(phi, eps, L): def symbolic_params(phi, eps, L): + L = sym.Dummy("L") + eps = sym.Dummy("eps") return Param( - L=sym.Dummy("L"), - h=sym.Dummy("h"), + L=L, + h=sample_rate(eps, L), B=sym.Dummy("B"), - eps=sym.Dummy("eps"), + eps=eps, ) def smooth_robustness(phi, *, L=None, eps=None): diff --git a/stl/utils.py b/stl/utils.py index e14eeea..d4e3b6b 100644 --- a/stl/utils.py +++ b/stl/utils.py @@ -4,7 +4,7 @@ from lenses import lens, Lens import funcy as fn import sympy -from stl.ast import LinEq, And, Or, NaryOpSTL, F, G, Interval +from stl.ast import LinEq, And, Or, NaryOpSTL, F, G, Interval, Neg def walk(stl, bfs=False): """Walks Ast. Defaults to DFS unless BFS flag is set.""" @@ -88,23 +88,23 @@ def set_params(stl_or_lens, val): def f_neg_or_canonical_form(phi): - if isinstance(phi, stl.LinEq): + if isinstance(phi, LinEq): return phi children = [f_neg_or_canonical_form(s) for s in phi.children()] - if isinstance(phi, (stl.And, stl.G)): - children = [stl.ast.Neg(s) for s in children] + if isinstance(phi, (And, G)): + children = [Neg(s) for s in children] children = tuple(children) - if isinstance(phi, stl.Or): - return stl.Or(children) - elif isinstance(phi, stl.And): - return stl.Neg(stl.Or(children)) - elif isinstance(phi, stl.Neg): - return stl.Neg(children[0]) - elif isinstance(phi, stl.F): - return stl.F(phi.interval, children[0]) - elif isinstance(phi, stl.G): - return stl.Neg(stl.F(phi.interval, children[0])) + if isinstance(phi, Or): + return Or(children) + elif isinstance(phi, And): + return Neg(Or(children)) + elif isinstance(phi, Neg): + return Neg(children[0]) + elif isinstance(phi, F): + return F(phi.interval, children[0]) + elif isinstance(phi, G): + return Neg(F(phi.interval, children[0])) else: raise NotImplementedError