implemented boolean evaluator + increasing converage
This commit is contained in:
Marcell Vazquez-Chanlatte
parent
f53cab4485
commit
77a904d050
4 changed files with 123 additions and 53 deletions
|
|
@ -11,13 +11,14 @@ import stl
|
|||
import stl.ast
|
||||
from stl.utils import const_trace, andf, orf
|
||||
|
||||
|
||||
TRUE_TRACE = const_trace(True)
|
||||
FALSE_TRACE = const_trace(False)
|
||||
|
||||
|
||||
def negate_trace(x):
|
||||
return x.operation(TRUE_TRACE, op.xor)
|
||||
out = x.operation(TRUE_TRACE, op.xor)
|
||||
out.domain = x.domain
|
||||
return out
|
||||
|
||||
|
||||
def pointwise_sat(phi, dt=0.1):
|
||||
|
|
@ -37,33 +38,63 @@ def eval_stl(phi, dt):
|
|||
raise NotImplementedError
|
||||
|
||||
|
||||
def or_traces(xs):
|
||||
out = orf(*xs)
|
||||
out.domain = xs[0].domain
|
||||
return out
|
||||
|
||||
|
||||
@eval_stl.register(stl.Or)
|
||||
def eval_stl_or(phi, dt):
|
||||
fs = [eval_stl(arg, dt) for arg in phi.args]
|
||||
|
||||
def _eval(x):
|
||||
out = orf(*(f(x) for f in fs))
|
||||
out = or_traces([f(x) for f in fs])
|
||||
out.compact()
|
||||
return out
|
||||
|
||||
return _eval
|
||||
|
||||
|
||||
def and_traces(xs):
|
||||
out = andf(*xs)
|
||||
out.domain = xs[0].domain
|
||||
return out
|
||||
|
||||
|
||||
@eval_stl.register(stl.And)
|
||||
def eval_stl_and(phi, dt):
|
||||
fs = [eval_stl(arg, dt) for arg in phi.args]
|
||||
|
||||
def _eval(x):
|
||||
out = andf(*(f(x) for f in fs))
|
||||
out = and_traces([f(x) for f in fs])
|
||||
out.compact()
|
||||
return out
|
||||
|
||||
return _eval
|
||||
|
||||
|
||||
def apply_until(y):
|
||||
periods = list(y.iterperiods())
|
||||
phi2_next = False
|
||||
for t, _, (phi1, phi2) in periods[::-1]:
|
||||
yield (t, phi2 or (phi1 and phi2_next))
|
||||
phi2_next = phi2
|
||||
|
||||
|
||||
@eval_stl.register(stl.Until)
|
||||
def eval_stl_until(phi, dt):
|
||||
raise NotImplementedError
|
||||
f1, f2 = eval_stl(phi.arg1, dt), eval_stl(phi.arg2, dt)
|
||||
|
||||
def _eval(x):
|
||||
y1, y2 = f1(x), f2(x)
|
||||
y = y1.operation(y2, lambda a, b: (a, b))
|
||||
out = traces.TimeSeries(apply_until(y), domain=y1.domain)
|
||||
out.compact()
|
||||
|
||||
return out
|
||||
|
||||
return _eval
|
||||
|
||||
|
||||
@eval_stl.register(stl.F)
|
||||
|
|
@ -79,11 +110,13 @@ def eval_stl_g(phi, dt):
|
|||
|
||||
def process_intervals(x):
|
||||
# Need to add last interval
|
||||
intervals = fn.chain(x.iterintervals(),
|
||||
[(x.last(), (float('inf'), None),)])
|
||||
intervals = fn.chain(x.iterintervals(), [(
|
||||
x.last(),
|
||||
(float('inf'), None),
|
||||
)])
|
||||
for (start, val), (end, val2) in intervals:
|
||||
start2, end2 = start - b, end + a
|
||||
if end2 > start2:
|
||||
if end2 > start2 and start2:
|
||||
yield (start2, val)
|
||||
|
||||
def _eval(x):
|
||||
|
|
@ -91,7 +124,8 @@ def eval_stl_g(phi, dt):
|
|||
if len(y) <= 1:
|
||||
return y
|
||||
|
||||
out = traces.TimeSeries(process_intervals(y))
|
||||
out = traces.TimeSeries(process_intervals(y)).slice(
|
||||
y.domain.start(), y.domain.end())
|
||||
out.compact()
|
||||
return out
|
||||
|
||||
|
|
@ -115,8 +149,10 @@ def eval_stl_next(phi, dt):
|
|||
f = eval_stl(phi.arg, dt)
|
||||
|
||||
def _eval(x):
|
||||
out = traces.TimeSeries((t + dt, v) for t, v in f(x))
|
||||
y = f(x)
|
||||
out = traces.TimeSeries(((t + dt, v) for t, v in y), domain=y.domain)
|
||||
out.compact()
|
||||
|
||||
return out
|
||||
|
||||
return _eval
|
||||
|
|
@ -127,6 +163,17 @@ def eval_stl_ap(phi, _):
|
|||
def _eval(x):
|
||||
out = x[str(phi.id)]
|
||||
out.compact()
|
||||
|
||||
return out
|
||||
|
||||
return _eval
|
||||
|
||||
|
||||
@eval_stl.register(stl.LinEq)
|
||||
def eval_stl_lineq(phi, _):
|
||||
def _eval(x):
|
||||
out = x[phi]
|
||||
out.compact()
|
||||
return out
|
||||
|
||||
return _eval
|
||||
|
|
|
|||
|
|
@ -1,13 +1,12 @@
|
|||
import hypothesis.strategies as st
|
||||
import traces
|
||||
|
||||
from hypothesis import given # , settings, Verbosity, Phase
|
||||
from hypothesis import given, settings, Verbosity, Phase
|
||||
from pytest import raises
|
||||
|
||||
import stl
|
||||
import stl.boolean_eval
|
||||
import stl.fastboolean_eval
|
||||
# from stl.hypothesis import SignalTemporalLogicStrategy
|
||||
|
||||
from stl.hypothesis import SignalTemporalLogicStrategy
|
||||
"""
|
||||
TODO: property based test that fasteval should be the same as slow
|
||||
TODO: property based test that x |= phi == ~(x |= ~phi)
|
||||
|
|
@ -24,40 +23,26 @@ TODO: Automatically generate input time series.
|
|||
"""
|
||||
|
||||
x = {
|
||||
"x": traces.TimeSeries([(0, 1), (0.1, 1), (0.2, 4)]),
|
||||
"y": traces.TimeSeries([(0, 2), (0.1, 4), (0.2, 2)]),
|
||||
"AP1": traces.TimeSeries([(0, True), (0.1, True), (0.2, False)]),
|
||||
"AP2": traces.TimeSeries([(0, False), (0.2, True), (0.5, False)]),
|
||||
"AP3": traces.TimeSeries([(0, True), (0.1, True), (0.3, False)]),
|
||||
"AP4": traces.TimeSeries([(0, False), (0.1, False), (0.3, False)]),
|
||||
"AP5": traces.TimeSeries([(0, False), (0.1, False), (0.3, True)]),
|
||||
"x":
|
||||
traces.TimeSeries([(0, 1), (0.1, 1), (0.2, 4)], domain=(0, 10)),
|
||||
"y":
|
||||
traces.TimeSeries([(0, 2), (0.1, 4), (0.2, 2)], domain=(0, 10)),
|
||||
"AP1":
|
||||
traces.TimeSeries([(0, True), (0.1, True), (0.2, False)], domain=(0, 10)),
|
||||
"AP2":
|
||||
traces.TimeSeries([(0, False), (0.2, True), (0.5, False)], domain=(0, 10)),
|
||||
"AP3":
|
||||
traces.TimeSeries([(0, True), (0.1, True), (0.3, False)], domain=(0, 10)),
|
||||
"AP4":
|
||||
traces.TimeSeries(
|
||||
[(0, False), (0.1, False), (0.3, False)], domain=(0, 10)),
|
||||
"AP5":
|
||||
traces.TimeSeries([(0, False), (0.1, False), (0.3, True)], domain=(0, 10)),
|
||||
}
|
||||
|
||||
|
||||
@given(st.just(stl.ast.Next(stl.BOT) | stl.ast.Next(stl.TOP)))
|
||||
# @given(SignalTemporalLogicStrategy)
|
||||
# @settings(max_shrinks=0, verbosity=Verbosity.verbose,
|
||||
# perform_health_check=False,
|
||||
# phases=[Phase.generate])
|
||||
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)
|
||||
|
||||
# phi2 = stl.alw(stl.ast.Next(phi))
|
||||
# phi3 = stl.ast.Next(stl.alw(phi))
|
||||
# stl_eval7 = stl.boolean_eval.pointwise_sat(phi2)
|
||||
# stl_eval8 = stl.boolean_eval.pointwise_sat(phi3)
|
||||
# assert stl_eval7(x, 0) == stl_eval8(x, 0)
|
||||
|
||||
def test_eval_smoke_tests(phi):
|
||||
stl_eval9 = stl.boolean_eval.pointwise_sat(stl.ast.Next(phi))
|
||||
stl_eval10 = stl.boolean_eval.pointwise_sat(~stl.ast.Next(phi))
|
||||
assert stl_eval9(x, 0) != stl_eval10(x, 0)
|
||||
|
|
@ -75,9 +60,48 @@ def test_boolean_identities(phi):
|
|||
assert stl_eval13(x, 0)
|
||||
assert not stl_eval13(x, 0.4)
|
||||
|
||||
phi7 = stl.parse('G(~(AP4))')
|
||||
stl_eval14 = stl.boolean_eval.pointwise_sat(phi7)
|
||||
assert stl_eval14(x, 0)
|
||||
|
||||
phi8 = stl.parse('F(AP5)')
|
||||
stl_eval15 = stl.boolean_eval.pointwise_sat(phi8)
|
||||
assert stl_eval15(x, 0)
|
||||
|
||||
phi9 = stl.parse('(AP1) U (AP2)')
|
||||
stl_eval16 = stl.boolean_eval.pointwise_sat(phi9)
|
||||
assert stl_eval16(x, 0)
|
||||
|
||||
phi10 = stl.parse('(AP2) U (AP2)')
|
||||
stl_eval17 = stl.boolean_eval.pointwise_sat(phi10)
|
||||
assert not stl_eval17(x, 0)
|
||||
|
||||
with raises(NotImplementedError):
|
||||
stl.boolean_eval.eval_stl(None, None)
|
||||
|
||||
|
||||
@given(SignalTemporalLogicStrategy)
|
||||
@settings(
|
||||
max_shrinks=0,
|
||||
verbosity=Verbosity.verbose,
|
||||
perform_health_check=False,
|
||||
phases=[Phase.generate])
|
||||
def test_temporal_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):
|
||||
def test_temporal_identities2(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)
|
||||
|
|
|
|||
|
|
@ -16,7 +16,7 @@ def test_hash_inheritance(phi):
|
|||
assert hash(repr(phi)) == hash(phi)
|
||||
|
||||
|
||||
def test_sugar_smoke_test():
|
||||
def test_sugar_smoke():
|
||||
stl.parse('(x) <-> (x)')
|
||||
stl.parse('(x) -> (x)')
|
||||
stl.parse('(x) ^ (x)')
|
||||
|
|
|
|||
13
stl/utils.py
13
stl/utils.py
|
|
@ -9,6 +9,9 @@ from stl.ast import (And, F, G, Interval, LinEq, Neg, Or, AP_lens)
|
|||
from stl.types import STL
|
||||
|
||||
|
||||
oo = float('inf')
|
||||
|
||||
|
||||
def f_neg_or_canonical_form(phi: STL) -> STL:
|
||||
if isinstance(phi, LinEq):
|
||||
return phi
|
||||
|
|
@ -67,15 +70,15 @@ def get_times(x):
|
|||
return sorted(times)
|
||||
|
||||
|
||||
def const_trace(x):
|
||||
oo = float('inf')
|
||||
return traces.TimeSeries([(-oo, x)])
|
||||
def const_trace(x, start=0):
|
||||
return traces.TimeSeries([(start, x)], domain=traces.Domain(start, oo))
|
||||
|
||||
|
||||
def eval_lineq(lineq, x, domain, compact=True):
|
||||
lhs = sum(const_trace(term.coeff)*x[term.id] for term in lineq.terms)
|
||||
compare = op_lookup.get(lineq.op)
|
||||
output = lhs.operation(const_trace(lineq.const), compare)
|
||||
output.domain = domain
|
||||
|
||||
if compact:
|
||||
output.compact()
|
||||
|
|
@ -101,10 +104,6 @@ def env(phi, *, lo=0, hi=float('inf')):
|
|||
return F(Interval(lo, hi), phi)
|
||||
|
||||
|
||||
def until(phi1, phi2, *, lo, hi):
|
||||
return stl.ast.Until(Interval(lo, hi), phi1, phi2)
|
||||
|
||||
|
||||
def andf(*args):
|
||||
return reduce(op.and_, args) if args else stl.TOP
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue