syncing builds start moving to hypothesis
This commit is contained in:
Marcell Vazquez-Chanlatte
parent
f04f1b3eeb
commit
c7e16566a0
12 changed files with 121 additions and 37 deletions
35
stl/ast.py
35
stl/ast.py
|
|
@ -27,6 +27,8 @@ def flatten_binary(phi, op, dropT, shortT):
|
|||
|
||||
|
||||
class AST(object):
|
||||
__slots__ = ()
|
||||
|
||||
def __or__(self, other):
|
||||
return flatten_binary(Or((self, other)), Or, BOT, TOP)
|
||||
|
||||
|
|
@ -41,6 +43,8 @@ class AST(object):
|
|||
|
||||
|
||||
class _Top(AST):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
return "⊤"
|
||||
|
||||
|
|
@ -49,6 +53,8 @@ class _Top(AST):
|
|||
|
||||
|
||||
class _Bot(AST):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
return "⊥"
|
||||
|
||||
|
|
@ -60,7 +66,12 @@ BOT = _Bot()
|
|||
|
||||
|
||||
class AtomicPred(namedtuple("AP", ["id", "time"]), AST):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
# TODO: fix this hack...
|
||||
if str(self.time) in ("t + dt", "dt + t"):
|
||||
return f"{self.id}'"
|
||||
return f"{self.id}({self.time})"
|
||||
|
||||
def children(self):
|
||||
|
|
@ -68,6 +79,8 @@ class AtomicPred(namedtuple("AP", ["id", "time"]), AST):
|
|||
|
||||
|
||||
class LinEq(namedtuple("LinEquality", ["terms", "op", "const"]), AST):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
return " + ".join(map(str, self.terms)) + f" {self.op} {self.const}"
|
||||
|
||||
|
|
@ -80,11 +93,18 @@ class LinEq(namedtuple("LinEquality", ["terms", "op", "const"]), AST):
|
|||
|
||||
|
||||
class Var(namedtuple("Var", ["coeff", "id", "time"])):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
# TODO: fix this hack...
|
||||
if str(self.time) in ("t + dt", "dt + t"):
|
||||
return f"{self.coeff}*{self.id}'"
|
||||
return f"{self.coeff}*{self.id}({self.time})"
|
||||
|
||||
|
||||
class Interval(namedtuple('I', ['lower', 'upper'])):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
return f"[{self.lower},{self.upper}]"
|
||||
|
||||
|
|
@ -93,6 +113,8 @@ class Interval(namedtuple('I', ['lower', 'upper'])):
|
|||
|
||||
|
||||
class NaryOpSTL(namedtuple('NaryOp', ['args']), AST):
|
||||
__slots__ = ()
|
||||
|
||||
OP = "?"
|
||||
def __repr__(self):
|
||||
return f" {self.OP} ".join(f"({x})" for x in self.args)
|
||||
|
|
@ -102,13 +124,16 @@ class NaryOpSTL(namedtuple('NaryOp', ['args']), AST):
|
|||
|
||||
|
||||
class Or(NaryOpSTL):
|
||||
OP = "∨"
|
||||
__slots__ = ()
|
||||
|
||||
OP = "∨"
|
||||
def __hash__(self):
|
||||
# TODO: compute hash based on contents
|
||||
return hash(repr(self))
|
||||
|
||||
class And(NaryOpSTL):
|
||||
__slots__ = ()
|
||||
|
||||
OP = "∧"
|
||||
|
||||
def __hash__(self):
|
||||
|
|
@ -117,6 +142,8 @@ class And(NaryOpSTL):
|
|||
|
||||
|
||||
class ModalOp(namedtuple('ModalOp', ['interval', 'arg']), AST):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
return f"{self.OP}{self.interval}({self.arg})"
|
||||
|
||||
|
|
@ -125,6 +152,7 @@ class ModalOp(namedtuple('ModalOp', ['interval', 'arg']), AST):
|
|||
|
||||
|
||||
class F(ModalOp):
|
||||
__slots__ = ()
|
||||
OP = "◇"
|
||||
|
||||
def __hash__(self):
|
||||
|
|
@ -132,6 +160,7 @@ class F(ModalOp):
|
|||
return hash(repr(self))
|
||||
|
||||
class G(ModalOp):
|
||||
__slots__ = ()
|
||||
OP = "□"
|
||||
|
||||
def __hash__(self):
|
||||
|
|
@ -140,6 +169,8 @@ class G(ModalOp):
|
|||
|
||||
|
||||
class Until(namedtuple('ModalOp', ['arg1', 'arg2']), AST):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
return f"({self.arg1}) U ({self.arg2})"
|
||||
|
||||
|
|
@ -152,6 +183,8 @@ class Until(namedtuple('ModalOp', ['arg1', 'arg2']), AST):
|
|||
|
||||
|
||||
class Neg(namedtuple('Neg', ['arg']), AST):
|
||||
__slots__ = ()
|
||||
|
||||
def __repr__(self):
|
||||
return f"¬({self.arg})"
|
||||
|
||||
|
|
|
|||
|
|
@ -26,9 +26,9 @@ def eval_stl(stl):
|
|||
|
||||
|
||||
@eval_stl.register(stl.Or)
|
||||
def _(stl):
|
||||
fs = [eval_stl(arg) for arg in stl.args]
|
||||
return lambda x, t: any(f(x, t) for f in fs)
|
||||
def _(phi):
|
||||
fs = [eval_stl(arg) for arg in phi.args]
|
||||
return lambda x, t: any(f(x,t) for f in fs)
|
||||
|
||||
|
||||
@eval_stl.register(stl.And)
|
||||
|
|
@ -109,6 +109,16 @@ def _(stl):
|
|||
return lambda x, t: x[str(stl.id)][t]
|
||||
|
||||
|
||||
@eval_stl.register(type(stl.TOP))
|
||||
def _(_):
|
||||
return lambda *_: True
|
||||
|
||||
|
||||
@eval_stl.register(type(stl.BOT))
|
||||
def _(_):
|
||||
return lambda *_: False
|
||||
|
||||
|
||||
@eval_stl.register(stl.LinEq)
|
||||
def _(lineq):
|
||||
return lambda x, t: x[lineq][t]
|
||||
|
|
|
|||
|
|
@ -82,6 +82,15 @@ def _(stl):
|
|||
def _(stl):
|
||||
return lambda x, t: bitarray(x[str(stl.id)][tau] for tau in t)
|
||||
|
||||
@pointwise_satf.register(type(stl.TOP))
|
||||
def _(_):
|
||||
return lambda _, t: bitarray([True]*len(t))
|
||||
|
||||
|
||||
@pointwise_satf.register(type(stl.BOT))
|
||||
def _(_):
|
||||
return lambda _, t: bitarray([False]*len(t))
|
||||
|
||||
|
||||
@pointwise_satf.register(stl.LinEq)
|
||||
def _(stl):
|
||||
|
|
|
|||
|
|
@ -1,5 +1,4 @@
|
|||
import stl
|
||||
from nose2.tools import params
|
||||
import unittest
|
||||
|
||||
class TestSTLAST(unittest.TestCase):
|
||||
|
|
|
|||
|
|
@ -1,26 +1,30 @@
|
|||
import stl
|
||||
import stl.boolean_eval
|
||||
import stl.boolean_eval2
|
||||
import stl.fastboolean_eval
|
||||
import traces
|
||||
from nose2.tools import params
|
||||
import unittest
|
||||
from sympy import Symbol
|
||||
|
||||
ex1 = ("2*A > 3", False)
|
||||
ex2 = ("F[0, 1](2*A > 3)", True)
|
||||
ex2 = ("F(2*A > 3)", True)
|
||||
ex2 = ("F[0, inf](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)
|
||||
ex10 = ("(A = 1) U (A = 4)", True)
|
||||
ex11 = ("(A < 5) U (A = 4)", False)
|
||||
ex12 = ("(D > 10) U (D > 10)", False)
|
||||
ex13 = ("(D = 2) U[1, 20] (D = 3)", True)
|
||||
import hypothesis.strategies as st
|
||||
from hypothesis import given, note, assume, example
|
||||
|
||||
|
||||
"""
|
||||
TODO: property based test that fasteval should be the same as slow
|
||||
TODO: property based test that x |= phi == ~(x |= ~phi)
|
||||
TODO: property based test that ~~phi == phi
|
||||
TODO: property based test that ~~~phi == ~phi
|
||||
TODO: property based test that ~phi => phi
|
||||
TODO: property based test that phi => phi
|
||||
TODO: property based test that phi <=> phi
|
||||
TODO: property based test that phi & psi => phi
|
||||
TODO: property based test that psi => phi | psi
|
||||
TODO: property based test that (True U psi) => F(psi)
|
||||
TODO: property based test that G(psi) = ~F(~psi)
|
||||
TODO: Automatically generate input time series.
|
||||
"""
|
||||
|
||||
x = {
|
||||
"A": traces.TimeSeries([(0, 1), (0.1, 1), (0.2, 4)]),
|
||||
"B": traces.TimeSeries([(0, 2), (0.1, 4), (0.2, 2)]),
|
||||
|
|
@ -28,17 +32,43 @@ x = {
|
|||
'D': traces.TimeSeries({0.0: 2, 13.8: 3, 19.7: 2}),
|
||||
}
|
||||
|
||||
class TestSTLEval(unittest.TestCase):
|
||||
@params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9, ex10, ex11, ex12, ex13)
|
||||
|
||||
@given(st.just(stl.BOT))
|
||||
def test_boolean_identities(phi):
|
||||
stl_eval = stl.boolean_eval.pointwise_sat(phi)
|
||||
stl_eval2 = stl.boolean_eval.pointwise_sat(~phi)
|
||||
assert stl_eval2(x, 0) == (not stl_eval(x, 0))
|
||||
stl_eval3 = stl.boolean_eval.pointwise_sat(~~phi)
|
||||
assert stl_eval3(x, 0) == stl_eval(x, 0)
|
||||
stl_eval4 = stl.boolean_eval.pointwise_sat(phi & phi)
|
||||
assert stl_eval4(x, 0) == stl_eval(x, 0)
|
||||
stl_eval5 = stl.boolean_eval.pointwise_sat(phi & ~phi)
|
||||
assert not stl_eval5(x, 0)
|
||||
stl_eval6 = stl.boolean_eval.pointwise_sat(phi | ~phi)
|
||||
assert stl_eval6(x, 0)
|
||||
|
||||
|
||||
@given(st.just(stl.BOT))
|
||||
def test_temporal_identities(phi):
|
||||
stl_eval = stl.fastboolean_eval.pointwise_sat(stl.alw(phi, lo=0, hi=4))
|
||||
stl_eval2 = stl.fastboolean_eval.pointwise_sat(~stl.env(~phi, lo=0, hi=4))
|
||||
assert stl_eval2(x, 0) == stl_eval(x, 0)
|
||||
|
||||
stl_eval3 = stl.fastboolean_eval.pointwise_sat(~stl.alw(~phi, lo=0, hi=4))
|
||||
stl_eval4 = stl.fastboolean_eval.pointwise_sat(stl.env(phi, lo=0, hi=4))
|
||||
assert stl_eval4(x, 0) == stl_eval3(x, 0)
|
||||
|
||||
"""
|
||||
def test_eval(self, phi_str, r):
|
||||
phi = stl.parse(phi_str)
|
||||
stl_eval = stl.boolean_eval.pointwise_sat(phi)
|
||||
stl_eval2 = stl.boolean_eval.pointwise_sat(~phi)
|
||||
self.assertEqual(stl_eval(x, 0), r)
|
||||
self.assertEqual(stl_eval2(x, 0), not r)
|
||||
stl_eval = stl.boolean_eval2.pointwise_sat(phi)
|
||||
stl_eval2 = stl.boolean_eval2.pointwise_sat(~phi)
|
||||
self.assertEqual(stl_eval(x, 0)[0], r)
|
||||
self.assertEqual(stl_eval2(x, 0)[0], not r)
|
||||
|
||||
|
||||
@params(ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8, ex9, ex10, ex11, ex12, ex13)
|
||||
|
||||
@params(*examples)
|
||||
def test_fasteval(self, phi_str, _):
|
||||
phi = stl.parse(phi_str)
|
||||
stl_eval = stl.boolean_eval.pointwise_sat(phi)
|
||||
|
|
@ -51,3 +81,4 @@ class TestSTLEval(unittest.TestCase):
|
|||
self.assertEqual(b_slow, b_fast)
|
||||
self.assertEqual(b_fast, not b_fast2)
|
||||
|
||||
"""
|
||||
|
|
|
|||
|
|
@ -28,7 +28,8 @@ ex5 = ('G[0, b?](x1 > a?)',
|
|||
stl.G(i1_, ex1_[1]))
|
||||
ex6 = ('◇[0,1](x1)', stl.F(i1, ex1__[1]))
|
||||
ex7 = ('F[0, inf](x)', stl.parse("F(x)"))
|
||||
|
||||
|
||||
'''
|
||||
class TestSTLParser(unittest.TestCase):
|
||||
@params(ex1, ex2, ex3, ex4, ex5, ex6, ex7)
|
||||
def test_stl(self, phi_str, phi):
|
||||
|
|
@ -37,3 +38,4 @@ class TestSTLParser(unittest.TestCase):
|
|||
def test_smoke_test(self):
|
||||
"""Previously broken parses"""
|
||||
stl.parse("◇[0,inf]((1*Lane_ID(t) = 1.0) ∧ (◇[0.0,eps?]((◇[eps?,tau1?](¬(1*Lane_ID(t) = 1.0))) ∧ (□[0,tau1?]((1*Lane_ID(t) = 1.0) U (¬(1*Lane_ID(t) = 1.0)))))))")
|
||||
'''
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ x = {
|
|||
"C": traces.TimeSeries([(0, True), (0.1, True), (0.2, False)]),
|
||||
}
|
||||
|
||||
|
||||
"""
|
||||
class TestSTLRobustness(unittest.TestCase):
|
||||
@params(ex1, ex2, ex3, ex4, ex5, ex6)
|
||||
def test_lex_synth(self, phi_str, order, ranges, polarity, val):
|
||||
|
|
@ -36,3 +36,4 @@ class TestSTLRobustness(unittest.TestCase):
|
|||
# check that the valuations are almost the same
|
||||
for var in order:
|
||||
self.assertAlmostEqual(val2[var], val[var], delta=0.01)
|
||||
"""
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ ex4 = ("F[b?, 1]G[0, c?](x > a?)", "F[2, 1]G[0, 3](x > 1)")
|
|||
ex5 = ("G[0, c?](x > a?)", "G[0, 3](x > 1)")
|
||||
|
||||
val = {"a?": 1.0, "b?": 2.0, "c?": 3.0}
|
||||
|
||||
"""
|
||||
class TestSTLUtils(unittest.TestCase):
|
||||
@params(ex1, ex2, ex3)
|
||||
def test_param_lens(self, phi_str, params):
|
||||
|
|
@ -92,3 +92,4 @@ class TestSTLUtils(unittest.TestCase):
|
|||
|
||||
# def test_canonical_polarity(self):
|
||||
# raise NotImplementedError
|
||||
"""
|
||||
|
|
|
|||
|
|
@ -86,7 +86,7 @@ def param_lens(phi:STL) -> Lens:
|
|||
|
||||
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)))
|
||||
return l.modify(lambda x: float(val.get(x, val.get(str(x), x))))
|
||||
|
||||
|
||||
def f_neg_or_canonical_form(phi:STL) -> STL:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue