From 92ff8c1526cf1ef3944da79c568f4317beb7a294 Mon Sep 17 00:00:00 2001 From: Shromona MacBook Date: Thu, 1 Dec 2016 18:29:50 -0800 Subject: [PATCH 1/4] Fast boolean evaluation --- stl/fastboolean_eval.py | 117 ++++++++++++++++++++++++++++++++++++++++ test_boolean.py | 26 +++++++++ 2 files changed, 143 insertions(+) create mode 100644 stl/fastboolean_eval.py create mode 100644 test_boolean.py diff --git a/stl/fastboolean_eval.py b/stl/fastboolean_eval.py new file mode 100644 index 0000000..a22b5ba --- /dev/null +++ b/stl/fastboolean_eval.py @@ -0,0 +1,117 @@ +# TODO: figure out how to deduplicate this with robustness +# - Abstract as working on distributive lattice + +from functools import singledispatch +import operator as op + +import numpy as np +import sympy as smp +from lenses import lens +import gmpy2 as gp + +import stl.ast + +@singledispatch +def pointwise_sat(stl): + raise NotImplementedError + + +@pointwise_sat.register(stl.Or) +def _(stl): + def sat_comp(x,t): + val = 0 + for arg in stl.args: + val = pointwise_sat(arg)(x, t) | val + return val + return sat_comp + #return lambda x, t: any(pointwise_sat(arg)(x, t) for arg in stl.args) + + +@pointwise_sat.register(stl.And) +def _(stl): + def sat_comp(x,t): + val = 2**(len(t))-1 + for arg in stl.args: + val = pointwise_sat(arg)(x, t) & val + return val + return sat_comp + #return lambda x, t: all(pointwise_sat(arg)(x, t) for arg in stl.args) + + +@pointwise_sat.register(stl.F) +def _(stl): + lo, hi = stl.interval + def sat_comp(x,t): + val = 0 + for tau in t: + tau_t = [min(tau + t2, x.index[-1]) for t2 in x[lo:hi].index] + val = (val << 1) | (pointwise_sat(stl.arg)(x, tau_t) > 0) + return val + return sat_comp + #return lambda x, t, val: [pointwise_sat(stl.arg)(x, [min(deltat + t2, x.index[-1]) + # for t2 in x[lo:hi].index], 0) for deltat in t] + + +@pointwise_sat.register(stl.G) +def _(stl): + lo, hi = stl.interval + def sat_comp(x,t): + val = 0 + for tau in t: + tau_t = [min(tau + t2, x.index[-1]) for t2 in x[lo:hi].index] + val = (val << 1) | (gp.popcount(pointwise_sat(stl.arg)(x, tau_t)) == len(tau_t)) + return val + return sat_comp + #return lambda x, t: all((pointwise_sat(stl.arg)(x, min(t + t2, x.index[-1])) + # for t2 in x[lo:hi].index)) + + +@pointwise_sat.register(stl.Neg) +def _(stl): + def sat_comp(x,t): + val = pointwise_sat(arg)(x, t) ^ (2**(len(t))-1) + return val + return sat_comp + #return lambda x, t: pointwise_sat(arg)(x, t, val) + + +op_lookup = { + ">": op.gt, + ">=": op.ge, + "<": op.lt, + "<=": op.le, + "=": op.eq, +} + + +@pointwise_sat.register(stl.AtomicPred) +def _(stl): + def sat_comp(x, t): + val = 0 + for tau in t: + val = (val << 1) | (1 if x[stl.id][tau] else 0) + return val + return sat_comp + #return lambda x, t, val: [(val << 1) | (x[stl.id][deltat] == True) for deltat in t] + + +@pointwise_sat.register(stl.LinEq) +def _(stl): + op = op_lookup[stl.op] + def sat_comp(x, t): + val = 0 + for tau in t: + val = (val << 1) | (op(eval_terms(stl, x, tau), stl.const) == True) + return val + return sat_comp + #return lambda x, t, val: [(val << 1) |(op(eval_terms(stl, x, deltat), stl.const) == True) for deltat in t] + + +def eval_terms(lineq, x, t): + psi = lens(lineq).terms.each_().modify(eval_term(x, t)) + return sum(psi.terms) + + +def eval_term(x, t): + # TODO(lift interpolation much higher) + return lambda term: term.coeff*np.interp(t, x.index, x[term.id.name]) diff --git a/test_boolean.py b/test_boolean.py new file mode 100644 index 0000000..1106060 --- /dev/null +++ b/test_boolean.py @@ -0,0 +1,26 @@ +import stl +import stl.fastboolean_eval +import pandas as pd +from nose2.tools import params +import unittest +from sympy import Symbol + +ex1 = ("2*A > 3", False) +ex2 = ("F[0, 1](2*A > 3)", True) +ex3 = ("F[1, 0](2*A > 3)", False) +ex4 = ("G[1, 0](2*A > 3)", True) +ex5 = ("(A < 0)", False) +ex6 = ("G[0, 0.1](A < 0)", False) +ex7 = ("G[0, 0.1](C)", True) +ex8 = ("G[0, 0.2](C)", False) +ex9 = ("(F[0, 0.2](C)) and (F[0, 1](2*A > 3))", True) +x = pd.DataFrame([[1,2, True], [1,4, True], [4,2, False]], index=[0,0.1,0.2], + columns=["A", "B", "C"]) + +tests = [ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9] +for test in tests: + phi = stl.parse(test[0]) + print(phi) + stl_eval = stl.fastboolean_eval.pointwise_sat(phi) + print(stl_eval(x, [0])) + \ No newline at end of file From fb80b0c3ce0bacc5c5002e0fb961ddc2c500ade3 Mon Sep 17 00:00:00 2001 From: Shromona MacBook Date: Fri, 2 Dec 2016 14:27:04 -0800 Subject: [PATCH 2/4] Updated fast boolean --- stl/fastboolean_eval.py | 9 --------- 1 file changed, 9 deletions(-) diff --git a/stl/fastboolean_eval.py b/stl/fastboolean_eval.py index a22b5ba..6c8091e 100644 --- a/stl/fastboolean_eval.py +++ b/stl/fastboolean_eval.py @@ -24,7 +24,6 @@ def _(stl): val = pointwise_sat(arg)(x, t) | val return val return sat_comp - #return lambda x, t: any(pointwise_sat(arg)(x, t) for arg in stl.args) @pointwise_sat.register(stl.And) @@ -35,7 +34,6 @@ def _(stl): val = pointwise_sat(arg)(x, t) & val return val return sat_comp - #return lambda x, t: all(pointwise_sat(arg)(x, t) for arg in stl.args) @pointwise_sat.register(stl.F) @@ -48,8 +46,6 @@ def _(stl): val = (val << 1) | (pointwise_sat(stl.arg)(x, tau_t) > 0) return val return sat_comp - #return lambda x, t, val: [pointwise_sat(stl.arg)(x, [min(deltat + t2, x.index[-1]) - # for t2 in x[lo:hi].index], 0) for deltat in t] @pointwise_sat.register(stl.G) @@ -62,8 +58,6 @@ def _(stl): val = (val << 1) | (gp.popcount(pointwise_sat(stl.arg)(x, tau_t)) == len(tau_t)) return val return sat_comp - #return lambda x, t: all((pointwise_sat(stl.arg)(x, min(t + t2, x.index[-1])) - # for t2 in x[lo:hi].index)) @pointwise_sat.register(stl.Neg) @@ -72,7 +66,6 @@ def _(stl): val = pointwise_sat(arg)(x, t) ^ (2**(len(t))-1) return val return sat_comp - #return lambda x, t: pointwise_sat(arg)(x, t, val) op_lookup = { @@ -92,7 +85,6 @@ def _(stl): val = (val << 1) | (1 if x[stl.id][tau] else 0) return val return sat_comp - #return lambda x, t, val: [(val << 1) | (x[stl.id][deltat] == True) for deltat in t] @pointwise_sat.register(stl.LinEq) @@ -104,7 +96,6 @@ def _(stl): val = (val << 1) | (op(eval_terms(stl, x, tau), stl.const) == True) return val return sat_comp - #return lambda x, t, val: [(val << 1) |(op(eval_terms(stl, x, deltat), stl.const) == True) for deltat in t] def eval_terms(lineq, x, t): From d5f38e27ed196f6aa719bf7acc2c5e7c2dac549c Mon Sep 17 00:00:00 2001 From: Shromona MacBook Date: Sat, 3 Dec 2016 01:14:55 -0800 Subject: [PATCH 3/4] Fast boolean eval --- stl/fastboolean_eval.py | 46 +++++++++++++++++------------------- stl/test_fastboolean_eval.py | 25 ++++++++++++++++++++ 2 files changed, 47 insertions(+), 24 deletions(-) create mode 100644 stl/test_fastboolean_eval.py diff --git a/stl/fastboolean_eval.py b/stl/fastboolean_eval.py index 6c8091e..f6d69b4 100644 --- a/stl/fastboolean_eval.py +++ b/stl/fastboolean_eval.py @@ -8,6 +8,7 @@ import numpy as np import sympy as smp from lenses import lens import gmpy2 as gp +from bitarray import bitarray import stl.ast @@ -19,20 +20,21 @@ def pointwise_sat(stl): @pointwise_sat.register(stl.Or) def _(stl): def sat_comp(x,t): - val = 0 + sat = bitarray(len(t)) for arg in stl.args: - val = pointwise_sat(arg)(x, t) | val - return val + sat = pointwise_sat(arg)(x, t) | sat + return sat return sat_comp @pointwise_sat.register(stl.And) def _(stl): def sat_comp(x,t): - val = 2**(len(t))-1 + sat = bitarray(len(t)) + sat.setall('True') for arg in stl.args: - val = pointwise_sat(arg)(x, t) & val - return val + sat = pointwise_sat(arg)(x, t) & sat + return sat return sat_comp @@ -40,11 +42,11 @@ def _(stl): def _(stl): lo, hi = stl.interval def sat_comp(x,t): - val = 0 + sat = bitarray() for tau in t: tau_t = [min(tau + t2, x.index[-1]) for t2 in x[lo:hi].index] - val = (val << 1) | (pointwise_sat(stl.arg)(x, tau_t) > 0) - return val + sat.append((pointwise_sat(stl.arg)(x, tau_t)).count() > 0) + return sat return sat_comp @@ -52,20 +54,18 @@ def _(stl): def _(stl): lo, hi = stl.interval def sat_comp(x,t): - val = 0 + sat = bitarray() for tau in t: tau_t = [min(tau + t2, x.index[-1]) for t2 in x[lo:hi].index] - val = (val << 1) | (gp.popcount(pointwise_sat(stl.arg)(x, tau_t)) == len(tau_t)) - return val + point_sat = pointwise_sat(stl.arg)(x, tau_t) + sat.append(point_sat.count() == point_sat.length()) + return sat return sat_comp @pointwise_sat.register(stl.Neg) def _(stl): - def sat_comp(x,t): - val = pointwise_sat(arg)(x, t) ^ (2**(len(t))-1) - return val - return sat_comp + return lambda x,t: ~pointwise_sat(arg)(x, t) op_lookup = { @@ -80,10 +80,9 @@ op_lookup = { @pointwise_sat.register(stl.AtomicPred) def _(stl): def sat_comp(x, t): - val = 0 - for tau in t: - val = (val << 1) | (1 if x[stl.id][tau] else 0) - return val + sat = bitarray() + [sat.append(x[stl.id][tau]) for tau in t] + return sat return sat_comp @@ -91,10 +90,9 @@ def _(stl): def _(stl): op = op_lookup[stl.op] def sat_comp(x, t): - val = 0 - for tau in t: - val = (val << 1) | (op(eval_terms(stl, x, tau), stl.const) == True) - return val + sat = bitarray() + [sat.append(op(eval_terms(stl, x, tau), stl.const)) for tau in t] + return sat return sat_comp diff --git a/stl/test_fastboolean_eval.py b/stl/test_fastboolean_eval.py new file mode 100644 index 0000000..043d754 --- /dev/null +++ b/stl/test_fastboolean_eval.py @@ -0,0 +1,25 @@ +import stl +import stl.fastboolean_eval +import pandas as pd +from nose2.tools import params +import unittest +from sympy import Symbol + +ex1 = ("2*A > 3", False) +ex2 = ("F[0, 1](2*A > 3)", True) +ex3 = ("F[1, 0](2*A > 3)", False) +ex4 = ("G[1, 0](2*A > 3)", True) +ex5 = ("(A < 0)", False) +ex6 = ("G[0, 0.1](A < 0)", False) +ex7 = ("G[0, 0.1](C)", True) +ex8 = ("G[0, 0.2](C)", False) +ex9 = ("(F[0, 0.2](C)) and (F[0, 1](2*A > 3))", True) +x = pd.DataFrame([[1,2, True], [1,4, True], [4,2, False]], index=[0,0.1,0.2], + columns=["A", "B", "C"]) + +class TestSTLRobustness(unittest.TestCase): + @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9) + def test_stl(self, phi_str, r): + phi = stl.parse(phi_str) + stl_eval = stl.fastboolean_eval.pointwise_sat(phi) + self.assertEqual(stl_eval(x, [0]), r) From 8cae363e61ba76d7a0e2524edce6d3b1c4bb8acc Mon Sep 17 00:00:00 2001 From: Shromona MacBook Date: Sat, 3 Dec 2016 01:21:00 -0800 Subject: [PATCH 4/4] Fast boolean with eval --- stl/__init__.py | 1 + stl/fastboolean_eval.py | 26 +++++++++++++------------- stl/test_fastboolean_eval.py | 2 +- 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/stl/__init__.py b/stl/__init__.py index b4b073b..a3574eb 100644 --- a/stl/__init__.py +++ b/stl/__init__.py @@ -4,3 +4,4 @@ from stl.ast import LinEq, Interval, NaryOpSTL, Or, And, F, G, ModalOp, Neg, Var 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 diff --git a/stl/fastboolean_eval.py b/stl/fastboolean_eval.py index f6d69b4..3fb40c2 100644 --- a/stl/fastboolean_eval.py +++ b/stl/fastboolean_eval.py @@ -13,59 +13,59 @@ from bitarray import bitarray import stl.ast @singledispatch -def pointwise_sat(stl): +def pointwise_satf(stl): raise NotImplementedError -@pointwise_sat.register(stl.Or) +@pointwise_satf.register(stl.Or) def _(stl): def sat_comp(x,t): sat = bitarray(len(t)) for arg in stl.args: - sat = pointwise_sat(arg)(x, t) | sat + sat = pointwise_satf(arg)(x, t) | sat return sat return sat_comp -@pointwise_sat.register(stl.And) +@pointwise_satf.register(stl.And) def _(stl): def sat_comp(x,t): sat = bitarray(len(t)) sat.setall('True') for arg in stl.args: - sat = pointwise_sat(arg)(x, t) & sat + sat = pointwise_satf(arg)(x, t) & sat return sat return sat_comp -@pointwise_sat.register(stl.F) +@pointwise_satf.register(stl.F) def _(stl): lo, hi = stl.interval def sat_comp(x,t): sat = bitarray() for tau in t: tau_t = [min(tau + t2, x.index[-1]) for t2 in x[lo:hi].index] - sat.append((pointwise_sat(stl.arg)(x, tau_t)).count() > 0) + sat.append((pointwise_satf(stl.arg)(x, tau_t)).count() > 0) return sat return sat_comp -@pointwise_sat.register(stl.G) +@pointwise_satf.register(stl.G) def _(stl): lo, hi = stl.interval def sat_comp(x,t): sat = bitarray() for tau in t: tau_t = [min(tau + t2, x.index[-1]) for t2 in x[lo:hi].index] - point_sat = pointwise_sat(stl.arg)(x, tau_t) + point_sat = pointwise_satf(stl.arg)(x, tau_t) sat.append(point_sat.count() == point_sat.length()) return sat return sat_comp -@pointwise_sat.register(stl.Neg) +@pointwise_satf.register(stl.Neg) def _(stl): - return lambda x,t: ~pointwise_sat(arg)(x, t) + return lambda x,t: ~pointwise_satf(arg)(x, t) op_lookup = { @@ -77,7 +77,7 @@ op_lookup = { } -@pointwise_sat.register(stl.AtomicPred) +@pointwise_satf.register(stl.AtomicPred) def _(stl): def sat_comp(x, t): sat = bitarray() @@ -86,7 +86,7 @@ def _(stl): return sat_comp -@pointwise_sat.register(stl.LinEq) +@pointwise_satf.register(stl.LinEq) def _(stl): op = op_lookup[stl.op] def sat_comp(x, t): diff --git a/stl/test_fastboolean_eval.py b/stl/test_fastboolean_eval.py index 043d754..2d0467f 100644 --- a/stl/test_fastboolean_eval.py +++ b/stl/test_fastboolean_eval.py @@ -21,5 +21,5 @@ class TestSTLRobustness(unittest.TestCase): @params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9) def test_stl(self, phi_str, r): phi = stl.parse(phi_str) - stl_eval = stl.fastboolean_eval.pointwise_sat(phi) + stl_eval = stl.fastboolean_eval.pointwise_satf(phi) self.assertEqual(stl_eval(x, [0]), r)