From 399bf2f421a731694803ee861a35bee1056fb682 Mon Sep 17 00:00:00 2001 From: Marcell Vazquez-Chanlatte Date: Mon, 10 Oct 2016 00:19:07 -0700 Subject: [PATCH] switch to Boolean semantics for synth --- synth.py | 11 +++++------ test_robustness.py | 1 - 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/synth.py b/synth.py index 6bf54bd..1637009 100644 --- a/synth.py +++ b/synth.py @@ -1,23 +1,22 @@ import operator as op from stl.utils import set_params, param_lens -from stl.robustness import pointwise_robustness +from stl.boolean_eval import pointwise_sat from lenses import lens def binsearch(stleval, *, tol=1e-3, lo, hi, polarity): """Only run search if tightest robustness was positive.""" # Early termination via bounds checks - if polarity and stleval(lo) > 0: + if polarity and stleval(lo): return lo - elif not polarity and stleval(hi) > 0: + elif not polarity and stleval(hi): return hi - test = op.le if polarity else op.gt while hi - lo > tol: mid = lo + (hi - lo) / 2 r = stleval(mid) - lo, hi = (mid, hi) if test(r, 0) else (lo, mid) + lo, hi = (mid, hi) if r ^ polarity else (lo, mid) # Want satisifiable formula return hi if polarity else lo @@ -28,7 +27,7 @@ def lex_param_project(stl, x, *, order, polarity, ranges, tol=1e-3): p_lens = param_lens(stl) def stleval_fact(var, val): l = lens(val)[var] - return lambda p: pointwise_robustness(set_params(stl, l.set(p)))(x, 0) + return lambda p: pointwise_sat(set_params(stl, l.set(p)))(x, 0) for var in order: stleval = stleval_fact(var, val) diff --git a/test_robustness.py b/test_robustness.py index 4c5db60..467db95 100644 --- a/test_robustness.py +++ b/test_robustness.py @@ -17,7 +17,6 @@ x = pd.DataFrame([[1,2], [1,4], [4,2]], index=[0,0.1,0.2], columns=["A", "B"]) - class TestSTLRobustness(unittest.TestCase): @params(ex1, ex2, ex3, ex4, ex5, ex6) def test_stl(self, phi_str, r):