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

switch to symbolic summation for smooth robustness

Browse source
This commit is contained in:
Marcell Vazquez-Chanlatte 2016-12-10 14:24:54 -08:00
parent f5b23637af
commit 5e9239a4f4
1 changed files with 20 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

34
stl/smooth_robustness.py
View file

@ -4,14 +4,14 @@ from functools import singledispatch
import sympy as sym import sympy as sym
from numpy import arange from numpy import arange
from funcy import pairwise, autocurry from funcy import pairwise
import stl.ast import stl.ast
from stl.ast import t_sym from stl.ast import t_sym
from stl.robustness import op_lookup from stl.robustness import op_lookup
@singledispatch @singledispatch
def smooth_robustness(stl, L, h, eps): def smooth_robustness(stl, L, h, eps, depth):
raise NotImplementedError raise NotImplementedError
@smooth_robustness.register(stl.And) @smooth_robustness.register(stl.And)
@ -35,37 +35,43 @@ def LSE(rs, eps=0.1):
@smooth_robustness.register(stl.Or) @smooth_robustness.register(stl.Or)
def _(stl, L, h, eps): def _(stl, L, h, eps, depth=0):
rl, rh = list(zip( rl, rh = list(zip(
*[smooth_robustness(arg, L, h, eps=eps/2) for arg in stl.args])) *[smooth_robustness(arg, L, h, eps=eps/2, depth=depth+1)
for arg in stl.args]))
return soft_max(rl, eps=eps/2), LSE(rh, eps=eps/2) return soft_max(rl, eps=eps/2), LSE(rh, eps=eps/2)
@autocurry
def x_ij(L, h, xi_xj): def x_ij(L, h, xi_xj):
x_i, x_j = xi_xj x_i, x_j = xi_xj
return (L*h + x_i + x_j)/2 return (L*h + x_i + x_j)/2
def soft_max2(r, eps, lo, hi, L, H, depth):
N = sym.ceiling((hi - lo) / H)
B = eps_to_base(eps, N)
i = sym.Symbol("i_{}".format(depth))
x_ij = (L*H + r.subs({t_sym: t_sym+i}) + r.subs({t_sym: t_sym+i+1}))/2
return sym.log(sym.summation(B**x_ij, (i, lo, hi)), B)
@smooth_robustness.register(stl.F) @smooth_robustness.register(stl.F)
def _(stl, L, H, eps): def _(stl, L, H, eps, depth=0):
lo, hi = stl.interval lo, hi = stl.interval
times = arange(lo, hi, H) times = arange(lo, hi, H)
rl, rh = smooth_robustness(stl.arg, L, H, eps=eps/2) rl, rh = smooth_robustness(stl.arg, L, H, eps=eps/2, depth=depth+1)
los, his = zip(*[(rl.subs({t_sym: t_sym + t}), return (soft_max2(rl, eps/2, lo, hi, L, H, depth),
rh.subs({t_sym: t_sym + t})) for t in times]) soft_max2(rh, eps/2, lo, hi, L, H, depth))
x_stars = list(map(x_ij(L, H), pairwise(his)))
return LSE(los, eps=eps/2), soft_max(x_stars, eps=eps/2)
@smooth_robustness.register(stl.Neg) @smooth_robustness.register(stl.Neg)
def _(stl, L, H, eps): def _(stl, L, H, eps, depth=0):
rl, rh = smooth_robustness(arg, L, H, eps) rl, rh = smooth_robustness(arg, L, H, eps, depth=depth+1)
return -rh, -rl return -rh, -rl
@smooth_robustness.register(stl.LinEq) @smooth_robustness.register(stl.LinEq)
def _(stl, L, H, eps): def _(stl, L, H, eps, depth=0):
op = op_lookup[stl.op] op = op_lookup[stl.op]
retval = op(eval_terms(stl), stl.const) retval = op(eval_terms(stl), stl.const)
return retval, retval return retval, retval