teaching/mtl-aas
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

deduplicate fastboolean_eval from boolean_eval + packaging

Browse source
This commit is contained in:
Marcell Vazquez-Chanlatte 2016-12-03 12:56:33 -08:00
parent c41231e964
commit 5756362b3c
6 changed files with 13 additions and 82 deletions
Download patch file Download diff file Expand all files Collapse all files

1
setup.py
View file

@ -12,6 +12,7 @@ setup(name='py-stl',
'parsimonious',
'lenses',
'sympy',
'bitarray',
],
extras_require = {
'robustness': ['numpy', 'pandas']

1
stl/boolean_eval.py
View file

@ -5,7 +5,6 @@ from functools import singledispatch
import operator as op
import numpy as np
import sympy as smp
from lenses import lens
import stl.ast

29
stl/fastboolean_eval.py
View file

@ -1,16 +1,8 @@
# 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
from bitarray import bitarray
import stl.ast
from stl.boolean_eval import eval_terms, op_lookup
@singledispatch
def pointwise_satf(stl):
@ -68,15 +60,6 @@ def _(stl):
return lambda x,t: ~pointwise_satf(arg)(x, t)
op_lookup = {
">": op.gt,
">=": op.ge,
"<": op.lt,
"<=": op.le,
"=": op.eq,
}
@pointwise_satf.register(stl.AtomicPred)
def _(stl):
def sat_comp(x, t):
@ -94,13 +77,3 @@ def _(stl):
[sat.append(op(eval_terms(stl, x, tau), stl.const)) for tau in t]
return sat
return sat_comp
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])

13
stl/test_boolean_eval.py
View file

@ -1,5 +1,6 @@
import stl
import stl.boolean_eval
import stl.fastboolean_eval
import pandas as pd
from nose2.tools import params
import unittest
@ -17,9 +18,17 @@ 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):
class TestSTLEval(unittest.TestCase):
@params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9)
def test_stl(self, phi_str, r):
def test_eval(self, phi_str, r):
phi = stl.parse(phi_str)
stl_eval = stl.boolean_eval.pointwise_sat(phi)
self.assertEqual(stl_eval(x, 0), r)
@params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9)
def test_fasteval(self, phi_str, _):
phi = stl.parse(phi_str)
stl_eval = stl.boolean_eval.pointwise_sat(phi)
stl_evalf = stl.fastboolean_eval.pointwise_satf(phi)
self.assertEqual(bool(int(stl_evalf(x, [0]).to01())), stl_eval(x, 0))

25
stl/test_fastboolean_eval.py
View file

@ -1,25 +0,0 @@
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_satf(phi)
self.assertEqual(stl_eval(x, [0]), r)

26
test_boolean.py
View file

@ -1,26 +0,0 @@
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]))